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

ALIA, AUFLIA, AUFLIRA, AUFNIRA, BV, LIA, LRA, NIA, NRA, QF_ABV, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFLIA, QF_AUFNIA, QF_AX, QF_BV, QF_BVFP, 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, UFIDL, UFLIA, UFLRA, UFNIA, Sage2

Incremental benchmarks

ALIA, ANIA, AUFNIRA, LIA, QF_ALIA, QF_ANIA, QF_AUFLIA, QF_BV, QF_LIA, QF_LRA, QF_NIA, QF_UFLIA, QF_UFLRA, QF_UFNIA, UFLRA

Instructions on how to clone each repository is 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.