Benchmarks

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

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2023-05-08 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	1660	LIA LRA NIA NRA	300 1013 248 99
Bitvec	1040	BV	1040
Equality+LinearArith	15539	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	1537 188 4185 1663 1683 278 3129 20 2849 7
Equality+MachineArith	6164	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVDT UFBVFP UFBVLIA UFFPDTNIRA	2487 60 77 761 742 8 1062 57 159 144 1 2 208 396
Equality+NonLinearArith	9551	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	56 762 3 300 2 2149 6279
Equality	4407	UF UFDT	2857 1550
FPArith	1849	BVFP BVFPLRA FP FPLRA	208 266 1334 41
QF_Bitvec	10084	QF_BV	10084
QF_Datatypes	401	QF_DT QF_UFDT	201 200
QF_Equality+Bitvec	1755	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	1341 38 300 76
QF_Equality+LinearArith	1922	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	166 530 76 9 300 300 541
QF_Equality+NonLinearArith	554	QF_ANIA QF_AUFNIA QF_UFDTNIA QF_UFNIA QF_UFNRA	123 9 76 298 48
QF_Equality	3757	QF_AX QF_UF	279 3478
QF_FPArith	1596	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFPDTNIRA	593 25 1 414 78 273 58 154
QF_LinearIntArith	6439	QF_IDL QF_LIA QF_LIRA	1203 5229 7
QF_LinearRealArith	825	QF_LRA QF_RDL	578 247
QF_NonLinearIntArith	11947	QF_NIA QF_NIRA	11945 2
QF_NonLinearRealArith	2795	QF_NRA	2795
QF_Strings	30855	QF_S QF_SLIA QF_SNIA	8847 21938 70
Total	113140

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_UFFP	9214 7 300 64 166 1
QF_LinearIntArith	69	QF_LIA	69
QF_LinearRealArith	10	QF_LRA	10
QF_NonLinearIntArith	12	QF_NIA	12
Total	22302

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	384	LIA NIA	227 157
Bitvec	425	BV	425
Equality+LinearArith	23690	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	401 88 4986 1296 9889 202 2873 30 3915 10
Equality+MachineArith	2165	ABV ABVFP ABVFPLRA AUFBVDTLIA AUFBVDTNIRA AUFFPDTNIRA UFFPDTNIRA	485 3 4 180 1062 131 300
Equality+NonLinearArith	6814	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	1 618 3 549 1 2022 3620
Equality	3195	UF UFDT	1826 1369
FPArith	21	BVFP BVFPLRA	10 11
QF_Bitvec	2949	QF_BV	2949
QF_Datatypes	200	QF_DT QF_UFDT	100 100
QF_Equality+Bitvec	2232	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	1865 34 327 6
QF_Equality+LinearArith	598	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	30 300 11 17 113 26 101
QF_Equality+NonLinearArith	271	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	29 12 205 25
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	1972 5 1589 52 10050 2 4
QF_LinearIntArith	1087	QF_IDL QF_LIA QF_LIRA	100 982 5
QF_LinearRealArith	208	QF_LRA	208
QF_NonLinearIntArith	2967	QF_NIA QF_NIRA	2965 2
QF_NonLinearRealArith	434	QF_NRA	434
QF_Strings	9382	QF_S QF_SLIA	2953 6429
Total	72959

Model Validation Track

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

Division	Division benchmarks	Logic	Logic benchmarks
QF_ADT+BitVece	5294	QF_ABV QF_AUFBV QF_UFBVDT	5227 24 43
QF_ADT+LinArithe	800	QF_ALIA QF_AUFLIA QF_AX QF_UFDTLIA QF_UFDTLIRA	101 300 272 47 80
QF_Array+Bitvec+LinArithe	5924	QF_ABV QF_ALIA QF_AUFBV QF_AUFLIA QF_AX	5227 101 24 300 272
QF_Bitvec	9069	QF_BV	9069
QF_Datatypes+BitVec+LinArithe	170	QF_UFBVDT QF_UFDTLIA QF_UFDTLIRA	43 47 80
QF_Datatypese	1939	QF_DT QF_UFDT	1836 103
QF_Equality+Bitvec	412	QF_UFBV	412
QF_Equality+LinearArith	921	QF_UFIDL QF_UFLIA QF_UFLRA	206 330 385
QF_Equality+NonLinearArithe	459	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	93 5 329 32
QF_Equality	1571	QF_UF	1571
QF_FPArithe	24441	QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFPDTNIRA	7046 25 1 7030 124 10137 54 24
QF_LinearIntArith	4958	QF_IDL QF_LIA QF_LIRA	745 4212 1
QF_LinearRealArith	631	QF_LRA QF_RDL	521 110
QF_NonLinearIntArithe	7607	QF_NIA	7607
QF_NonLinearRealArithe	2982	QF_NRA	2982
Total	67178

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	1700	LIA LRA NIA NRA	150 425 167 958
Bitvec	1428	BV	1428
Equality+LinearArith	12406	ALIA AUFDTLIA AUFDTLIRA AUFLIA AUFLIRA UFDTLIA UFDTLIRA UFIDL UFLIA UFLRA	442 88 2527 677 4946 202 1471 57 1986 10
Equality+MachineArith	2006	ABV ABVFP ABVFPLRA AUFBV AUFBVDTLIA AUFBVDTNIRA AUFBVFP AUFFPDTNIRA UFBV UFBVFP UFBVLIA UFFPDTNIRA	485 3 4 353 185 531 27 131 127 2 8 150
Equality+NonLinearArith	4736	ANIA AUFDTNIRA AUFNIA AUFNIRA UFDTNIA UFDTNIRA UFNIA	1 372 3 286 1 1246 2827
Equality	1880	UF UFDT	977 903
FPArith	1177	BVFP BVFPLRA FP	14 24 1139
QF_Bitvec	6969	QF_BV	6969
QF_Datatypes	1230	QF_DT QF_UFDT	1130 100
QF_Equality+Bitvec	1389	QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT	1171 40 172 6
QF_Equality+LinearArith	799	QF_ALIA QF_AUFLIA QF_UFDTLIA QF_UFDTLIRA QF_UFIDL QF_UFLIA QF_UFLRA	72 190 11 66 150 160 150
QF_Equality+NonLinearArith	242	QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA	29 12 176 25
QF_Equality	1240	QF_AX QF_UF	150 1090
QF_FPArith	7041	QF_ABVFP QF_ABVFPLRA QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP QF_UFFPDTNIRA	990 5 797 53 5061 5 2 128
QF_LinearIntArith	1442	QF_IDL QF_LIA QF_LIRA	229 1208 5
QF_LinearRealArith	295	QF_LRA QF_RDL	182 113
QF_NonLinearIntArith	2256	QF_NIA QF_NIRA	2254 2
QF_NonLinearRealArith	1596	QF_NRA	1596
QF_Strings	9283	QF_S QF_SLIA	1670 7613
Total	59115

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.