Description
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.Download
The current stable version is 0.66. Get recent versions and view the changelog.The current testing version is 0.4β. Feel free to test it through the web interface β.
News
| 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 |
Documents
-
H. Zankl and A. Middeldorp
Satisfiability of Non-Linear (Ir)rational Arithmetic
In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), Lecture Notes in Artificial Intelligence 6355, pp. 481-500, 2010. © Springer-Verlag
Contact
The authors are Harald Zankl and Simon Legner. For questions or feedback please write toharald dot zankl at uibk dot ac dot at.