Benchmarks

The SMT-LIB benchmark repository is now hosted on the SMT-LIB git-lab service service. 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.

Non-incremental benchmarks

ABVFP, ALIA, AUFBVDTLIA, AUFDTLIA, AUFLIA, AUFLIRA, 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_ABVFP, QF_ALIA, QF_ANIA, QF_AUFLIA, QF_BV, QF_BVFP, QF_FP, QF_LIA, QF_LRA, QF_NIA, 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.