Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Benchmarks

SMT-COMP 2016 will use a subset of the benchmarks available within the 2016-05-23 release of SMT-LIB, as described in the competition rules. Specifically, 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) will not be used.

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2016-05-23 on StarExec.

Main Track

Logic Benchmarks eligible for SMT-COMP Benchmarks with unknown status Benchmarks in SMT-LIB
ALIA 42 0 42
AUFLIA 4 0 4
AUFLIRA 19849 165 20014
AUFNIRA 1050 445 1495
BV 85 106 191
LIA 201 189 390
LRA 339 282 621
NIA 9 5 14
NRA 3788 25 3813
QF_ABV 14720 (197 excluded1) 174 15091
QF_ALIA 139 0 139
QF_ANIA 8 0 8
QF_AUFBV 37 0 37
QF_AUFLIA 1009 0 1009
QF_AUFNIA 21 0 21
QF_AX 551 0 551
QF_BV 26414 (6062 excluded1) 17504 49980
QF_BVFP 7 (1 excluded1) 0 8
QF_FP 34413 (5706 excluded1) 215 40334
QF_IDL 2094 104 2198
QF_LIA 5839 302 6141
QF_LIRA 6 1 7
QF_LRA 1626 56 1682
QF_NIA 8593 927 9520
QF_NIRA 2 1 3
QF_NRA 10245 1356 11601
QF_RDL 220 35 255
QF_UF 6649 1 6650
QF_UFBV 31 0 31
QF_UFIDL 441 0 441
QF_UFLIA 598 0 598
QF_UFLRA 1627 3 1630
QF_UFNIA 7 0 7
QF_UFNRA 34 9 43
UF 2839 2909 5748
UFBV 71 129 200
UFIDL 68 12 80
UFLIA 8404 3736 12140
UFLRA 25 0 25
UFNIA 2319 1033 3352
Total 154424 (11966 excluded1) 29724 196114

1. Excluded because they contain partial or underspecified operations (e.g., bit-vector division, fp.min).

Application Track

Logic Benchmarks eligible for SMT-COMP Benchmarks with unknown status2 Benchmarks in SMT-LIB
ALIA 24 0 24
ANIA 3 0 3
AUFNIRA3 0 165 165
LIA 6 0 6
QF_ALIA 44 0 44
QF_ANIA 5 0 5
QF_AUFLIA 72 0 72
QF_BV 18 0 18
QF_LIA 69 (1 excluded4) 0 70
QF_LRA 10 0 10
QF_NIA 10 0 10
QF_UFLIA 905 0 905
QF_UFLRA 3331 2 3333
QF_UFNIA 1 0 1
UFLRA 5358 0 5358
Total 9856 (1 excluded4) 167 10024

2. 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.
3. As there are no eligible benchmarks in SMT-LIB, AUFNIRA is not actually an application track division in SMT-COMP 2016.
4. 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). The unsat-core track is experimental in 2016.

Logic Benchmarks eligible for the unsat-core track All main track benchmarks
ALIA 41 42
AUFLIA 3 4
AUFLIRA 19749 19849
AUFNIRA 1046 1050
BV 56 85
LIA 191 201
LRA 319 339
NIA 3 9
NRA 3788 3788
QF_ABV 4644 14720
QF_ALIA 80 139
QF_ANIA 8 8
QF_AUFBV 31 37
QF_AUFLIA 516 1009
QF_AUFNIA 15 21
QF_AX 279 551
QF_BV 17172 26414
QF_BVFP 6 7
QF_FP 17213 34413
QF_IDL 816 2094
QF_LIA 2840 5839
QF_LIRA 5 6
QF_LRA 633 1626
QF_NIA 316 8593
QF_NIRA 2 2
QF_NRA 4948 10245
QF_RDL 113 220
QF_UF 4100 6649
QF_UFBV 31 31
QF_UFIDL 335 441
QF_UFLIA 195 598
QF_UFLRA 853 1627
QF_UFNIA 7 7
QF_UFNRA 18 34
UF 2039 2839
UFBV 53 71
UFIDL 62 68
UFLIA 8377 8404
UFLRA 20 25
UFNIA 2318 2319
Total 93241 154424
Home Rules Benchmarks Tools Specs Participants Results SMT-LIB Previous

Last modified: Mon 19 Jun 2017 23:00 UTC
Valid XHTML 1.0 Valid CSS!