SMT-LIB 2024 Release on Zenodo

6 views
Skip to first unread message

Mathias Preiner

unread,
Apr 24, 2024, 4:26:17 PMApr 24
to smt...@googlegroups.com, smt-an...@googlegroups.com, smt-...@cs.nyu.edu
Dear all,

The 2024 SMT-LIB release is now available on Zenodo.

You can access the new release here:

- incremental: https://zenodo.org/records/11061220
- non-incremental: https://zenodo.org/records/11061097

For this year's release we received 4419 non-incremental and 1046
incremental benchmarks in the following logics:

incremental:
QF_BVLRA 1046 (new logic)

non-incremental:
ANIA 22
AUFBV 1
NIA 6
UFNIRA 266 (new logic)
QF_ANIA 2
QF_AUFBV 8
QF_DT 500
QF_LIA 80
QF_NRA 20
QF_S 17
QF_SLIA 3287
QF_UFDTNIA 4
QF_UFNIA 206

We also received 2308 benchmarks that require some standardization work
on the SMT-LIB language and therefore did not make it into this year's
release. However, we hope that we can include these benchmarks in next
year's release.

Many thanks to the contributors for submitting benchmarks:

Antti Hyvärinen, Aron Spang, Arthur Sanin, Chad E. Brown,
Christoph Beierle, Denghang Hu, Federico Mora, Francesco Pontiggia,
Jim Grundy, Martin von Berg, Mate Soos, Matthias Heizmann,
Michele Chiari, Mikoláš Janota, Mirek Olšák, Nathan Wetzler,
Oliver Markgraf, Philipp Rummer, Rod Chapman, Rongcheng Li,
Shilpi Goel, Tobias Winkler, Tomas Kolarik, Yan Peng, Zhilin Wu

Also many thanks to Hans-Joerg Schurr for managing the GitHub submission
process and helping out with this release!

Cheers,
Mathias
OpenPGP_0xA4AF2BDE778B2463.asc
OpenPGP_signature.asc

Mathias Preiner

unread,
May 13, 2024, 6:09:26 PMMay 13
to smt...@googlegroups.com, smt-an...@googlegroups.com, smt-...@cs.nyu.edu
Dear all,

We uploaded a new release for the incremental benchmarks to Zenodo. The
previous upload had some issues in the QF_UF and QF_LRA logics, which
are now fixed. You can find the newest version on Zenodo here:
https://zenodo.org/records/11186591

2024.05.13 Changes
------------------
* Changed logic string for incremental/QF_UF/20190906-CLEARSY benchmarks
from UF to QF_UF.
* Files in incremental/QF_LRA only contained the git LFS metadata
instead of the benchmarks.

Cheers,
Mathias
Reply all
Reply to author
Forward
0 new messages