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