Dear all,
The 2025 SMT-LIB release is now available on Zenodo.
You can access the new release here:
- incremental:
https://zenodo.org/records/15493096
- non-incremental:
https://zenodo.org/records/15493090
For this year's release we received 11843 non-incremental and 375
incremental benchmarks in the following logics:
incremental:
QF_SNIA 2 (new logic)
QF_NIA 107
QF_S 245 (new logic)
QF_BV 21
non-incremental:
UFDTLIA 1255
AUFBVFPDTNIRA 117 (new logic)
UFBVDTLIA 24 (new logic)
QF_NIA 9
QF_SLIA 16
QF_S 3232
UFNIA 68
QF_UFBV 1029
UFBVFPDTNIRA 89 (new logic)
UFBVDTNIRA 1259 (new logic)
AUFBVDTNIRA 2916
AUFBVDTNIA 544
LIA 120
UFDTNIA 1008
UFBVDTNIA 157 (new logic)
This release also includes benchmarks that use features introduced in
SMT-LIB version 2.7. These benchmarks have an `smt-lib-version` header
of 2.7.
Many thanks to the contributors for submitting benchmarks:
AdaCore
Amar Shah
Anthony W. Lin
Bohan Li
Certora
Daniel Stan
Hernan Ponce de Leon
Hongjian Jiang
Johannes Bauer
Lukáš Holík
Michal Hečko
Oliver Markgraf
Ondřej Lengál
Philipp Ruemmer
Rod Chapman
Shaoke Cui
Vojtěch Havlena
Yoni Zohar
Also many thanks to Hans-Joerg Schurr for managing the GitHub submission
process and helping out with this year's release!
Cheers,
Mathias