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 18 divisions in the Unsat Core Track.
You can download the list of selected benchmarks.

Division	Division benchmarks	Logic	Logic benchmarks
Arith	237	LIA NIA	227 10
Bitvec	300	BV	300
Equality+LinearArith	22866	AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIRA UFIDL UFLIA UFLRA	60 4917 1245 9885 2857 30 3862 10
Equality+MachineArith	1515	ABV AUFBVDTLIA AUFBVDTNIRA AUFFPDTNIRA UFFPDTNIRA	2 20 1062 131 300
Equality+NonLinearArith	4161	AUFDTNIRA AUFNIA AUFNIRA UFDTNIRA UFNIA	492 3 526 1552 1588
Equality	2628	UF UFDT	1697 931
FPArith	1	BVFPLRA	1
QF_Bitvec	2886	QF_BV	2886
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	228	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	26 12 179 11
QF_Equality	2263	QF_AX QF_UF	202 2061
QF_FPArith	13634	QF_ABVFP QF_BVFP QF_BVFPLRA QF_FP QF_UFFP QF_UFFPDTNIRA	1965 1586 46 10031 2 4
QF_LinearIntArith	1027	QF_IDL QF_LIA QF_LIRA	100 922 5
QF_LinearRealArith	196	QF_LRA	196
QF_NonLinearIntArith	2058	QF_NIA QF_NIRA	2056 2
QF_NonLinearRealArith	243	QF_NRA	243
Total	57245

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	7319	QF_BV	7319
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	17243	QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA	7024 106 10068 45
QF_LinearIntArith	4785	QF_IDL QF_LIA QF_LIRA	735 4049 1
QF_LinearRealArith	582	QF_LRA QF_RDL	473 109
Total	32766

Proof Exhibition Track

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

Division	Division benchmarks	Logic	Logic benchmarks
Arith	237	LIA NIA	227 10
Bitvec	300	BV	300
Equality+LinearArith	22866	AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIRA UFIDL UFLIA UFLRA	60 4917 1245 9885 2857 30 3862 10
Equality+MachineArith	1515	ABV AUFBVDTLIA AUFBVDTNIRA AUFFPDTNIRA UFFPDTNIRA	2 20 1062 131 300
Equality+NonLinearArith	4161	AUFDTNIRA AUFNIA AUFNIRA UFDTNIRA UFNIA	492 3 526 1552 1588
Equality	2628	UF UFDT	1697 931
FPArith	1	BVFPLRA	1
QF_Bitvec	2886	QF_BV	2886
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	228	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	26 12 179 11
QF_Equality	2263	QF_AX QF_UF	202 2061
QF_FPArith	13634	QF_ABVFP QF_BVFP QF_BVFPLRA QF_FP QF_UFFP QF_UFFPDTNIRA	1965 1586 46 10031 2 4
QF_LinearIntArith	1027	QF_IDL QF_LIA QF_LIRA	100 922 5
QF_LinearRealArith	196	QF_LRA	196
QF_NonLinearIntArith	2058	QF_NIA QF_NIRA	2056 2
QF_NonLinearRealArith	243	QF_NRA	243
Total	57245

Cloud Track

The Cloud Track divisions are not yet available.

Parallel Track

The Parallel Track divisions are not yet available.

n Non-competing.
e Experimental.