About SMT-LIB

SMT-LIB was created with the expectation that the availability of common standards and a library of benchmarks would greatly facilitate the evaluation and the comparison of SMT systems, and advance the state of the art in the field in the same way as, for instance, the TPTP library has done for theorem proving, or the SATLIB library has done initially for SAT.

These expectations have been largely met, thanks in no small part to extensive contributions from the research community and to an annual SMT solver competition, SMT-COMP, based on benchmarks from the library. The initiative is, however, still on-going, with work on improving the usefulness and the scope of the SMT-LIB language, defining new background theories, and collecting more benchmarks.

About SMT

Satisfiability Modulo theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas with respect to some logical theory T of interest. It differs from general automated deduction in that the background theory T need not be finitely or even first-order axiomatizable, and specialized inference methods are used for each theory. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, quantifier-free formulas), these specialized methods can be implemented in solvers that are more efficient in practice than general-purpose theorem provers.

While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications in other areas of computer science such as, for instance, planning, model checking and automated test generation. Typical theories of interest in these applications include formalizations of arithmetic, arrays, bit vectors, algebraic datatypes, equality with uninterpreted functions, and various combinations of these.

Latest News

June 8, 2017

A new release of the SMT-LIB benchmark library is now available, both on the GitLab server and on StarExec. For this release we have fixed minor errors in formatting; removed duplicate benchmarks; updated statuses of 6,492 previously unknown benchmarks; added new benchmarks in new logics. [More]

Previous News

June 5, 2017

A close-to-final draft of the upcoming version of the SMT-LIB standard, version 2.6, is now available in the Language section. The most notable new features is the addition of algebraic datatypes to the language.

Older News

May 30, 2017

The discussion list smt-lib@cs.nyu.edu has been decommissioned. Its archives will remain available at http://www.cs.nyu.edu/pipermail/smt-lib. The new discussion forum for SMT-LIB is now https://groups.google.com/d/forum/smt-lib.