Welcome to Boolector’s API documentation!

Introduction

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 https://boolector.github.io.