PV4 ⊧ Boolectorproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

One of the following:

• BTOR/BTOR2 (its own formats)
• SMT-LIB (version 1.2 or 2.0)

Expected output

• If satisfiable then it can print a model (if model generation is enabled) or query assignments of bit vector and array variables or uninterpreted functions.
• Else unsatisfiable

Comments

This is an SMT solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It has a C and Python API.