Boolector 2.0

Aina Niemetz, Mathias Preiner, Armin Biere


In this paper, we discuss the most important changes and new features introduced with version 2.0 of our SMT solver Boolector, which placed first in the QF_BV and QF_ABV tracks of the SMT competition 2014. We further outline some features and techniques that where not yet described in the context of Boolector.


SMT; Lemmas on Demand; Lambdas; Don't Care Reasoning

Full Text:



Cyrille Artho, Armin Biere, and Martina Seidl. Model-Based Testing for Verification Back-Ends. In TAP, 7942 of LNCS. Springer, 2013.

A. Biere. Yet Another Local Search Solver and Lingeling and Friends Entering the SAT Competition 2014. In SAT Competition 2014, Univ. of Helsinki, 2014.

Robert Brummayer. Efficient SMT Solving for the Extensional Theory of Arrays. PhD thesis, JKU Linz, 2009.

Robert Brummayer and Armin Biere. Fuzzing and Delta-Debugging SMT solvers. In SMT 2009. ACM, 2009.

Robert Brummayer and Armin Biere. Lemmas on demand for the extensional theory of arrays. JSAT, 6(1-3), 2009.

Niklas Een and Niklas Sörensson. An extensible SAT-solver. In SAT’04, 2919 of LNCS. Springer, 2004.

Andreas Fröhlich, Gergely Kovásznai, and Armin Biere. Efficiently solving bit-vector problems using model checkers. In SMT 2013, Helsinki, Finland, 2013.

Aina Niemetz and Armin Biere. ddSMT: A Delta Debugger for the SMT-LIB v2 Format. In SMT 2014, Helsinki, Finland, 2013.

Aina Niemetz, Mathias Preiner, and Armin Biere. Turbo-charging lemmas on demand with don’t care reasoning. In FMCAD’14. IEEE, 2014.

Mathias Preiner, Aina Niemetz, and Armin Biere. Lemmas on demand for lambdas. In DIFTS’13, 1130 of CEUR Workshop Proceedings, 2013.

Christian Reisenberger. PBoolector: A Parallel SMT Solver for QF BV by Combining Bit-Blasting and Look-Ahead. Master’s thesis, JKU Linz, 2014.


  • There are currently no refbacks.

Comments on this article

View all comments