MiniSmt is a simple SMT solver for non-linear arithmetic based on MiniSat and Yices. It accepts the SMT-LIB format as input, is efficient on small domains, supports reasoning about non-rational real numbers, and is able to output models.


The current stable version is 0.6. Get recent versions and view the changelog.
The current testing version is 0.4β. Feel free to test it through the web interface β.


Mar 9, 2014: version 0.6 released (compile with interfaced GPW)
Mar 21, 2013: version 0.5 released (compile properly w/ and w/o yices)
May 25, 2012: version 0.4 released (compile w/ and w/o yices)
February 14, 2012: version 0.4β released (download, web interface β, requires TTT2 1.08β)
July, 2010: MiniSmt comes first in QF_NIA and QF_NRA in SMT-COMP
March 12, 2010: version 0.3 released
January 14, 2010: version 0.2 released
September 19, 2009: version 0.1 released, homepage created



The authors are Harald Zankl and Simon Legner. For questions or feedback please write to   harald dot zankl at uibk dot ac dot at.

Third Party Libraries

MiniSmt interfaces the SAT solver MiniSat, the SMT solver Yices, and uses libraries from TTT2.