Benchmarks
We intend to use benchmarks from the current
SMT-LIB release
(June 19, 2007) in the following divisions.
The benchmark files themselves will be unmodified (except for scrambling)
for the competition. However, for benchmark selection, please note:
- We have recomputed difficulties based on SMT-COMP'06 solvers.
In the new divisions QF_BV and QF_AUFBV, difficulties are estimated
rather than calculated. The new difficulties are not encoded in the
above files, but are available in a file on the
benchmark selection page.
Statistics on the difficulty recalculation are available.
- In the above SMT-LIB release of QF_UFIDL, benchmark categories are
omitted for 44 UCLID benchmarks. These are in fact industrial benchmarks and
for benchmark selection will be considered so.
- For benchmarks with “unknown” status as of the
June 19, 2007 release of SMT-LIB, we have decided that they will remain
unknown and will not be included in competition this year.
- Some benchmarks with “sat” or “unsat”
status have recently come under suspicion; in particular, all AUFLIA
benchmarks in the “boogie” family with an encoded status of
“sat” are being left out of SMT-COMP'07.
Last modified: Tue 17 Feb 2015 14:58 UTC
