| 14/06/11 | 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). |
| 11/06/11 | The declarations for the following logics have been added in the Logics section: QF_NRA, QF_UFBV, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFLRA, UFNIA.smt2. A couple of logics them are new. The rest had had benchmarks in the library for a while but their declaration was missing. |
| 03/06/11 | 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). |
| 03/06/11 | Added a note to the declaration of QF_UFIDL. |
| 03/06/11 | Extended the definition of linear term in the :extension attribute of QF_AUFLIA. |
| 18/01/11 | Links to a set of Java utilities for SMT-LIB 2 scripts has been added in the Utilities section. |
| 18/01/11 | A tutorial, by D. Cok, on the SMT-LIB 2 format has been added in the Documents section. |
| 21/12/10 | 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. |
| 01/09/10 | Section Utilities has been revamped, with the addition of two parsers for SMT-LIB 2. |
| 28/08/10 | 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. |
| 04/05/10 | 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. |
| 01/05/10 | 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. |
| 30/03/10 | 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. |
| 10/02/10 | An updated, almost final draft of the Version 2.0 document is now available in the Documents section. |
| 01/02/10 | A draft of the coming Version 2.0 of the SMT-LIB format is now available in the Documents section. |
| 18/08/09 | A link to Robert Brummayer's SMT debugging utilities has been added in the Utilities section. |
| 04/07/09 | The logic LRA, for (quantified) formulas in linear real arithmetic, has been added. |
| 02/07/09 | 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. |
| 25/06/09 |
Three new logics have been added, all having to do with non-linear arithmetic: QF_NIA, QF_UFNRA and UFNIA.
|
| 03/06/09 |
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. |
| 05/06/08 | QF_BV/spear benchmarks were missing the ":formula" attribute. ":formula true" has been added to all of these benchmarks. |
| 01/06/08 | 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. |
| 21/05/08 |
An additional 415 benchmarks have been added to QF_BV in subdirectories uclid/catchconv (the 1 existing benchmark was moved here) and uclid/tcas. |
| 20/05/08 |
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". |
| 01/05/08 |
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 |
| 14/04/08 |
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 |
| 20/02/08 | All benchmarks have been updated to the version used in SMT COMP 2007. |
| 19/06/07 | Rebuilt the AUFLIA tar file. |
| 18/06/07 | 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. |
| 14/06/07 | A minor problem with the QF_BV/spear benchmarks has been fixed. |
| 12/06/07 | 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_UFBV32. The rest are from various sources and make use of the new theories and logics. |
| 17/05/07 | A set of sample benchmarks have been added to QF_BV and QF_AUFBV. |
| 08/05/07 | 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. |
| 01/05/07 | A total of 1325 new benchmarks have been added to the set of AUFLIRA benchmarks. These are translations of the Caduceus benchmarks provided by Claude Marche using the Why verifiction tool. See http://proval.lri.fr/why-benchmarks. |
| 20/11/06 | 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. |
| 19/11/06 | 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. |
| 19/11/06 | 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. |
| 01/09/06 | This web site has now a new url: www.SMT-LIB.org . |
| 05/08/06 | 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). |
| 24/07/06 | 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. |
| 11/05/06 | 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/06 | The SMT-LIB discussion list has moved to a new server. |
| 28/06/05 | 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. |
| 08/04/05 | The first set of benchmarks in SMT-LIB format has been added to the Benchmarks section! |
| 08/04/05 | An initial set of SMT-LIB (sub)logic specifications has been released, in the Logics section. |
| 08/04/05 | An initial set of SMT-LIB theory specifications has been released, in the Theories section. |
| 18/03/05 | Version 1.1 of the SMT-LIB standard has been posted, in the Documents section. |
| 18/10/04 | Added link to SMT-COMP'05 in the SMT-COMP section. |
| 05/09/04 | We now have a section of SMT-COMP, the SMT solver competition. |
| 27/07/04 | Updated section on discussion list. |
| 27/07/04 | A new section on the SMT-LIB system competition has been added. |
| 26/07/04 | A couple of sample declarations of theories in SMT-LIB format, Arrays-1 and Reals-1, have been posted in the Documents section. |
| 26/07/04 | Version 1.0 of the SMT-LIB standard has been published! Check out the Documents section of this site. |
| 25/07/04 | The list of SMT solvers in the Solvers section has been updated. |
| 24/07/04 | News page created. Check this page for news on the SMT-LIB initiative and for updates on this website. |