Skip to content
Documentation
Development
SMT

SMT

ESBMC encodes verification conditions into SMT and discharges them with backends such as Bitwuzla, Z3, Boolector, CVC4/CVC5, Yices, and MathSAT. These guides cover extending that backend.

Implementing an SMT Theory
Add a new SMT theory to ESBMC’s encoding.
Integrating a New SMT Solver
Wire a new solver into the ESBMC backend.
Updating an SMT Solver
Update an existing solver integration to a new version.