Benchmarks

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

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2021-05-26 on StarExec.

Single Query Track

In total there are 18 divisions in the Single Query Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	1620	LIA LRA NIA NRA	300 1003 17 300
Bitvec	970	BV	970
Equality+LinearArith	17873	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	19 147 6069 1638 1683 277 5165 20 2848 7
Equality+MachineArith	2852	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVFP AUFFPDTLIRA UFBV UFBVFP UFBVLIA UFFPDTLIRA UFFPDTNIRA	169 30 75 761 845 1 57 153 143 2 208 387 21
Equality+NonLinearArith	7816	AUFDTNIRA AUFFPDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	300 13 3 300 1 921 6278
Equality	4409	UF UFDT	2857 1552
FPArith	1805	BVFP BVFPLRA FP FPLRA	229 185 1364 27
QF_Bitvec	8828	QF_BV	8828
QF_Equality+Bitvec	3221	QF_ABV QF_AUFBV QF_UFBV	2880 41 300
QF_Equality+LinearArith	1961	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	116 558 146 300 300 541
QF_Equality+NonLinearArith	430	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	94 9 300 27
QF_Equality	4229	QF_AX QF_DT QF_UF QF_UFDT	300 204 3522 203
QF_FPArith	1710	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFPDTLIRA	619 25 1 484 72 300 55 154
QF_LinearIntArith	4456	QF_IDL QF_LIA QF_LIRA	1138 3311 7
QF_LinearRealArith	829	QF_LRA QF_RDL	582 247
QF_NonLinearIntArith	11683	QF_NIA QF_NIRA	11681 2
QF_NonLinearRealArith	2766	QF_NRA	2766
QF_Strings	23842	QF_S QF_SLIA QF_SNIA	807 23030 5
Total	101300

Incremental Track

In total there are 17 divisions in the Incremental Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	11	LIA LRA	6 5
Bitvec	18	BV	18
Equality+LinearArith	959	ALIA UFLRA	24 935
Equality+MachineArith	4	ABVFP	4
Equality+NonLinearArith	2342	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	3 165 139 2031 4
Equality	2033	UF	2033
FPArith	10	BVFP	10
QF_Bitvec	1294	QF_BV	1294
QF_Equality+Bitvec+Arith	523	QF_AUFBVLIA QF_AUFBVNIA QF_UFBVLIA	300 44 179
QF_Equality+Bitvec	1832	QF_ABV QF_AUFBV QF_UFBV	636 31 1165
QF_Equality+LinearArith	2031	QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA	44 72 386 1529
QF_Equality+NonLinearArith	512	QF_ANIA QF_UFNIA QF_UFNRA	5 506 1
QF_Equality	889	QF_UF	889
QF_FPArith	9686	QF_ABVFP QF_BVFP QF_FP QF_UFFP	9218 300 167 1
QF_LinearIntArith	69	QF_LIA	69
QF_LinearRealArith	10	QF_LRA	10
QF_NonLinearIntArith	10	QF_NIA	10
Total	22233

Unsat Core Track

In total there are 17 divisions in the Unsat Core Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	237	LIA NIA	235 2
Bitvec	300	BV	300
Equality+LinearArith	24477	AUFDTLIRA AUFLIA AUFLIRA UFDTLIRA UFIDL UFLIA UFLRA	5385 1245 9885 4060 30 3862 10
Equality+MachineArith	455	ABV AUFBVDTLIA AUFFPDTLIRA UFFPDTLIRA UFFPDTNIRA	2 20 131 300 2
Equality+NonLinearArith	2516	AUFDTNIRA AUFNIA AUFNIRA UFDTNIRA UFNIA	50 3 526 349 1588
Equality	2628	UF UFDT	1697 931
FPArith	1	BVFPLRA	1
QF_Bitvec	2868	QF_BV	2868
QF_Equality+Bitvec	2225	QF_ABV QF_AUFBV QF_UFBV	1865 34 326
QF_Equality+LinearArith	577	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	30 300 17 113 16 101
QF_Equality+NonLinearArith	210	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	8 12 179 11
QF_Equality	2463	QF_AX QF_DT QF_UF QF_UFDT	202 100 2061 100
QF_FPArith	13634	QF_ABVFP QF_BVFP QF_BVFPLRA QF_FP QF_UFFP QF_UFFPDTLIRA	1965 1586 46 10031 2 4
QF_LinearIntArith	381	QF_IDL QF_LIA QF_LIRA	100 276 5
QF_LinearRealArith	196	QF_LRA	196
QF_NonLinearIntArith	2053	QF_NIA QF_NIRA	2051 2
QF_NonLinearRealArith	243	QF_NRA	243
Total	55464

Model Validation Track

In total there are 6 divisions in the Model Validation Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
QF_Bitvec	7268	QF_BV	7268
QF_Equality+Bitvece	375	QF_UFBV	375
QF_Equality+LinearArithe	891	QF_UFIDL QF_UFLRA QF_UFLIA	206 385 300
QF_Equalitye	1571	QF_UF	1571
QF_LinearIntArith	2615	QF_IDL QF_LIA QF_LIRA	691 1923 1
QF_LinearRealArith	582	QF_RDL QF_LRA	109 473
Total	13302

Cloud Track

In total there are 14 divisions in the Cloud Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	23	LIA LRA NIA NRA	4 16 1 2
Bitvec	16	BV	16
Equality+LinearArith	107	AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	16 16 16 16 16 9 16 2
Equality+MachineArith	16	UFBV	16
Equality+NonLinearArith	67	AUFDTNIRA AUFNIA AUFNIRA UFDTNIRA UFNIA	16 3 16 16 16
Equality	32	UF UFDT	16 16
QF_Bitvec	16	QF_BV	16
QF_Equality+Bitvec	16	QF_ABV	16
QF_Equality+NonLinearArith	6	QF_UFNRA	6
QF_FPArith	19	QF_BVFP QF_FP	3 16
QF_LinearIntArith	32	QF_IDL QF_LIA	16 16
QF_LinearRealArith	32	QF_LRA QF_RDL	16 16
QF_NonLinearIntArith	16	QF_NIA	16
QF_NonLinearRealArith	16	QF_NRA	16
Total	414

Parallel Track

In total there are 14 divisions in the Parallel Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	24	LIA LRA NIA NRA	4 17 1 2
Bitvec	17	BV	17
Equality+LinearArith	113	AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	17 17 17 17 17 9 17 2
Equality+MachineArith	17	UFBV	17
Equality+NonLinearArith	71	AUFDTNIRA AUFNIA AUFNIRA UFDTNIRA UFNIA	17 3 17 17 17
Equality	34	UF UFDT	17 17
QF_Bitvec	17	QF_BV	17
QF_Equality+Bitvec	17	QF_ABV	17
QF_Equality+NonLinearArith	6	QF_UFNRA	6
QF_FPArith	20	QF_BVFP QF_FP	3 17
QF_LinearIntArith	34	QF_IDL QF_LIA	17 17
QF_LinearRealArith	17	QF_LRA	17
QF_NonLinearIntArith	17	QF_NIA	17
QF_NonLinearRealArith	17	QF_NRA	17
Total	421

n Non-competing.
e Experimental.