Boolector

News

Release 1.6.0.

Release 1.5.118.

BEEM benchmarks in BTOR format contributed by Jori Dubrovin.

Release 1.4.1 fixes a bug by removing unconstrained expression optimization.

Source code release of Boolector 1.4 until 1.5.118 under GPL.

Launched Google group.

Download

Latest source release 1.6.0:

boolector-1.6.0-with-sat-solvers.tar.gz ]

Starting with version 1.6.0 we use a restricted license for non-commercial use.

By default it is also prohibited to use these newer version of Boolector as part of a competition, without explicit written permission.

Older versions are still available under the GNU General Public License Version 3:

boolector-1.5.118-6b56be4-121013.tar.gz ]
boolector-1.5.116-eeaf10b-121004.tar.gz ]
boolector-1.5.115-5d546c8-120922.tar.gz ]
boolector-1.4.1-376e6b0-110304.tar.gz ]
boolector-1.4-ffc2089-100608.tar.gz ]
boolector-1.3-e71a070-100601.tar.gz ]

The over-due source release 1.5.115 of Boolector is close to the version used in the SMT Competition 2012, where Boolector ranked first in both bit-vector tracks, with and without arrays. It is best used in combination with the latest public version al6 of Lingeling, but also works with PicoSAT and MiniSAT. The source code of these SAT solvers needs to be obtained separately with the archives listed above.

Version 1.5.118 uses the 'simpdelay' feature of Lingeling for faster solving of simple instances and the library has now support for choosing the SAT solver through the API. This only works with a newer Lingeling of Version ala and above.

In version 1.5.116 we fixed a wrong assertion and made the examples compile again. It now also uses the latest reentrant version 953 of PicoSAT, i.e.  does not work with previous versions of PicoSAT anymore.

The following archives contain easier to compile versions of Boolector 1.5.115 packaged already with Lingeling al6 respectively a package with Boolector 1.5.116, Lingeling al6, PicoSAT 953, and MiniSAT 2.2.0.

boolector-1.5.118-with-sat-solvers.tar.gz ]
boolector-1.5.116-with-sat-solvers.tar.gz ]
boolector-1.5.115-with-lingeling-al6.tar.bz2 ]

These versions with Lingeling version al6 as back-end should be slightly faster on the plain bit-vector benchmarks without array from the SMT Competition 2012, than the competition version 1.5.110-agm and slightly slower on those with arrays. This is both mainly due to Lingeling. The competition version of Lingeling is not available publically. You find more information on this new version of Boolector in the NEWS file. See also the README and COPYING files.

Older versions

The 3rd source code release of Boolector 1.4.1 fixes a rare bug in the simplifier by removing the unconstrained expression optimization.

boolector-0.0.tar.bz2 ]
boolector-0.5.tar.bz2 ]
boolector-0.6.tar.bz2 ]
boolector-0.7.tar.bz2 ]
boolector-1.0-IA-32.tar.bz2 ]
boolector-1.1-IA-32.tar.bz2 ]

These are all 32-bit statically linked Linux-x86 binaries. We do not support other platforms at this moment. A source release is not planned either. Finally, the restrictions of the license section apply.

Overview

Boolector is an SMT solver for bit-vectors and arrays. Version 0.0 was used in experiments that are described in our recent SMT'08 paper. Version 0.4 entered the SMT'08 competition and is available from the overview of competitors. It won first places in both the bit-vector (QF_BV) and bit-vector with arrays track (QF_AUFBV). See www.smtcomp.org/2008 for more details. In the latest SMT competition, Boolector 1.2 won the second place in QF_BV and again the first place in QF_AUFBV.

A small history of Boolector can be found in the NEWS file.

Currently, we are working on papers that describe and evaluate Boolector's under-approximation features.

Community

Please use our google group for any questions, bug reports and comments. You should also join if you want to be informed of new releases.

Publications related to Boolector

Slides related to Boolector

License

Boolector is copyrighted 2007 - 2010 by Robert Brummayer, and 20007 - 2012 Armin Biere, both Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria.

The older binary releases until and including Boolector 1.2 are available for research and evaluation purposes in an academic environment only. They can not be used in a commercial environment, particularly as part of a commercial product, without written permission.

For the newer source code releases, starting with Boolector 1.3, we use the GNU General Public License Version 3 (GPLV3). You can find more information about GPLV3 in the file COPYING that comes with the sources. In particular, this license forbids to link or use Boolector 1.3 in a redistributed program, without making the source code of that program available under GPL as well.

In general, Boolector is provided as is, without any warranty.

Please contact Armin Biere for additional questions regarding licensing Boolector under a different license or to obtain more up-to-date versions.