Documentation
SMT
Implementing SMT Solver

Implementing SMT Solver

In order to integrate a new SMT solver into the ESBMC backend, we would need to follow these steps:

  1. Copy and paste this directory:

https://github.com/esbmc/esbmc/tree/master/src/solvers/z3

  1. Replace everything with “z3” by “NewSolver”.

  2. Replace the calls to the Z3 SMT solver methods with those from your NewSolver in https://github.com/esbmc/esbmc/tree/master/src/solvers/z3.

  3. Update https://github.com/esbmc/esbmc/blob/master/src/solvers/z3/CMakeLists.txt.

  4. Update https://github.com/esbmc/esbmc/blob/master/src/solvers/CMakeLists.txt#L24 https://github.com/esbmc/esbmc/blob/master/src/solvers/solve.cpp#L10 https://github.com/esbmc/esbmc/blob/master/src/solvers/solve.cpp#L40

  5. Update https://github.com/esbmc/esbmc/blob/master/BUILDING.md

  6. Update: https://github.com/esbmc/esbmc/blob/7f41ac14baf26ca32521781a9404105413dc61a4/src/esbmc/options.cpp#L93-L97

  7. Update https://github.com/esbmc/esbmc/blob/7f41ac14baf26ca32521781a9404105413dc61a4/src/esbmc/esbmc_parseoptions.cpp#L1752

  1. Update: https://github.com/esbmc/esbmc/blob/7f41ac14baf26ca32521781a9404105413dc61a4/src/solvers/solver_config.h.in#L1

  2. Integrate the solver into the CI: Build and Release

Implementing SMT Theory