SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

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.