[SMT-LIB] New version of SMT-LIB benchmarks available

Morgan Deters mdeters at cs.nyu.edu
Tue May 4 18:21:11 EDT 2010


SMT-LIB and SMT-COMP community members,

A new version of the SMT-LIB benchmark library, conforming to version
2.0 of the SMT-LIB standard, is now available. These benchmarks can be
accessed through the SMT-LIB website at

  http://www.smt-lib.org

Through this interface, the benchmark library may be downloaded in
whole or in part.  The benchmarks carry the file extension ".smt2" to
more easily distinguish them from benchmarks from the previous SMT-LIB
version, 1.2.

All current benchmarks belong to a restricted subset of SMT-LIB 2.0,
as described in the 2010 SMT-COMP official rules, to allow an easier
upgrade path for competition solvers this year.

In working on this release, we discovered a number of duplicate
benchmarks, which have been removed from this release.  The current
benchmark count for SMT-LIB is 85219.  Difficulties have already been
assessed for most of these benchmarks as described in the SMT-COMP
2010 official rules.

SMT-LIB version 2.0 information, including the full specification as
well as theories and logics, can be found at:

  http://www.smt-lib.org

Sincerely,

Morgan Deters
(also for Cesare Tinelli, Clark Barrett, Aaron Stump, and Albert Oliveras)


More information about the SMT-LIB mailing list