[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