Welcome to Boolector’s API documentation!¶

Introduction¶

Boolector is an SMT solver for the theories of bit-vectors, arrays, uninterpreted functions and their combinations. Boolector 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 https://boolector.github.io.

API Documentations¶