SMT-LIB Benchmarks

Benchmarks

You can browse the available benchmarks, indexed by their respective logic.

New benchmarks: July 2, 2009

The following is an update of the new benchmarks for 2009. It includes a number of fixes and repairs to the previously posted benchmarks as well as several new sets of benchmarks. The benchmarks previously posted as AUFLIRA have been recategorized as LRA (since they do not involve arrays, uninterpreted functions, or integers). Similarly, one set of benchmarks from AUFLIA has been moved to UFNIA. Note that only the first tarball for QF_BV has changed (i.e. QF_BV0). The other QF_BV tarballs are no different from the June 3 release.

AUFLIA tarball
LRA tarball
QF_AUFBV tarball
QF_BV tarballs: 0 1 2 3 4 5 6 7 8
QF_LIA tarball
QF_NIA tarball
QF_UFNRA tarball
UFNIA tarball

New benchmarks: June 3, 2009

The following benchmarks are new for 2009. They will be merged with the existing SMT-LIB benchmarks in the near future.

AUFLIA tarball
AUFLIRA tarball
QF_AUFBV tarball
QF_BV tarballs: 0 1 2 3 4 5 6 7 8
QF_LIA tarball
QF_NIA tarball

Current version: June 1, 2008

AUFLIA benchmarks tarball
AUFLIRA benchmarks tarball
AUFNIRA benchmarks tarball
QF_AUFBV benchmarks tarball
QF_AUFLIA benchmarks tarball
QF_AX benchmarks tarball
QF_BV benchmarks tarball
QF_IDL benchmarks tarball
QF_LIA benchmarks tarball
QF_LRA benchmarks tarball
QF_RDL benchmarks tarball
QF_UF benchmarks tarball
QF_UFIDL benchmarks tarball
QF_UFLIA benchmarks tarball
QF_UFLRA benchmarks tarball
QF_UFBV[32] benchmarks tarball

Preview of new library interface

Demo