[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