[SMT-COMP] SMT-LIB release
Clark Barrett
barrett at cs.stanford.edu
Wed May 8 21:59:47 EDT 2019
A new release of the SMT-LIB benchmark library is now available on the
GitLab server. It will be on StarExec soon (StarExec release has been
delayed by a StarExec upload bug).
For this release, we have:
* Added 49,005 new benchmarks in new logics:
o non-incremental:
QF_BVFPLRA (1), QF_FPLRA (13), QF_S (1976), QF_SLIA (46,350),
UFDTNIA (1)
o incremental:
QF_AUFBVLIA (441), QF_AUFBVNIA (44), QF_UFBVLIA (179)
* Added 17,890 new benchmarks in existing logics:
o non-incremental:
FP (2,415), QF_ABV (17), QF_AUFBV (25), QF_BV (1594),
QF_UFBV (10), QF_UFNIA (471), UFDTLIA (24), UFNIA (10,105)
o incremental:
QF_ABV (1,257), QF_ABVFP (60), QF_AUFBV (21), QF_BV (1,771),
QF_BVFP (117), QF_UFBV (3)
* Updated statuses of 3039 previously unknown non-incremental
benchmarks (based on the results from 2 or more solvers from
SMT-COMP'18)
* Updated 79255 statuses of previously unknown incremental check-sat
calls (based on the results from 2 or more solvers from
SMT-COMP'18)
* Removed duplicate benchmarks
* Unified Sage2 and QF_BV benchmark repositories (non-incremental)
GitLab changes:
Benchmarks with a size >= 10M are now stored via git LFS. Please
refer to the repository's README on how to check out the repository.
Further, we unified the Sage2 and QF_BV repositories into one
repository. A fresh checkout is required since the git history of the
repository has been rewritten.
Thank you to the 11 submitters of the new benchmarks:
Alexandre Gonzalvez, Andres Nötzli, Andrew Reynolds, Bernhard Gleiss,
Clifford Wolf, Jie-Hong Roland Jiang, Makai Mann, Mathias Preiner,
Matthias Güdemann, Thomas Bunk, Yoni Zohar
More information about the SMT-COMP
mailing list