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 http://fmv.jku.at/boolector.

API Documentations

• Boolector C API documentation
  • Interface
  • Quickstart
  • Options
  • Internals
  • Examples
• Boolector Python API documentation
  • Interface
  • Quickstart
  • Options
  • Internals
  • Examples