Boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.

GitHub

Documentation
BibTex
Publications
Slides
SMT competitions
People
Download Archive
Third Party Contributions

License: MIT
CI

Third Party Contributions

Partial Haskell Bindings

https://github.com/jwaldmann/haskell-boolector by Johannes Waldmann

Benchmarks

BEEM benchmarks in BTOR format by Jori Dubrovin

pBoolector

The following sources represent the prototype implementation pBoolector as implemented by Christian Reisenberger for his master’s thesis. pBoolector is an extension of Boolector version 2.0.1 and will not be maintained in the future.

pboolector-0.1.tar.gz

pBoolector is a parallel implementation of Boolector based on bit-blasting and look-ahead for QF_BV. It is available under a restricted license for non-commercial use. See the COPYING and README files provided with the sources for license information and more detailed information on how to patch Boolector version 2.0.1 with the provided pBoolector sources.

Note: The pBoolector sources as provided are an extension to Boolector version 2.0.1 and are not compatible with earlier or later releases of Boolector.