The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year
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 |
AUFBVDTNIA^{n} | 1 |
AUFDTLIA | 147 |
AUFDTLIRA | 4878 |
AUFDTNIRA | 300 |
AUFFPDTLIRA | 154 |
AUFFPDTNIRA^{n} | 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_ANIA^{n} | 5 |
QF_AUFBV | 31 |
QF_AUFBVLIA^{n} | 300 |
QF_AUFBVNIA^{n} | 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_UFBVLIA^{n} | 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_ANIA^{n} | 8 |
QF_AUFBV | 34 |
QF_AUFLIA | 300 |
QF_AUFNIA^{n} | 12 |
QF_AX | 202 |
QF_BV | 2119 |
QF_BVFP | 1269 |
QF_BVFPLRA^{n} | 46 |
QF_FP | 8024 |
QF_LIA | 271 |
QF_LIRA | 5 |
QF_LRA | 196 |
QF_NIA^{n} | 1636 |
QF_NIRA^{n} | 2 |
QF_NRA^{n} | 243 |
QF_UF | 1644 |
QF_UFBV | 300 |
QF_UFFP | 2 |
QF_UFIDL | 13 |
QF_UFLIA | 16 |
QF_UFLRA | 101 |
QF_UFNIA^{n} | 164 |
QF_UFNRA^{n} | 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_IDL^{e} | 512 |
QF_LIA^{e} | 1532 |
QF_LIRA^{e} | 1 |
QF_LRA^{e} | 378 |
QF_RDL^{e} | 109 |
Total | 8284 |
n Non-competing.
e Experimental.