We intend to use benchmarks from the current
(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: Fri 22 Feb 2008 09:28 CST