SMT Solvers

This is an incomplete list of publicly available SMT solvers. Please contact us if you have or know of another solver not listed here.

Current Systems

To our knowledge, the following systems (listed alphabetically) were under active development in 2015: Alt-Ergo, AProVE, Boolector, CVC4, MathSAT 5, OpenSMT 2, raSAT, SMTInterpol, SMT-RAT, STP, veriT, Yices 2, 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. Ario, Barcelogic, Beaver, CVC3, DPT, Fx7, haRVey, ICS, iSAT3, LPSAT, MathSAT 4, MiniSmt, Mistral, OpenSMT, RDL, SatEEn, Simplify, Simplics, SONOLAR, Spear, STeP, SVC, SWORD, UCLID, Yices.