The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
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.
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 |
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 |
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 |
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 |
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 |
n Non-competing.
e Experimental.