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

News

Boolector version 3.0.0 released.

Boolector is now hosted on GitHub and licensed under the MIT License.

Download

boolector-3.0.0

Documentation

Find the documentation of Boolector’s public C and Python APIs here.

Bibtex Entry

If you cite Boolector >= version 2.0, please use the system description in JSAT volum 9 (BibTex) as listed below:

@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},
}

License

Boolector is hosted on GitHub and licensed under the MIT License.

Technical Support

Please use the Boolector issue tracker for bug reports. For questions, comments or information on new releases, please use our Google group.