SMT Solvers

This is an incomplete list of publicly available SMT solvers.

Please contact us if you have or know of other solvers not listed here.

Current Systems

To our knowledge, the following systems (listed alphabetically) were under active development in 2011-12:

Alt-Ergo, Barcelogic, Beaver, Boolector, CVC4, MathSAT 5, Mistral, SMTInterpol, SONOLAR, STP, veriT, Yices, Z3.

Older Systems

To our knowledge, the following systems are no longer current as their development has been discontinued. They are included for historical reasons and comparison purposes.

Argo-lib, Ario, CVC, CVC Lite, CVC3, DPT, Fx7, haRVey, HTP, ICS, LPSAT, MathSAT 4, MiniSmt, OpenSMT, RDL, SatEEn, Sammy, Simplify, Simplics, Spear, STeP, SVC, SWORD, Tsat++, UCLID.