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 2018: Alt-Ergo, AProVE, Boolector, CVC4, MathSAT 5, Minkeyrink, OpenSMT 2, Q3B, 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, raSAT, RDL, SatEEn, Simplify, Simplics, SONOLAR, Spear, STeP, SVC, SWORD, UCLID, Yices.