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