Benchmarks

SMT-COMP 2017 will use a large subset of the benchmarks available within the 2017-06-05 release of SMT-LIB, as described in the competition rules.

Note that—unlike in 2016—benchmarks with unknown status, bit-vector benchmarks that contain partial operations (i.e., bvudiv, bvurem, bvsdiv, bvsrem or bvsmod), and floating-point benchmarks that contain underspecified operations (i.e., fp.min, fp.max, fp.to_ubv, fp.to_sbv or fp.to_real) are generally eligible for the competition. If your solver is competing in divisions that feature these operations, please ensure that it implements the correct semantics for them.

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2017-06-05 on StarExec.

Main Track

All non-incremental SMT-LIB benchmarks (except those excluded because they were syntactically invalid) are eligible for the main track. In total, there are 49 main track divisions. Divisions containing datatypes (DT) are experimental in 2017.

1. These benchmarks were excluded because they contained sorts or operations that are unavailable in the respective logic. Thanks to Andres Nötzli who reported the issue.
2. Benchmarks non-incremental/NRA/keymaera/ETCS-essentials-live-range2.proof-node1046.smt2 and non-incremental/NRA/keymaera/reactivity-lemma-node2938.smt2 were excluded because they contained possibly incorrect :status information.

Application Track

In total, there are 16 application track divisions.

3. For the application track, a benchmark is ineligible if its first check-sat command has unknown status. Otherwise, (some non-empty prefix of) the benchmark is eligible.
4. As there are no eligible benchmarks in SMT-LIB, ABVFP, AUFNIRA, BV, BVFP, LRA and QF_ABVFP are not actually application track divisions in SMT-COMP 2017.
5. The five benchmarks in incremental/LRA/20160930-Kopczynski-LOIS/ were excluded because they did not contain :status information.
6. Benchmark incremental/QF_LIA/UltimateBuchiAutomizer/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c.smt2 was excluded because it contained incorrect :status information.

Unsat-Core Track

All unsatisfiable main track benchmarks are eligible for the unsat-core track (with minor modifications, e.g., named assertions). Divisions containing datatypes (DT) were excluded from the unsat-core track due to lacking tool support. In total, there are 41 unsat-core track divisions.

7. As there are no eligible benchmarks in SMT-LIB, ABVFP, AUFBVDTLIA, AUFDTLIA, BVFP, FP, QF_DT, UFDT and UFDTLIA are not actually unsat-core track divisions in SMT-COMP 2017.

Last modified: Tue 12 Jun 2018 12:25 UTC