Boolector

News

Boolector won first places in 3 divisions (out of 5) of the main track of the SMT Competition 2016.

Release 2.4.1.

Release 2.4.0.

Release 2.3.1.

Boolector won first places in 3 division (out of 6) of the SMT Competition 2016.

Release 2.2.0.

Boolector won first places in 3 division (out of 5) of the SMT Competition 2015.

pBoolector: release 0.1 (parallel prototype implementation)

Partial Haskell bindings: https://github.com/jwaldmann/haskell-boolector (by Johannes Waldmann)

BEEM benchmarks in BTOR format contributed by Jori Dubrovin.

Download

boolector-2.4.1-with-lingeling-bbc.tar.bz2 ]

This version of Boolector is available under a restricted license for non-commercial use.

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

See the NEWS, README and COPYING files for more detailed information on Boolector and its license.

Please use our google group for any questions, bug reports, comments and information on new releases.

Documentation

The documentation of Boolector's public APIs can be found here.

Bibtex Entry

Use the system description in JSAT vol. 9 for citations of current versions of Boolector (>=2.0):

@article{NiemetzPreinerBiere-JSAT15,
  title={Boolector 2.0 system description},
  author={Aina Niemetz and Mathias Preiner and Armin Biere},
  journal={Journal on Satisfiability, Boolean Modeling and Computation},
  volume={9},
  pages={53-58},
  year={2014 (published 2015)},
  publisher={IOS Press},
}

Publications related to Boolector

Aina Niemetz, Mathias Preiner, Armin Biere. Propagation based local search for bit-precise reasoning . In Journal of Formal Methods in System Design, Springer, 29 pages, published online first, October 2, 2017.
[ paper | preprint | bibtex | experiments ]

Aina Niemetz, Mathias Preiner, Armin Biere. Model-Based API Testing for SMT Solvers. In Proc. 15th Intl. Workshop on Satisfiability Modulo Theories (SMT'17), 10 pages, aff. to CAV'17, Heidelberg, Germany, 2017.
[ paper | bibtex | boolector ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2017. Technical Report 17/1, June 2017, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Aina Niemetz. Bit Precise Reasoning Beyond Bit-Blasting. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2017.
[ thesis | bibtex ]

Mathias Preiner. Lambdas, Arrays and Quantifiers. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2017.
[ thesis | bibtex ]

Mathias Preiner, Aina Niemetz, Armin Biere. Counterexample-Guided Model Synthesis. In Proc. 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Lecture Notes in Computer Science (LNCS) vol. 10205, pages 264-280, Springer 2017.
[ paper | bibtex | data | boolector ]

Aina Niemetz, Mathias Preiner, Armin Biere. Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. In Proc. 28th Intl. Conf. on Computer Aided Verification (CAV'16), Lecture Notes in Computer Science (LNCS) vol. 9779, pages 199-217, Springer 2016.
[ paper | bibtex | data ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2016. Technical Report 16/1, June 2016, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex ]

Mathias Preiner, Aina Niemetz, Armin Biere. Better Lemmas with Lambda Extraction. In Proc. 15th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'15), pages 128-135, FMCAD Inc. 2015.
[ paper | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhpch. Improving Local Search For Bit-Vector Logics in SMT with Path Propagation. In Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15), 10 pages, aff. to FMCAD'15, Austin, TX, USA, 2015.
[ paper | bibtex | data ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2015. Technical Report 15/1, June 2015, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ paper | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector 2.0 Journal of Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, 2015, pages 53-58.
[ paper | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere. Turbo-Charging Lemmas on Demand with Don't Care Reasoning. In Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), 179-186, FMCAD Inc, 2014.
[ paper | bibtex | data ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2014. Technical Report 14/1, June 2014, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ paper | bibtex ]

Mathias Preiner, Aina Niemetz, Armin Biere. Lemmas on Demand for Lambdas. In Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems, 10 pages, aff. to FMCAD'13, Portland, Oregon, USA, 2013.
[ paper | bibtex | data ]

Armin Biere. Boolector Entering the SMT Competition 2012. Technical Report 12/1, June 2012, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ paper | bibtex ]

Robert Brummayer. Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2009.
[ thesis | bibtex ]

Robert Brummayer, Armin Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), Lecture Notes in Computer Science (LNCS), vol. 5505, Springer 2009.
[ paper | bibtex ]

Robert Brummayer, Armin Biere. Lemmas on Demand for the Extensional Theory of Arrays. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 6, pages 165-201, Delft University, 2009.
[ paper | bibtex ]

Robert Brummayer, Armin Biere, Florian Lonsing. BTOR: Bit-Precise Modeling of Word-Level Problems for Model Checking. In Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA, July 2008.
[ paper | bibtex ]

Robert Brummayer, Armin Biere. Lemmas on Demand for the Extensional Theory of Arrays. In Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08), Princeton, New Jersey, USA, July 2008.
[ paper | bibtex ]

Andreas Vida. Random Test Case Generation and Delta Debugging for BitVector Logic with Arrays. Master Thesis, Johannes Kepler University, Oct. 2008.
[ Master thesis | software ]

Slides related to Boolector

Awards

  • SMT Competition 2017:
    Divisions:  QF_BV (main track), QF_UFBV (main track), QF_ABV (main track), QF_AUFBV (main track), BV (main track)
    Competing version:  Boolector 3.0-pre
    Awards: 1st place in QF_BV (main track)
    1st place in QF_UFBV (main track)
    1st place in QF_ABV (main track)

  • SMT Competition 2016:
    Divisions:  QF_BV (main track), QF_UFBV (main track), QF_ABV (main track), QF_AUFBV (main track), BV (main track), UFBV (main track)
    Competing version:  Boolector 2.999
    Awards: 1st place in QF_BV (main track)
    1st place in QF_UFBV (main track)
    1st place in QF_ABV (main track)

  • SMT Competition 2015:
    Divisions:  QF_BV (main and application track), QF_UFBV (main track), QF_ABV (main track), QF_AUFBV (main track)
    Competing version:  Boolector 2.1.0
    Awards: 1st place in QF_BV (main track)
    1st place in QF_UFBV (main track)
    1st place in QF_ABV (main track)

  • SMT Competition 2014:
    Divisions:  QF_BV (main track), QF_ABV (main track)
    Competing version:  Boolector 2.0.0
    Awards: 1st place in QF_BV (main track)
    1st place in QF_ABV (main track)
     Boolector thus won one Gödel medal during the FLoC'14 Olympic Games.

  • SMT Competition 2012:
    Divisions:  QF_BV (main track), QF_AUFBV (main track)
    Competing version:  Boolector 1.5.110-agm
    Awards: 1st place in QF_BV (main track)
    1st place in QF_AUFBV (main track)

  • SMT Competition 2011:
    Divisions:  QF_BV (main track), QF_AUFBV (main track)
    Competing version:  Boolector 1.5.23-833
    Awards: 3rd place in QF_BV (main track)
    1st place in QF_AUFBV (main track)

  • SMT Competition 2010:
     no participation

  • SMT Competition 2009:
    Divisions:  QF_BV (main track), QF_AUFBV (main track)
    Competing version:  Boolector 1.2
    Awards: 2nd place in QF_BV (main track)
    1st place in QF_AUFBV (main track)

  • SMT Competition 2008:
    Divisions:  QF_BV (main track), QF_AUFBV (main track)
    Competing version:  Boolector 0.4
    Awards: 1st place in QF_BV (main track)
    1st place in QF_AUFBV (main track)

License

Newer versions, starting with release 1.6.0, use a restricted license for non-commercial use.

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

All source code releases prior to release 1.6.0 are still available under the GNU General Public License Version 3.

All binary releases (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.

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.

Older versions

The following versions are available under a restricted license for non-commercial use.
Note that by default it is also prohibited to use versions of Boolector under this license as part of a competition without explicit written permission.

boolector-2.4.0-with-lingeling-bbc.tar.bz2 ]
boolector-2.3.1-with-lingeling-bbc.tar.bz2 ]
boolector-2.2.0-with-lingeling-bal.tar.bz2 ]
boolector-2.1.1-with-lingeling-b85.tar.bz2 ]
boolector-2.0.7-with-lingeling-azd.tar.bz2 ]
boolector-2.0.6-with-lingeling-azd.tar.bz2 ]
boolector-2.0.5-with-lingeling-azd.tar.bz2 ]
boolector-2.0.4-with-lingeling-azd.tar.bz2 ]
boolector-2.0.1-with-lingeling-azd.tar.bz2 ]
boolector-2.0.0-with-lingeling-azd.tar.bz2 ]
boolector-1.6.0-with-sat-solvers.tar.gz ]

The following 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 ]

Release 1.5.118 uses the 'simpdelay' feature of Lingeling for faster solving of simple instances. Further, the library now supports choosing the SAT solver via the API. This release only works with a newer Lingeling of Version ala and above.

Release 1.5.116 fixes an incorrect assertion and the examples provided (which were previously broken) compile again. This release uses the latest reentrant version 953 of PicoSAT, hence it does not work with previous versions of PicoSAT.

Release 1.5.115 of Boolector is close to the version used in the SMT Competition 2012. It is best used in combination with 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.

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

The following archives contain easier to compile versions of Boolector 1.5.115 packaged with Lingeling al6, and Boolector 1.5.116 and 1.5.118 packaged with 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 than the competition version 1.5.110-agm on the plain bit vectors without arrays benchmarks from the SMT Competition 2012, and slightly slower on those with arrays. This is both mainly due to Lingeling. The competition version of Lingeling is not available publically.

The following releases are all 32-bit statically linked Linux-x86 binaries. For these versions, we do neither support other platforms nor do we plan a source release. Finally, the restrictions of the license section apply.

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

pBoolector

The following sources represent the prototype implementation pBoolector, a parallel implementation of Boolector based on bit-blasting and look-ahead for QF_BV. This version was developed by Christian Reisenberger for his master's thesis and will not be maintained in the future.

It is available under a restricted license for non-commercial use. See the README and COPYING files provided with the sources for more detailed information on pBoolector and its license.

Note that the pBoolector sources as provided are an extension to the SMT solver Boolector version 2.0.1.

pboolector-0.1.tar.gz ]