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

Clark Barrett barrett at cs.stanford.edu
Tue May 29 14:24:42 EDT 2018


A few minor updates have been made to SMT-LIB since the release on May 20.
These updates have been committed to GitLab and the affected benchmarks
have been updated on StarExec.  If you have cloned one of the affected
directories, you may want to grab a new copy.  All updates are to
non-incremental benchmarks and are detailed below:

1. Rename "reset" to "reset_" as reset is a reserved word in SMT-LIB.
Affected benchmarks:

UFNIA/vcc-havoc/baby.34.vamp_step.smt2
UFNIA/vcc-havoc/verisoft-baby.c.35.vamp_step.smt2
UFNIA/vcc-havoc/verisoft-vamp.c.35.vamp_step.smt2

2. Update incorrect statuses.  Affected benchmarks:

QF_UF/20170829-Rodin/smt2831655880469397696.smt2
QF_UF/20170829-Rodin/smt3232867547761696161.smt2
QF_UF/20170829-Rodin/smt3248576982810563470.smt2
QF_UF/20170829-Rodin/smt3508124013603727984.smt2
QF_UF/20170829-Rodin/smt3809952321495040629.smt2
QF_UF/20170829-Rodin/smt3910673230463462036.smt2
QF_UF/20170829-Rodin/smt4027072204816894856.smt2
QF_UF/20170829-Rodin/smt4241633917533372498.smt2
QF_UF/20170829-Rodin/smt4480564921249140261.smt2
QF_UF/20170829-Rodin/smt6109211130895037835.smt2
QF_UF/20170829-Rodin/smt6377531776677660648.smt2
QF_UF/20170829-Rodin/smt834303034702425531.smt2
QF_UF/20170829-Rodin/smt862177804180920815.smt2
QF_UF/20170829-Rodin/smt8855268942650190404.smt2

3. Remove unused "declare-sort".  Affected benchmark:

QF_FP/griggio/fmcad12/f23.smt2

4. Remove benchmarks using uninterpreted functions from QF_FP.  Affected
benchmarks:

QF_FP/schanda/spark/O402-020_1.smt2
QF_FP/schanda/spark/O402-020_2.smt2


More information about the SMT-COMP mailing list