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 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

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.