SMT-LIB The Satisfiability Modulo Theories Library (original) (raw)
SMT-LIB is an international initiative aimed at facilitating research and development inSatisfiability 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 forSMT 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
September 20, 2024
A new release of the the SMT-LIB 2.6 reference document is now available. This is a minor release. The main changes concern the verbosity of the output.
Previous News
April 2, 2024
Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server. Official yearly releases of the library will be availableZenodo.
Older News
Feb 13, 2024
The latest release (2023) of the SMT-LIB benchmark library is now available on Zenodo in the form of compressed archives.