The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
SMT-COMP 2015 will use a subset of the benchmarks available within the 2015-06-01 release of SMT-LIB, as described in the competition rules. Specifically, benchmarks with unknown status, bit-vector benchmarks that contain partial operations (e.g., bit-vector division), and floating-point benchmarks that contain underspecified operations (e.g., fp.min) will not be used.
The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2015-06-01 on StarExec. They may also be downloaded from http://www.cs.nyu.edu/~barrett/smtlib/.
The subset of benchmarks eligible for SMT-COMP 2015 is available in StarExec spaces root/SMT/Competitions and evaluations/SMT-COMP 2015/Benchmarks - Application Track and root/SMT/Competitions and evaluations/SMT-COMP 2015/Benchmarks - Main Track for the application and main track, respectively.
| Logic | Benchmarks eligible for SMT-COMP | Benchmarks with unknown status | Benchmarks in SMT-LIB |
|---|---|---|---|
| ALIA | 42 | 0 | 42 |
| AUFLIA | 4 | 0 | 4 |
| AUFLIRA | 19849 | 165 | 20014 |
| AUFNIRA | 1050 | 445 | 1495 |
| BV | 85 | 106 | 191 |
| LIA | 201 | 189 | 390 |
| LRA | 339 | 282 | 621 |
| NIA | 9 | 5 | 14 |
| NRA | 3788 | 25 | 3813 |
| QF_ABV | 14720 (197 excluded1) | 174 | 15091 |
| QF_ALIA | 134 | 0 | 134 |
| QF_ANIA | 6 | 0 | 6 |
| QF_AUFBV | 37 | 0 | 37 |
| QF_AUFLIA | 1009 | 0 | 1009 |
| QF_AUFNIA | 21 | 0 | 21 |
| QF_AX | 551 | 0 | 551 |
| QF_BV | 26414 (6062 excluded1) | 17953 | 50429 |
| QF_BVFP2 | 7 (1 excluded1) | 0 | 8 |
| QF_FP2 | 34413 (5706 excluded1) | 215 | 40334 |
| QF_IDL | 2094 | 104 | 2198 |
| QF_LIA | 5839 | 302 | 6141 |
| QF_LIRA | 6 | 1 | 7 |
| QF_LRA | 1626 | 56 | 1682 |
| QF_NIA | 8475 | 925 | 9400 |
| QF_NIRA | 2 | 1 | 3 |
| QF_NRA | 10184 | 1356 | 11540 |
| QF_RDL | 220 | 35 | 255 |
| QF_UF | 6649 | 1 | 6650 |
| QF_UFBV | 31 | 0 | 31 |
| QF_UFIDL | 441 | 0 | 441 |
| QF_UFLIA | 598 | 0 | 598 |
| QF_UFLRA | 1627 | 3 | 1630 |
| QF_UFNIA | 7 | 0 | 7 |
| QF_UFNRA | 34 | 9 | 43 |
| UF | 2839 | 2909 | 5748 |
| UFBV | 71 | 129 | 200 |
| UFIDL | 68 | 12 | 80 |
| UFLIA | 8404 | 3736 | 12140 |
| UFLRA | 25 | 0 | 25 |
| UFNIA | 2319 | 1033 | 3352 |
| Total | 154238 (11966 excluded1) | 30171 | 196375 |
1. Excluded because they contain partial or underspecified
operations (e.g., bit-vector division, fp.min).
2. Floating-point divisions are considered experimental in 2015.
| Logic | Benchmarks eligible for SMT-COMP | Benchmarks with unknown status3 | Benchmarks in SMT-LIB |
|---|---|---|---|
| ALIA | 24 | 0 | 24 |
| ANIA | 3 | 0 | 3 |
| AUFNIRA4 | 0 | 165 | 165 |
| LIA | 6 | 0 | 6 |
| QF_ALIA | 44 | 0 | 44 |
| QF_ANIA | 5 | 0 | 5 |
| QF_AUFLIA | 72 | 0 | 72 |
| QF_BV | 18 | 0 | 18 |
| QF_LIA | 65 | 0 | 65 |
| QF_LRA | 10 | 0 | 10 |
| QF_NIA | 10 | 0 | 10 |
| QF_UFLIA | 905 | 0 | 905 |
| QF_UFLRA | 3331 | 2 | 3333 |
| QF_UFNIA | 1 | 0 | 1 |
| UFLRA | 5358 | 0 | 5358 |
| Total | 9852 | 167 | 10019 |
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, AUFNIRA is not
actually an application track division in SMT-COMP 2015.