Welcome to Boolector’s API documentation!¶
Boolector is an SMT solver for the quantifier-free theory of bit vectors with arrays. It supports BTOR, SMT-LIB v1, and SMT-LIB v2 as input format and can be either used as a stand-alone SMT solver, or as back end for other tools via its public API. This is the documentation of Boolector’s public C interface and Python interface. For further information and the latest version of Boolector, please refer to http://fmv.jku.at/boolector.