The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
SMT-COMP 2018 will use a large subset of the benchmarks available within the 2018-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/2018-05-20 on StarExec.
All non-incremental SMT-LIB benchmarks are eligible for the main track. In total, there are 50 main track divisions. Division QF_SLIA, which contains strings, is experimental in 2018.
| Logic | Eligible Benchmarks | Excluded Benchmarks |
|---|---|---|
| ABVFP | 1 | |
| ALIA | 42 | |
| AUFBVDTLIA | 1709 | |
| AUFDTLIA | 728 | |
| AUFLIA | 4 | 32721 |
| AUFLIRA | 20011 | |
| AUFNIA2 | 0 | 31 |
| AUFNIRA | 1480 | |
| BV | 5751 | |
| BVFP | 24 | |
| FP | 61 | |
| LIA | 388 | |
| LRA | 2419 | |
| NIA | 14 | |
| NRA | 3813 | |
| QF_ABV | 15066 | |
| QF_ABVFP | 18129 | |
| QF_ALIA | 139 | |
| QF_ANIA | 8 | |
| QF_AUFBV | 31 | |
| QF_AUFLIA | 1009 | 2941 |
| QF_AUFNIA | 17 | |
| QF_AX | 551 | |
| QF_BV | 40102 | |
| QF_BVFP | 17215 | |
| QF_DT | 8000 | |
| QF_FP | 40300 | |
| QF_IDL | 2193 | |
| QF_LIA | 6947 | |
| QF_LIRA | 7 | |
| QF_LRA | 1649 | |
| QF_NIA | 23876 | |
| QF_NIRA | 3 | |
| QF_NRA | 11489 | |
| QF_RDL | 255 | |
| QF_SLIA | 72705 | |
| QF_UF | 7423 | 341 |
| QF_UFBV | 1224 | |
| QF_UFIDL | 428 | |
| QF_UFLIA | 583 | |
| QF_UFLRA | 1284 | |
| QF_UFNIA | 7 | |
| QF_UFNRA | 36 | |
| UF | 7562 | |
| UFBV | 200 | |
| UFDT | 4527 | |
| UFDTLIA | 303 | |
| UFIDL | 68 | |
| UFLIA | 10137 | |
| UFLRA | 15 | |
| UFNIA | 3308 | |
| Total | 333241 | 3603 |
1. All benchmarks in family 20170829-Rodin/ were excluded
because they contained :named terms.
2. As there are no eligible benchmarks in SMT-LIB, AUFNIA is not
actually a main track division in SMT-COMP 2018.
In total, there are 21 application track divisions.
| Logic | Eligible Benchmarks | Excluded Benchmarks | Benchmarks with unknown status3 | Benchmarks in SMT-LIB |
|---|---|---|---|---|
| ABVFP4 | 0 | 4 | 4 | |
| ALIA | 24 | 0 | 24 | |
| ANIA | 3 | 0 | 3 | |
| AUFNIRA | 117 | 48 | 165 | |
| BV | 17 | 1 | 18 | |
| BVFP4 | 0 | 10 | 10 | |
| LIA | 6 | 0 | 6 | |
| LRA4 | 0 | 55 | 0 | 5 |
| QF_ABV | 15 | 0 | 15 | |
| QF_ABVFP4 | 0 | 9 | 9 | |
| QF_ALIA | 44 | 0 | 44 | |
| QF_ANIA | 5 | 0 | 5 | |
| QF_AUFBV | 10 | 0 | 10 | |
| QF_AUFLIA | 72 | 0 | 72 | |
| QF_BV | 815 | 3 | 818 | |
| QF_BVFP | 2 | 63 | 65 | |
| QF_FP | 2 | 1 | 3 | |
| QF_LIA | 69 | 0 | 69 | |
| QF_LRA | 10 | 0 | 10 | |
| QF_NIA | 10 | 0 | 10 | |
| QF_UF4 | 0 | 766 | 766 | |
| QF_UFBV | 2327 | 0 | 2327 | |
| QF_UFLIA | 780 | 0 | 780 | |
| QF_UFLRA | 3058 | 0 | 3058 | |
| QF_UFNIA | 1 | 0 | 1 | |
| UFLRA | 1870 | 0 | 1870 | |
| Total | 9257 | 5 | 905 | 10167 |
3. For the application track, a benchmark is ineligible if its
first check-sat command has unknown status.
Otherwise, (some non-empty prefix of) the benchmark is eligible.
4. As there are no eligible benchmarks in SMT-LIB, ABVFP, BVFP,
LRA, QF_ABVFP and QF_UF are not actually application track
divisions in SMT-COMP 2018.
5. The five benchmarks
in incremental/LRA/20160930-Kopczynski-LOIS/ were
excluded because they did not contain :status
information.
All unsatisfiable main track benchmarks are eligible for the unsat-core track (with minor modifications, e.g., named assertions). In total, there are 44 unsat-core track divisions.
| Logic | Eligible Benchmarks | All main track benchmarks |
|---|---|---|
| ABVFP6 | 0 | 1 |
| ALIA | 41 | 42 |
| AUFBVDTLIA | 25 | 1709 |
| AUFDTLIA6 | 0 | 728 |
| AUFLIA | 3 | 4 |
| AUFLIRA | 19771 | 20011 |
| AUFNIA6 | 0 | 0 |
| AUFNIRA | 1053 | 1480 |
| BV | 4937 | 5751 |
| BVFP6 | 0 | 24 |
| FP6 | 0 | 61 |
| LIA | 233 | 388 |
| LRA | 1539 | 2419 |
| NIA | 4 | 14 |
| NRA | 3801 | 3813 |
| QF_ABV | 4677 | 15066 |
| QF_ABVFP | 3934 | 18129 |
| QF_ALIA | 80 | 139 |
| QF_ANIA | 8 | 8 |
| QF_AUFBV | 25 | 31 |
| QF_AUFLIA | 516 | 1009 |
| QF_AUFNIA | 12 | 17 |
| QF_AX | 279 | 551 |
| QF_BV | 25700 | 40102 |
| QF_BVFP | 3174 | 17215 |
| QF_DT | 4422 | 8000 |
| QF_FP | 20026 | 40300 |
| QF_IDL | 816 | 2193 |
| QF_LIA | 3019 | 6947 |
| QF_LIRA | 5 | 7 |
| QF_LRA | 683 | 1649 |
| QF_NIA | 4842 | 23876 |
| QF_NIRA | 2 | 3 |
| QF_NRA | 5357 | 11489 |
| QF_RDL | 113 | 255 |
| QF_SLIA6 | 0 | 72705 |
| QF_UF | 4330 | 7423 |
| QF_UFBV | 575 | 1224 |
| QF_UFIDL | 322 | 428 |
| QF_UFLIA | 183 | 583 |
| QF_UFLRA | 511 | 1284 |
| QF_UFNIA | 7 | 7 |
| QF_UFNRA | 11 | 36 |
| UF | 3442 | 7562 |
| UFBV | 97 | 200 |
| UFDT | 1863 | 4527 |
| UFDTLIA6 | 0 | 303 |
| UFIDL | 57 | 68 |
| UFLIA | 7743 | 10137 |
| UFLRA | 10 | 15 |
| UFNIA | 2457 | 3308 |
| Total | 130705 | 333241 |
6. As there are no eligible benchmarks in SMT-LIB, ABVFP, AUFDTLIA, AUFNIA, BVFP, FP, QF_SLIA and UFDTLIA are not actually unsat-core track divisions in SMT-COMP 2018.