[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