2019-06-14 09:37:00 +02:00
|
|
|
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of
|
|
|
|
|
fixed-size bit-vectors, arrays and uninterpreted functions. It supports the
|
|
|
|
|
SMT-LIB logics BV, QF_ABV, QF_AUFBV, QF_BV and QF_UFBV. Boolector provides a
|
|
|
|
|
rich C and Python API and supports incremental solving, both with the SMT-LIB
|
2021-06-02 10:02:45 +02:00
|
|
|
commands push and pop, and solving under assumptions.
|
2019-06-14 09:37:00 +02:00
|
|
|
|
|
|
|
|
WWW: https://boolector.github.io/
|
