This is the main web site of the SMT-LIB initiative.

The major goal of SMT-LIB is to establish a library of benchmarks for Satisfiability Modulo Theories, that is, satisfiability of formulas with respect to background theories for which specialized decision procedures exist---such as, for instance, the theory of lists, of arrays, linear arithmetic, and so on.

Systems for satisfiability modulo theories have applications in formal verification, compiler optimization, and scheduling, among others. A lot of work has been done in the last few years on building SMT systems. The main motivation of the SMT-LIB initiative is that having a library of benchmarks will greatly facilitate the evaluation and the comparison of these 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 for propositional satisfiability.

To reach its goals, the initiative first aims at establishing a common standard for the specification of benchmarks and of background theories. An initial version of the standard has been developed within the SMT-LIB interest group.

Documentation on the latest version of the SMT-LIB language and format is available in the Documents section.