SMT-LIB is an international initiative aimed at facilitating research and development in Satisfiability Modulo Theories (SMT). Since its inception in 2003, the initiative has pursued these aims by focusing on the following concrete goals.

  • Provide standard rigorous descriptions of background theories used in SMT systems.
  • Develop and promote common input and output languages for SMT solvers.
  • Connect developers, researchers and users of SMT, and develop a community around it.
  • Establish and make available to the research community a large library of benchmarks for SMT solvers.
  • Collect and promote software tools useful to the SMT community.
This website provides access to the following main artifacts of the initiative.
  • Documents describing the SMT-LIB input/output language for SMT solvers and its semantics;
  • Specifications of background theories and logics;
  • A large library of input problems, or benchmarks, written in the SMT-LIB language.
  • Links to SMT solvers and related tools and utilities.

Latest News

July 18, 2017

Version 2.6 of the SMT-LIB standard has been released and is now available in the Language section. Its main difference with Version 2.5 is the addition of algebraic datatypes to the language. See the document for more details.

Previous 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]

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.