This is an incomplete list of publicly available SMT solvers. Please contact us if you have or know of another solver not listed here.
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.
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.