Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

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.

Logic Benchmarks eligible for SMT-COMP
ABVFP 1
ALIA 42
AUFBVDTLIA 1709 (39 excluded1)
AUFDTLIA 728
AUFLIA 4
AUFLIRA 20011
AUFNIRA 1480
BV 5151
BVFP 24
FP 61
LIA 388
LRA 2419
NIA 14
NRA 3811 (2 excluded2)
QF_ABV 15061
QF_ABVFP 18129
QF_ALIA 139
QF_ANIA 8
QF_AUFBV 31
QF_AUFLIA 1009
QF_AUFNIA 17
QF_AX 551
QF_BV 40043
QF_BVFP 17215
QF_DT 8000
QF_FP 40302
QF_IDL 2193
QF_LIA 6141
QF_LIRA 7
QF_LRA 1649
QF_NIA 23876
QF_NIRA 3
QF_NRA 11354
QF_RDL 255
QF_UF 6650
QF_UFBV 31
QF_UFIDL 428
QF_UFLIA 583
QF_UFLRA 1284
QF_UFNIA 7
QF_UFNRA 36
UF 7562 (524 excluded1)
UFBV 200
UFDT 4535 (541 excluded1)
UFDTLIA 303
UFIDL 68
UFLIA 10137
UFLRA 15
UFNIA 3308
Total 256973 (1106 excluded)

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.

Logic Benchmarks eligible for SMT-COMP Benchmarks with unknown status3 Benchmarks in SMT-LIB
ABVFP4 0 4 4
ALIA 24 0 24
ANIA 3 0 3
AUFNIRA4 0 165 165
BV4 0 18 18
BVFP4 0 10 10
LIA 6 0 6
LRA4 0 (5 excluded5) 0 5
QF_ABVFP4 0 9 9
QF_ALIA 44 0 44
QF_ANIA 5 0 5
QF_AUFLIA 72 0 72
QF_BV 18 13 31
QF_BVFP 2 63 65
QF_FP 2 1 3
QF_LIA 68 (1 excluded6) 0 69
QF_LRA 10 0 10
QF_NIA 10 0 10
QF_UFLIA 780 0 780
QF_UFLRA 3056 2 3058
QF_UFNIA 1 0 1
UFLRA 1870 0 1870
Total 5971 (6 excluded) 285 6262

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.

Logic Benchmarks eligible for the unsat-core track All main track benchmarks
ABVFP7 0 1
ALIA 41 42
AUFBVDTLIA7 0 (25 excluded) 1709
AUFDTLIA7 0 728
AUFLIA 3 4
AUFLIRA 19771 20011
AUFNIRA 1050 1480
BV 94 5151
BVFP7 0 24
FP7 0 61
LIA 233 388
LRA 1106 2419
NIA 4 14
NRA 3801 3813
QF_ABV 4673 15061
QF_ABVFP 3934 18129
QF_ALIA 80 139
QF_ANIA 8 8
QF_AUFBV 25 31
QF_AUFLIA 516 1009
QF_AUFNIA 12 17
QF_AX 279 551
QF_BV 23732 40043
QF_BVFP 3174 17215
QF_DT7 0 8000
QF_FP 20028 40302
QF_IDL 816 2193
QF_LIA 2844 6141
QF_LIRA 5 7
QF_LRA 671 1649
QF_NIA 3130 23876
QF_NIRA 2 3
QF_NRA 5296 11354
QF_RDL 113 255
QF_UF 4101 6650
QF_UFBV 31 31
QF_UFIDL 322 428
QF_UFLIA 183 583
QF_UFLRA 511 1284
QF_UFNIA 7 7
QF_UFNRA 11 36
UF 3316 7562
UFBV 97 200
UFDT7 0 (430 excluded) 4535
UFDTLIA7 0 303
UFIDL 57 68
UFLIA 7714 10137
UFLRA 10 15
UFNIA 2432 3308
Total 114233 (455 excluded) 256973

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.

Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Last modified: Tue 12 Jun 2018 12:25 UTC
Valid XHTML 1.0 Valid CSS!