Benchmarks

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

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2022-05-20 on StarExec.

Single Query Track

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

Division	Division benchmarks	Logic	Logic benchmarks
Arith	1610	LIA LRA NIA NRA	300 1003 208 99
Bitvec	970	BV	970
Equality+LinearArith	13994	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	19 188 4185 1638 1683 277 3129 20 2848 7
Equality+MachineArith	3812	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	169 30 75 761 742 8 1062 57 159 143 2 208 396
Equality+NonLinearArith	9493	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	762 3 300 1 2149 6278
Equality	4407	UF UFDT	2857 1550
FPArith	1835	BVFP BVFPLRA FP FPLRA	205 209 1334 87
QF_Bitvec	8464	QF_BV	8464
QF_Datatypes	401	QF_DT QF_UFDT	201 200
QF_Equality+Bitvec	2168	QF_ABV QF_AUFBV QF_UFBV	1830 38 300
QF_Equality+LinearArith	1805	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	116 539 9 300 300 541
QF_Equality+NonLinearArith	387	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	102 9 249 27
QF_Equality	3793	QF_AX QF_UF	300 3493
QF_FPArith	1654	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFPDTNIRA	600 25 1 465 69 285 55 154
QF_LinearIntArith	7430	QF_IDL QF_LIA QF_LIRA	1204 6219 7
QF_LinearRealArith	825	QF_LRA QF_RDL	578 247
QF_NonLinearIntArith	12231	QF_NIA QF_NIRA	12229 2
QF_NonLinearRealArith	2908	QF_NRA	2908
QF_Strings	15758	QF_S QF_SLIA QF_SNIA	545 15143 70
Total	93945

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	ABVFPLRA	4
Equality+NonLinearArith	2342	ANIA AUFNIRA UFDTNIA UFNIA UFNRA	3 165 139 2031 4
Equality	2033	UF	2033
FPArith	10	BVFP BVFPLRA	1 9
QF_Bitvec	1295	QF_BV	1295
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	9752	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP	9214 7 300 63 166 1 1
QF_LinearIntArith	69	QF_LIA	69
QF_LinearRealArith	10	QF_LRA	10
QF_NonLinearIntArith	10	QF_NIA	10
Total	22300

Unsat Core Track

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

Division	Division benchmarks	Logic	Logic benchmarks
Arith	359	LIA NIA	227 132
Bitvec	362	BV	362
Equality+LinearArith	23260	AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	88 4977 1289 9888 202 2863 30 3913 10
Equality+MachineArith	1710	ABV ABVFP ABVFPLRA AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFFPDTNIRA UFFPDTNIRA	23 1 4 166 3 1062 132 319
Equality+NonLinearArith	6829	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	634 3 549 1 2012 3630
Equality	2938	UF UFDT	1784 1154
FPArith	21	BVFP BVFPLRA FPLRA	10 9 2
QF_Bitvec	2887	QF_BV	2887
QF_Datatypes	200	QF_DT QF_UFDT	100 100
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	246	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	27 12 196 11
QF_Equality	2263	QF_AX QF_UF	202 2061
QF_FPArith	13674	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_UFFP QF_UFFPDTNIRA	1971 5 1588 52 10052 2 4
QF_LinearIntArith	1108	QF_IDL QF_LIA QF_LIRA	100 1003 5
QF_LinearRealArith	204	QF_LRA	204
QF_NonLinearIntArith	2830	QF_NIA QF_NIRA	2828 2
QF_NonLinearRealArith	409	QF_NRA	409
QF_Strings	3352	QF_S QF_SLIA	172 3180
Total	65454

Model Validation Track

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

Division	Division benchmarks	Logic	Logic benchmarks
QF_Bitvec	7324	QF_BV	7324
QF_Equality+Bitvec	375	QF_UFBV	375
QF_Equality+LinearArith	891	QF_UFIDL QF_UFLIA QF_UFLRA	206 300 385
QF_Equality	1571	QF_UF	1571
QF_FPArithe	17301	QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA	7028 116 10106 51
QF_LinearIntArith	4940	QF_IDL QF_LIA QF_LIRA	743 4196 1
QF_LinearRealArith	625	QF_LRA QF_RDL	516 109
Total	33027

Proof Exhibition Track

In total there are 19 divisions in the Proof Exhibition Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	3119	LIA LRA NIA NRA	266 802 141 1910
Bitvec	2660	BV	2660
Equality+LinearArith	23392	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	41 88 4977 1296 9888 202 2916 57 3917 10
Equality+MachineArith	2197	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	23 1 4 321 171 3 1062 24 132 126 1 8 321
Equality+NonLinearArith	6829	AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	634 3 549 1 2012 3630
Equality	2938	UF UFDT	1784 1154
FPArith	1195	BVFP BVFPLRA FP FPLRA	14 9 1157 15
QF_Bitvec	13848	QF_BV	13848
QF_Datatypes	2361	QF_DT QF_UFDT	2261 100
QF_Equality+Bitvec	2725	QF_ABV QF_AUFBV QF_UFBV	2343 40 342
QF_Equality+LinearArith	1301	QF_ALIA QF_AUFLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	72 380 66 300 183 300
QF_Equality+NonLinearArith	246	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	27 12 196 11
QF_Equality	2459	QF_AX QF_UF	279 2180
QF_FPArith	13848	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	1973 5 1591 52 10091 6 2 128
QF_LinearIntArith	2840	QF_IDL QF_LIA QF_LIRA	458 2377 5
QF_LinearRealArith	462	QF_LRA QF_RDL	349 113
QF_NonLinearIntArith	3410	QF_NIA QF_NIRA	3408 2
QF_NonLinearRealArith	2959	QF_NRA	2959
QF_Strings	4593	QF_S QF_SLIA	172 4421
Total	93382

Cloud Track

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

Division	Division benchmarks	Logic	Logic benchmarks
Arith	41	LRA NRA	40 1
Equality+LinearArith	84	AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFLIA	18 10 7 7 23 19
Equality+NonLinearArith	83	AUFDTNIRA AUFNIRA UFDTNIRA UFNIA	9 38 5 31
Equality	79	UF UFDT	41 38
QF_Equality+LinearArith	1	QF_UFLRA	1
QF_LinearIntArith	89	QF_IDL QF_LIA	63 26
QF_LinearRealArith	23	QF_LRA QF_RDL	19 4
Total	400

Parallel Track

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

Division	Division benchmarks	Logic	Logic benchmarks
Arith	41	LRA NRA	40 1
Equality+LinearArith	84	AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFLIA	18 10 7 7 23 19
Equality+NonLinearArith	83	AUFDTNIRA AUFNIRA UFDTNIRA UFNIA	9 38 5 31
Equality	79	UF UFDT	41 38
QF_Equality+LinearArith	1	QF_UFLRA	1
QF_LinearIntArith	89	QF_IDL QF_LIA	63 26
QF_LinearRealArith	23	QF_LRA QF_RDL	19 4
Total	400

n Non-competing.
e Experimental.