The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
SMT-COMP 2020 will use a large subset of the benchmarks available within the 2020-04-25 release of SMT-LIB, as described in the competition rules.
The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2020-04-25 on StarExec.
In total there are 70 divisions in the Single Query Track. You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.
| Division | Number of Included Benchmarks |
|---|---|
| ABV | 169 |
| ABVFP | 30 |
| ABVFPLRA | 75 |
| ALIA | 19 |
| AUFBVDTLIA | 683 |
| AUFBVDTNIAn | 1 |
| AUFDTLIA | 147 |
| AUFDTLIRA | 4878 |
| AUFDTNIRA | 300 |
| AUFFPDTLIRA | 154 |
| AUFFPDTNIRAn | 13 |
| AUFLIA | 1310 |
| AUFLIRA | 1346 |
| AUFNIA | 3 |
| AUFNIRA | 300 |
| BV | 696 |
| BVFP | 224 |
| BVFPLRA | 185 |
| FP | 993 |
| FPLRA | 27 |
| LIA | 300 |
| LRA | 802 |
| NIA | 17 |
| NRA | 93 |
| QF_ABV | 3385 |
| QF_ABVFP | 500 |
| QF_ABVFPLRA | 74 |
| QF_ALIA | 116 |
| QF_ANIA | 94 |
| QF_AUFBV | 34 |
| QF_AUFLIA | 467 |
| QF_AUFNIA | 9 |
| QF_AX | 300 |
| QF_BV | 6861 |
| QF_BVFP | 394 |
| QF_BVFPLRA | 168 |
| QF_DT | 4 |
| QF_FP | 270 |
| QF_FPLRA | 57 |
| QF_IDL | 834 |
| QF_LIA | 2508 |
| QF_LIRA | 7 |
| QF_LRA | 429 |
| QF_NIA | 9195 |
| QF_NIRA | 2 |
| QF_NRA | 2230 |
| QF_RDL | 247 |
| QF_S | 927 |
| QF_SLIA | 27033 |
| QF_UF | 2800 |
| QF_UFBV | 217 |
| QF_UFFP | 2 |
| QF_UFIDL | 300 |
| QF_UFLIA | 300 |
| QF_UFLRA | 432 |
| QF_UFNIA | 300 |
| QF_UFNRA | 27 |
| UF | 2291 |
| UFBV | 72 |
| UFDT | 1223 |
| UFDTLIA | 277 |
| UFDTLIRA | 4296 |
| UFDTNIA | 1 |
| UFDTNIRA | 736 |
| UFFPDTLIRA | 373 |
| UFFPDTNIRA | 21 |
| UFIDL | 20 |
| UFLIA | 2278 |
| UFLRA | 7 |
| UFNIA | 5041 |
| Total | 89924 |
In total there are 32 divisions in the Incremental Track. You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.
| Division | Number of Included Benchmarks |
|---|---|
| ALIA | 24 |
| ANIA | 3 |
| AUFNIRA | 165 |
| BV | 18 |
| BVFP | 1 |
| LIA | 6 |
| LRA | 5 |
| QF_ABV | 508 |
| QF_ABVFP | 62 |
| QF_ALIA | 44 |
| QF_ANIAn | 5 |
| QF_AUFBV | 31 |
| QF_AUFBVLIAn | 300 |
| QF_AUFBVNIAn | 44 |
| QF_AUFLIA | 72 |
| QF_BV | 1035 |
| QF_BVFP | 119 |
| QF_FP | 1 |
| QF_LIA | 69 |
| QF_LRA | 10 |
| QF_NIA | 10 |
| QF_UF | 306 |
| QF_UFBV | 932 |
| QF_UFBVLIAn | 179 |
| QF_UFFP | 1 |
| QF_UFLIA | 309 |
| QF_UFLRA | 1223 |
| QF_UFNIA | 1 |
| UF | 2031 |
| UFLRA | 748 |
| UFNIA | 2029 |
| UFNRA | 5 |
| Total | 10296 |
In total there are 49 divisions in the Unsat Core Track. You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.
| Division | Number of Included Benchmarks |
|---|---|
| ABV | 2 |
| AUFBVDTLIA | 20 |
| AUFDTLIRA | 4330 |
| AUFDTNIRA | 50 |
| AUFFPDTLIRA | 132 |
| AUFLIA | 996 |
| AUFLIRA | 7908 |
| AUFNIA | 3 |
| AUFNIRA | 421 |
| BV | 255 |
| BVFPLRA | 1 |
| LIA | 235 |
| NIA | 2 |
| QF_ABV | 1492 |
| QF_ABVFP | 1572 |
| QF_ALIA | 30 |
| QF_ANIAn | 8 |
| QF_AUFBV | 34 |
| QF_AUFLIA | 300 |
| QF_AUFNIAn | 12 |
| QF_AX | 202 |
| QF_BV | 2119 |
| QF_BVFP | 1269 |
| QF_BVFPLRAn | 46 |
| QF_FP | 8024 |
| QF_LIA | 271 |
| QF_LIRA | 5 |
| QF_LRA | 196 |
| QF_NIAn | 1636 |
| QF_NIRAn | 2 |
| QF_NRAn | 243 |
| QF_UF | 1644 |
| QF_UFBV | 300 |
| QF_UFFP | 2 |
| QF_UFIDL | 13 |
| QF_UFLIA | 16 |
| QF_UFLRA | 101 |
| QF_UFNIAn | 164 |
| QF_UFNRAn | 11 |
| UF | 1374 |
| UFDT | 745 |
| UFDTLIRA | 3342 |
| UFDTNIRA | 300 |
| UFFPDTLIRA | 300 |
| UFFPDTNIRA | 2 |
| UFIDL | 30 |
| UFLIA | 3093 |
| UFLRA | 10 |
| UFNIA | 1276 |
| Total | 44539 |
In total there are 6 divisions in the Model Validation Track. You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.
| Division | Number of Included Benchmarks |
|---|---|
| QF_BV | 5752 |
| QF_IDLe | 512 |
| QF_LIAe | 1532 |
| QF_LIRAe | 1 |
| QF_LRAe | 378 |
| QF_RDLe | 109 |
| Total | 8284 |
n Non-competing.
e Experimental.