The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
SMT-COMP 2017 will use a large subset of the benchmarks available within the 2017-06-05 release of SMT-LIB, as described in the competition rules.
Note that—unlike in 2016—benchmarks with unknown status, bit-vector benchmarks that contain partial operations (i.e., bvudiv, bvurem, bvsdiv, bvsrem or bvsmod), and floating-point benchmarks that contain underspecified operations (i.e., fp.min, fp.max, fp.to_ubv, fp.to_sbv or fp.to_real) are generally eligible for the competition. If your solver is competing in divisions that feature these operations, please ensure that it implements the correct semantics for them.
The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2017-06-05 on StarExec.
All non-incremental SMT-LIB benchmarks (except those excluded because they were syntactically invalid) are eligible for the main track. In total, there are 49 main track divisions. Divisions containing datatypes (DT) are experimental in 2017.
| Logic | Benchmarks eligible for SMT-COMP | Excluded Benchmarks |
|---|---|---|
| ABVFP | 1 | |
| ALIA | 42 | |
| AUFBVDTLIA | 1709 | 391 |
| AUFDTLIA | 728 | |
| AUFLIA | 4 | |
| AUFLIRA | 20011 | |
| AUFNIRA | 1480 | |
| BV | 5151 | |
| BVFP | 24 | |
| FP | 61 | |
| LIA | 388 | |
| LRA | 2419 | |
| NIA | 14 | |
| NRA | 3811 | 22 |
| QF_ABV | 15061 | |
| QF_ABVFP | 18129 | |
| QF_ALIA | 139 | |
| QF_ANIA | 8 | |
| QF_AUFBV | 31 | |
| QF_AUFLIA | 1009 | |
| QF_AUFNIA | 17 | |
| QF_AX | 551 | |
| QF_BV | 40043 | |
| QF_BVFP | 17215 | |
| QF_DT | 8000 | |
| QF_FP | 40302 | |
| QF_IDL | 2193 | |
| QF_LIA | 6141 | |
| QF_LIRA | 7 | |
| QF_LRA | 1649 | |
| QF_NIA | 23876 | |
| QF_NIRA | 3 | |
| QF_NRA | 11354 | |
| QF_RDL | 255 | |
| QF_UF | 6650 | |
| QF_UFBV | 31 | |
| QF_UFIDL | 428 | |
| QF_UFLIA | 583 | |
| QF_UFLRA | 1284 | |
| QF_UFNIA | 7 | |
| QF_UFNRA | 36 | |
| UF | 7562 | 5241 |
| UFBV | 200 | |
| UFDT | 4535 | 541 1 |
| UFDTLIA | 303 | |
| UFIDL | 68 | |
| UFLIA | 10137 | |
| UFLRA | 15 | |
| UFNIA | 3308 | |
| Total | 256973 | 1106 |
1. These benchmarks were excluded because they contained sorts or
operations that are unavailable in the respective logic. Thanks
to Andres Nötzli who reported the issue.
2. Benchmarks non-incremental/NRA/keymaera/ETCS-essentials-live-range2.proof-node1046.smt2
and non-incremental/NRA/keymaera/reactivity-lemma-node2938.smt2
were excluded because they contained possibly
incorrect :status information.
In total, there are 16 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 | |
| AUFNIRA4 | 0 | 165 | 165 | |
| BV4 | 0 | 18 | 18 | |
| BVFP4 | 0 | 10 | 10 | |
| LIA | 6 | 0 | 6 | |
| LRA4 | 0 | 5 5 | 0 | 5 |
| QF_ABVFP4 | 0 | 9 | 9 | |
| QF_ALIA | 44 | 0 | 44 | |
| QF_ANIA | 5 | 0 | 5 | |
| QF_AUFLIA | 72 | 0 | 72 | |
| QF_BV | 18 | 13 | 31 | |
| QF_BVFP | 2 | 63 | 65 | |
| QF_FP | 2 | 1 | 3 | |
| QF_LIA | 68 | 1 6 | 0 | 69 |
| QF_LRA | 10 | 0 | 10 | |
| QF_NIA | 10 | 0 | 10 | |
| QF_UFLIA | 780 | 0 | 780 | |
| QF_UFLRA | 3056 | 2 | 3058 | |
| QF_UFNIA | 1 | 0 | 1 | |
| UFLRA | 1870 | 0 | 1870 | |
| Total | 5971 | 6 | 285 | 6262 |
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, AUFNIRA,
BV, BVFP, LRA and QF_ABVFP are not actually application track
divisions in SMT-COMP 2017.
5. The five benchmarks
in incremental/LRA/20160930-Kopczynski-LOIS/ were
excluded because they did not contain :status
information.
6. Benchmark incremental/QF_LIA/UltimateBuchiAutomizer/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c.smt2
was excluded because it contained incorrect :status
information.
All unsatisfiable main track benchmarks are eligible for the unsat-core track (with minor modifications, e.g., named assertions). Divisions containing datatypes (DT) were excluded from the unsat-core track due to lacking tool support. In total, there are 41 unsat-core track divisions.
| Logic | Eligible Benchmarks | Excluded Benchmarks | All main track benchmarks |
|---|---|---|---|
| ABVFP7 | 0 | 1 | |
| ALIA | 41 | 42 | |
| AUFBVDTLIA7 | 0 | 25 | 1709 |
| AUFDTLIA7 | 0 | 728 | |
| AUFLIA | 3 | 4 | |
| AUFLIRA | 19771 | 20011 | |
| AUFNIRA | 1050 | 1480 | |
| BV | 94 | 5151 | |
| BVFP7 | 0 | 24 | |
| FP7 | 0 | 61 | |
| LIA | 233 | 388 | |
| LRA | 1106 | 2419 | |
| NIA | 4 | 14 | |
| NRA | 3801 | 3813 | |
| QF_ABV | 4673 | 15061 | |
| 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 | 23732 | 40043 | |
| QF_BVFP | 3174 | 17215 | |
| QF_DT7 | 0 | 8000 | |
| QF_FP | 20028 | 40302 | |
| QF_IDL | 816 | 2193 | |
| QF_LIA | 2844 | 6141 | |
| QF_LIRA | 5 | 7 | |
| QF_LRA | 671 | 1649 | |
| QF_NIA | 3130 | 23876 | |
| QF_NIRA | 2 | 3 | |
| QF_NRA | 5296 | 11354 | |
| QF_RDL | 113 | 255 | |
| QF_UF | 4101 | 6650 | |
| QF_UFBV | 31 | 31 | |
| QF_UFIDL | 322 | 428 | |
| QF_UFLIA | 183 | 583 | |
| QF_UFLRA | 511 | 1284 | |
| QF_UFNIA | 7 | 7 | |
| QF_UFNRA | 11 | 36 | |
| UF | 3316 | 7562 | |
| UFBV | 97 | 200 | |
| UFDT7 | 0 | 430 | 4535 |
| UFDTLIA7 | 0 | 303 | |
| UFIDL | 57 | 68 | |
| UFLIA | 7714 | 10137 | |
| UFLRA | 10 | 15 | |
| UFNIA | 2432 | 3308 | |
| Total | 114233 | 455 | 256973 |
7. As there are no eligible benchmarks in SMT-LIB, ABVFP, AUFBVDTLIA, AUFDTLIA, BVFP, FP, QF_DT, UFDT and UFDTLIA are not actually unsat-core track divisions in SMT-COMP 2017.