[SMT-COMP] SMT-LIB release
Clark Barrett
barrett at cs.stanford.edu
Fri May 10 19:48:17 EDT 2019
The new SMT-LIB release is now also available on StarExec (2019-05-06).
On Wed, May 8, 2019 at 6:59 PM Clark Barrett <barrett at cs.stanford.edu>
wrote:
> 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