News
May 12, 2021A new release of the the SMT-LIB 2.6 reference document is now available. This is a minor release addressing a minor error in the 2021-04-02 release.
April 2, 2021A new release of the the SMT-LIB 2.6 reference document is now available. This is a minor release addressing a few errors in the 2017-07-18 release.
Feb 11, 2020A theory of Unicode character strings and regular expressions has been added to the set of SMT-LIB theories.
May 9, 2019A new release of the SMT-LIB benchmark library (2019-05-09) is now available, both on the GitLab server and on StarExec. For this release, we have:
- Added 49,005 new benchmarks in new logics: non-incremental: QF_BVFPLRA (1), QF_FPLRA (13), QF_S (1976), QF_SLIA (46,350), UFDTNIA (1); incremental: QF_AUFBVLIA (441), QF_AUFBVNIA (44), QF_UFBVLIA (179).
- Added 17,890 new benchmarks in existing logics: non-incremental: FP (2,415), QF_ABV (17), QF_AUFBV (25), QF_BV (1594), QF_UFBV (10), QF_UFNIA (471), UFDTLIA (24), UFNIA (10,105); incremental: QF_ABV (1,257), QF_ABVFP (60), QF_AUFBV (21), QF_BV (1,771), QF_BVFP (117), QF_UFBV (3).
- Updated statuses of 3039 previously unknown non-incremental benchmarks (based on the results from 2 or more solvers from SMT-COMP'18).
- Updated 79255 statuses of previously unknown incremental check-sat calls (based on the results from 2 or more solvers from SMT-COMP'18).
- Removed duplicate benchmarks
- Unified Sage2 and QF_BV benchmark repositories (non-incremental).
- Benchmarks with a size >= 10M are now stored via git LFS. Please refer to the repository's README on how to check out the repository.
- We unified the Sage2 and QF_BV repositories into one repository. A fresh checkout is required since the git history of the repository has been rewritten.
A new release of the SMT-LIB benchmark library (2018-05-20) 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 18,739 previously unknown non-incremental benchmarks (based on the results from 2 or more solvers from SMT-COMP'17); updated 232,167 statuses of previously unknown incremental check-sat calls (based on the results from 2 or more solvers from SMT-COMP'17); added 3,121 new benchmarks in new logics: (non-incremental: AUFNIA (3), incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327)); added 7,969 new benchmarks in previous logics: (non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5), QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807), QF_UFBV (1193) - incremental: QF_BV (787), QF_LIA (1) For details on the changes to SMT-LIB, please check the git logs for incremental and non-incremental benchmarks.
July 18, 2017Version 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.
June 8, 2017A 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 based on the results produced by 2 or more solvers from SMT-COMP'16; added new benchmarks in new logics: ABVFP, AUFBVDTLIA, AUFDTLIA, BVFP, FP, QF_ABVFP, QF_DT, UFDT, UFDTLIA (non-incremental) and ABVFP, BV, BVFP, LRA, QF_ABVFP, QF_BVFP, QF_FP (incremental); added new benchmarks in existing logics: BV, LRA, QF_BV, QF_BVFP, QF_FP, QF_LRA, QF_NIA, QF_NRA, UF (non-incremental) and QF_BV (incremental). For details on the changes to SMT-LIB, please check the git logs for the non-incremental and incremental benchmarks.
June 5, 2017A 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.
May 30, 2017The 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.
April 27, 2017The SMT-LIB benchmark repository is now hosted on the SMT-LIB GitLab service. See the Benchmarks section for more info.
June 1, 2015
A new release of the SMT-LIB
benchmark library is available on StarExec. Many old benchmarks that
had status "unknown" now have updated statuses of either "sat" or
"unsat". A number of new benchmarks have also been added, both
incremental and non-incremental. Incremental divisions with new
benchmarks are: ALIA, ANIA, LIA, QF_ALIA, QF_ANIA, QF_LIA, QF_NIA, and
QF_UFNIA. Non-incremental divisions with new benchmarks are: LIA, NIA,
QF_ALIA, QF_AUFNIA, QF_LIRA, QF_NIA, QF_NIRA, UFBV, UFLIA, and UFNIA.
Benchmarks can be downloaded directly from StarExec or from a mirror at
NYU.
May 28, 2015
Version 2.5 of the SMT-LIB standard is out!
It is an extension of Version 2.0 and, with two minor exceptions, it is fully backward compatible with that previous version.
See the Language section for the reference document.
June 11, 2014
For bulk downloads, zip archives containing section of the latest release of the repository (2014-06-03) are also available. See the Benchmarks section for further instructions.
June 4, 2014
The migration of the benchmark repository to the StarExec service is now complete. See the Benchmarks section for instructions on how to access the repository.
The current release, 2014-06-03, has been considerably expanded with new logics and thousands of new benchmarks.
We have also created a few new logics that best describe some sets of benchmarks. As a consequence, a number of old benchmarks have been reclassified accordingly logic-wise.
June 4, 2014
We have added a graph in the Logics section that illustrates the containment relation between the various SMT-LIB logics.
May 24, 2014
A theory of floating point numbers, called FloatingPoint, has
been added to the Theories section.
May 24, 2014
A new, completely revamped web site went live today.
June 26, 2013
A :value attribute has been defined for the theory FixedSizedBitvectors.
June 26, 2013
The theory Fixed_Sized_Bitvectors has been renamed FixedSizedBitvectors, for naming consistency. The logic declarations that refer to that theory have been updated accordingly.
September 9, 2012
A new release of the reference of the Version 2.0 reference document has been posted in the Documents section. It contains a few minor fixes and a clarification on the language of a logic.
June 14, 2011
The definition of bvsmod in the QF_BV logic has been updated to correct a bug (the definition was incorrect in case the divisor is negative and the dividend is a multiple of the divisor).
June 11, 2011
The declarations for the following logics have been added in the Logics section: QF_NRA, QF_UFBV, QF_UFLIA, QF_UF, LRA, QF_UFNRAUFLRA, UFNIA. A couple of them are new. The rest had had benchmarks in the library for a while but their declaration was missing.
June 03, 2011
Fixed an error in the declaration of all the logics including the Reals theory (the definition of coefficient in the :extension attribute was missing a case).
June 03, 2011
Added a note to the declaration of QF_UFIDL.
June 03, 2011
Extended the definition of linear term in the :extension attribute of QF_AUFLIA.
January 18, 2011
Links to a set of Java utilities for SMT-LIB 2 scripts has been added in the Utilities section.
January 18, 2011
A tutorial, by D. Cok, on the SMT-LIB 2 format has been added in the Documents section.
December 21, 2010
A new release of the Version 2.0 reference document has been posted in the Documents section. This is another minor release, fixing a number errors, clarifying the text in a few points, and adjusting the standard in minor ways.
September 1, 2010
Section Utilities has been revamped, with the addition of two parsers for SMT-LIB 2.
August 28, 2010
A new release of the Version 2.0 reference document has been posted in the Documents section. This is a minor release, fixing a number errors, clarifying the text in a few points, and adjusting the standard in minor ways.
May 4, 2010
An initial version of the benchmark repository in the SMT-LIB 2.0 format is now available in the Benchmarks section. Conformance checking is still ongoing, and these benchmarks may be changed to conform to the SMT-LIB 2.0 format.
May 1, 2010
A number of theory and logic declarations have been converted from Version 1.2 to Version 2.0 of the SMT-LIB format. They are available in the Theories and Benchmarks sections. More theories and logic declarations will be added in the next few days.
March 30, 2010
Version 2.0 of the SMT-LIB format has been released. Its reference document, which supersedes all previous drafts, is now available from the Documents section.
February 10, 2010
An updated, almost final draft of the Version 2.0 document is now available in the Documents section.
February 1, 2010
A draft of the coming Version 2.0 of the SMT-LIB format is now available in the Documents section.
August 18, 2009
A link to Robert Brummayer's SMT debugging utilities has been added in the Utilities section.
July 4, 2009
The logic LRA, for (quantified) formulas in linear real arithmetic, has been added.
July 2, 2009
Updates and additions to the new 2009 benchmarks have been posted to the SMT-LIB benchmark page. No new benchmarks will be added before SMT-COMP 2009. These benchmarks are in the process of being integrated with the SMT-LIB.
June 25, 2009
Three new logics have been added, all having to do with non-linear arithmetic: QF_NIA, QF_UFNRA and UFNIA.
June 3, 2009
New benchmarks for 2009 have been posted to the SMT-LIB benchmark page. These benchmarks are in the process of being integrated with the SMT-LIB.
June 5, 2008
QF_BV/spear benchmarks were missing the ":formula" attribute. ":formula true" has been added to all of these benchmarks.
June 1, 2008
Status and difficulty updates have been done across all benchmarks. Also, 1485 benchmarks were moved from QF_AUFLIA to QF_AX. These benchmarks do not use uninterpreted functions or arithmetic in any meaningful way. The only change needed was to change the sorts from Int to Index/Element in order to fit within the QF_AX logic. Fixed a typo in QF_AUFBV: brummaryerbiere -> brummayerbiere.
May 21, 2008
An additional 415 benchmarks have been added to QF_BV in subdirectories uclid/catchconv (the 1 existing benchmark was moved here) and uclid/tcas.
May 20, 2008
A total of 66 new benchmarks have been added to QF_BV: 65 in brummayerbiere2 and 1 in uclid.
Minor fixes have been made in QF_UF/eq_diamond and QF_BV/brummayerbiere.
The UFNIA benchmarks have been added as "pending".
May 1, 2008
A total of 935 new benchmarks have been added.
QF_AUFBV : 293 in brummayerbiere;
QF_BV : 13 in brummayerbiere;
QF_IDL : 280 in schedulingIDL;
QF_LIA : 294 in rings;
QF_LRA : 42 in miplib;
QF_UFIDL : 13 in bcnscheduling.
April 14, 2008
A total of 4731 new benchmarks have been added.
AUFLIA : 32 in sexpr;
AUFLIRA : 198 in peter;
QF_IDL : 248 in parity;
QF_LIA : 2780 in nec-smt;
QF_UF : 100 in eq_diamond;
QF_UFIDL : 19 in mathsat;
QF_UFLIA : 454 in mathsat.
A new category of benchmarks added.
QF_UFLRA : 900 in mathsat.
February 20, 2008
All benchmarks have been updated to the version used in SMT COMP 2007.
June 19, 2007
Rebuilt the AUFLIA tar file.
June 18, 2007
The logic field for the check benchmarks has been updated to always match the division in which the benchmark appears. Additionally, the status and difficulty fields have been updated in some of the benchmarks in QF_BV/tacas07.
June 14, 2007
A minor problem with the QF_BV/spear benchmarks has been fixed.
June 12, 2007
The new bitvector theories and logics have been posted. Also, a total of 2011 new benchmarks have been added to QF_BV and 8168 new benchmakrs have been added to QF_AUFBV. Some of these have been retranslated from QF_UFBV 32. The rest are from various sources and make use of the new theories and logics.
May 17, 2007
A set of sample benchmarks have been added to QF_BV and QF_AUFBV.
May 08, 2007
A total of 3603 new benchmarks have been added to the set of AUFLIA benchmarks. These are translations of the boogie benchmarks (see http://research.microsoft.com/specsharp/) and an alternative and more complete translation of the simplify benchmarks (in subdirectory simplify2). These were translated by Michal Moskal.
May 1, 2007
A total of 1325 new benchmarks have been added to the set of AUFLIRAbenchmarks. These are translations of the Caduceus benchmarks provided by Claude Marche using the Why verifiction tool. See http://proval.lri.fr/why-benchmarks.
Movember 20, 2006
A total of 6404 new benchmarks have been added to the set of QF_UF benchmarks. These were provided by Volker Sorge and are based on classification of quasi-groups.
November 19, 2006
Most of the RTCL benchmarks were moved from QF_LIA to QF_UFIDL because they are a better fit for difference logic than linear arithmetic.
November 19, 2006
Some slight modifications were made to a number of the other QF_UFIDL benchmarks to eliminate the use of constructs that technically are not allowed by this logic.
September 1, 2006
This web site has now a new url: www.SMT-LIB.org .
August 5, 2006
A new version of the SMT-LIB format has been released. Notable changes are the possibility of overloading function and predicate symbols, and the addition of indexed identifiers (see the document).
July 24, 2006
A new version of the benchmarks has been released. Some benchmarks have been reclassified, and several more have been added for both new and old logics.
May 11, 2006
A theory of bit vectors with size up to 32 bits and a related logic have been added. The logic will be a division in the next SMT-COMP.
17/04/, 2006
The SMT-LIB discussion list has moved to a new server.
June 28, 2005
A new version of the benchmarks has been released. Some benchmarks have been reclassified, others have been retranslated because they were in an incorrect format. A few more have been added.
April 8, 2005
The first set of benchmarks in SMT-LIB format has been added to the Benchmarks section!
April 8, 2005
An initial set of SMT-LIB (sub)logic specifications has been released, in the Logics section.
April 8, 2005
An initial set of SMT-LIB theory specifications has been released, in the Theories section.
March 18, 2005
Version 1.1 of the SMT-LIB standard has been posted, in the Documents section.
October 18, 2004
Added link to SMT-COMP'05 in the SMT-COMP section.
September 5, 2004
We now have a section of SMT-COMP, the SMT solver competition.
July 27, 2004
Updated section on discussion list.
July 27, 2004
A new section on the SMT-LIB system competition has been added.
July 26, 2004
A couple of sample declarations of theories in SMT-LIB format, Arrays-1 and Reals-1, have been posted in the Documents section.
July 26, 2004
Version 1.0 of the SMT-LIB standard has been published! Check out the Documents section of this site.
July 25, 2004
The list of SMT solvers in the Solvers section has been updated.
July 24, 2004
News page created. Check this page for news on the SMT-LIB initiative and for updates on this website.