Conclusion

This tutorial is a basic introduction to using SMT solvers. There are numerous resources available for those who wish to learn more.

The SMT-LIB website smt-lib.org has details about the SMT-LIB standard [5], as well as links to software and an extensive collection of benchmarks. More information on the foundations of SMT and how solvers work under the hood can be found in several overview papers and book chapters [R6], [R9], [R18]. There are also tool papers describing the most prominent SMT solvers, including: Alt- Ergo [R15], Bitwuzla [R33], cvc5 [R29], MathSAT [R14], OpenSMT2 [R26], SMTInterpol [R12], SMT-RAT [R16], STP [R22], veriT [R10], Yices2 [R19], and Z3 [R32]. More information about cvc5 is available on its website.