[SMT-COMP] New official release of SMT-LIB benchmark library

Cesare Tinelli cesare-tinelli at uiowa.edu
Thu Jun 8 03:17:43 EDT 2017


[reposted from smt-lib at googlegroups.com]

A new release of the SMT-LIB benchmark library (2017-06-05) is now
available, both on the GitLab
<https://clc-gitlab.cs.uiowa.edu:2443/explore/groups> server and on StarExec
<https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=234826>.
For this release we have

   - Fixed minor errors in formatting
   - Removed duplicate benchmarks
   - Updated statuses of 6,492 previously unknown benchmarks (based on the
   results from 2 or more solvers from SMT-COMP'16)
   - Added new benchmarks in new logics:
      - non-incremental: ABVFP, AUFBVDTLIA, AUFDTLIA, BVFP, FP, QF_ABVFP,
      QF_DT, UFDT, UFDTLIA
      - incremental: ABVFP, BV, BVFP, LRA, QF_ABVFP, QF_BVFP, QF_FP
   - Added new benchmarks in existing logics:
      - non-incremental: BV, LRA, QF_BV, QF_BVFP, QF_FP, QF_LRA, QF_NIA,
      QF_NRA, UF
      - incremental: QF_BV

Starting with this release, benchmarks will be distributed under the Creative
Commons Attribution 4.0 International License
<https://creativecommons.org/licenses/by/4.0/>.

For details on the changes to SMT-LIB, please check the git logs at
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks and
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc

The SMT-LIB coordinators


PS: In the new logics, FP stands for Floating Point and DT for data types.
(Yes, logic names are gotten totally out of hand. We plan to address this
problem in Version 3 of the standard.)


More information about the SMT-COMP mailing list