Benchmarks

The SMT-LIB benchmark repository is now hosted on the SMT-LIB GitLab server. Read access does not require an account. The releases are stored in the master branch. The current release is at the head.

The following links point to the repositories for individual logics.
Note: Some of the logics listed below have not been entered in the Logics section yet.

Non-incremental benchmarks

ABVFP, ALIA, AUFBVDTLIA, AUFDTLIA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, BV, BVFP, FP, LIA, LRA, NIA, NRA, QF_ABV, QF_ABVFP, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFLIA, QF_AUFNIA, QF_AX, QF_BV, QF_BVFP, QF_DT, QF_FP, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_NIA, QF_NIRA, QF_NRA, QF_RDL, QF_UF, QF_UFBV, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFDT, UFDTLIA, UFIDL, UFLIA, UFLRA, UFNIA, Sage2

Incremental benchmarks

ABVFP, ALIA, ANIA, AUFNIRA, BV, BVFP, LIA, LRA, QF_ABV, QF_ABVFP, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFLIA, QF_BV, QF_BVFP, QF_FP, QF_LIA, QF_LRA, QF_NIA, QF_UF, QF_UFBV, QF_UFLIA, QF_UFLRA, QF_UFNIA, UFLRA,

Instructions on how to clone each repository are available in the repository's space. You can also download this bash script, uncomment the lines relevant to the logic/repositories you want to clone, and run it.

Zip archives

Zip archives containing all sections of the latest release of the repository are also available here.

StarExec

The latest release of the benchmark library is also available on StarExec.

Submitting Benchmarks

For details on how to submit benchmarks to SMT-LIB, please refer to the README file in the benchmarks-pending repository on the SMT-LIB GitLab.