The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
SMT-COMP 2019 will use a large subset of the benchmarks available within the 2019-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/2019-05-06 on StarExec.
In total there are 55 divisions in the Single Query Track. You can download the list of selected benchmarks.
| Division | Number of Included Benchmarks |
|---|---|
| ABVFP | 1 |
| ALIA | 19 |
| AUFBVDTLIAn | 854 |
| AUFDTLIA | 275 |
| AUFLIA | 1638 |
| AUFLIRA | 1683 |
| AUFNIA | 3 |
| AUFNIRA | 300 |
| BV | 823 |
| BVFP | 24 |
| FP | 1238 |
| LIA | 300 |
| LRA | 1003 |
| NIA | 11 |
| NRA | 93 |
| QF_ABV | 7538 |
| QF_ABVFPn | 630 |
| QF_ALIA | 139 |
| QF_ANIA | 7 |
| QF_AUFBV | 41 |
| QF_AUFLIA | 651 |
| QF_AUFNIA | 9 |
| QF_AX | 300 |
| QF_BV | 8909 |
| QF_BVFP | 516 |
| QF_BVFPLRAn | 1 |
| QF_DT | 4 |
| QF_FP | 250 |
| QF_FPLRAn | 13 |
| QF_IDL | 1042 |
| QF_LIA | 3136 |
| QF_LIRA | 7 |
| QF_LRA | 546 |
| QF_NIA | 11494 |
| QF_NIRA | 2 |
| QF_NRA | 2842 |
| QF_RDL | 247 |
| QF_Se | 988 |
| QF_SLIAe | 23175 |
| QF_UF | 3512 |
| QF_UFBV | 223 |
| QF_UFIDL | 300 |
| QF_UFLIA | 300 |
| QF_UFLRA | 541 |
| QF_UFNIA | 300 |
| QF_UFNRA | 26 |
| UF | 2816 |
| UFBV | 72 |
| UFDT | 1547 |
| UFDTLIA | 299 |
| UFDTNIA | 1 |
| UFIDL | 20 |
| UFLIA | 2848 |
| UFLRA | 7 |
| UFNIA | 6253 |
| Total | 89817 |
In total there are 29 divisions in the Incremental Track. You can download the list of selected benchmarks.
| Division | Number of Included Benchmarks |
|---|---|
| ABVFP | 4 |
| ALIA | 24 |
| ANIA | 3 |
| AUFNIRA | 165 |
| BV | 18 |
| BVFP | 10 |
| LIA | 6 |
| LRA | 5 |
| QF_ABV | 631 |
| QF_ABVFPn | 69 |
| QF_ALIA | 44 |
| QF_ANIA | 5 |
| QF_AUFBV | 25 |
| QF_AUFBVLIAn | 300 |
| QF_AUFBVNIA | 44 |
| QF_AUFLIA | 72 |
| QF_BV | 1291 |
| QF_BVFPn | 182 |
| QF_FPn | 2 |
| QF_LIA | 69 |
| QF_LRA | 10 |
| QF_NIA | 10 |
| QF_UF | 383 |
| QF_UFBV | 1165 |
| QF_UFBVLIAn | 179 |
| QF_UFLIA | 386 |
| QF_UFLRA | 1529 |
| QF_UFNIA | 1 |
| UFLRA | 935 |
| Total | 7567 |
In total there are 3 divisions in the Challenge Track (non-incremental). You can download the list of selected benchmarks.
| Division | Number of Included Benchmarks |
|---|---|
| QF_ABV | 7 |
| QF_AUFBV | 15 |
| QF_BV | 7 |
| Total | 29 |
In total there are 3 divisions in the Challenge Track (incremental). You can download the list of selected benchmarks.
| Division | Number of Included Benchmarks |
|---|---|
| QF_ABV | 9 |
| QF_AUFBV | 6 |
| QF_BV | 7 |
| Total | 22 |
In total there are 38 divisions in the Unsat Core Track. You can download the list of selected benchmarks.
| Division | Number of Included Benchmarks |
|---|---|
| AUFBVDTLIAn | 20 |
| AUFLIA | 1245 |
| AUFLIRA | 9885 |
| AUFNIA | 3 |
| AUFNIRA | 526 |
| BV | 233 |
| LIA | 200 |
| NIA | 2 |
| QF_ABV | 1865 |
| QF_ABVFPn | 1965 |
| QF_ALIA | 38 |
| QF_ANIA | 8 |
| QF_AUFBV | 34 |
| QF_AUFLIA | 300 |
| QF_AUFNIA | 12 |
| QF_AX | 202 |
| QF_BV | 2641 |
| QF_BVFPn | 1586 |
| QF_FPn | 10031 |
| QF_LIA | 271 |
| QF_LIRA | 5 |
| QF_LRA | 196 |
| QF_NIA | 2045 |
| QF_NIRA | 2 |
| QF_NRA | 243 |
| QF_UF | 2055 |
| QF_UFBV | 300 |
| QF_UFIDL | 13 |
| QF_UFLIA | 16 |
| QF_UFLRA | 101 |
| QF_UFNIA | 164 |
| QF_UFNRA | 11 |
| UF | 1705 |
| UFDTn | 931 |
| UFIDL | 30 |
| UFLIA | 3867 |
| UFLRA | 10 |
| UFNIA | 1580 |
| Total | 44341 |
In total there are 1 divisions in the Model Validation Track (experimental). You can download the list of selected benchmarks.
| Division | Number of Included Benchmarks |
|---|---|
| QF_BV | 7191 |
| Total | 7191 |
n Non-competing.
e Experimental.