A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
Documentation
BibTex
Publications
Slides
SMT competitions
People
Download Archive
Third Party Contributions
If you cite Boolector >= version 2.0, please use the system description in JSAT volum 9 (BibTex) as listed below:
@article{DBLP:journals/jsat/NiemetzPB14,
author = {Aina Niemetz and
Mathias Preiner and
Armin Biere},
title = {Boolector 2.0},
journal = {J. Satisf. Boolean Model. Comput.},
volume = {9},
number = {1},
pages = {53--58},
year = {2014},
url = {https://doi.org/10.3233/sat190101},
doi = {10.3233/sat190101},
biburl = {https://dblp.org/rec/journals/jsat/NiemetzPB14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}