Home • Intro • Rules • Participants • Results • Tools • Specs • Thanks • SMT-LIB • Previous

Selected Benchmarks

Please note that the metadata (category and difficulty) of benchmarks used for SMT-COMP'07 benchmark selection are different than that encoded in benchmark files of the current SMT-LIB release. In some cases even the status (SAT, UNSAT, or UNKNOWN) for benchmarks has been changed due to new evidence that questions the validity of a SAT or UNSAT status. See the benchmarks page for details.

The benchmark selection process for SMT-COMP'07 is described in the competition rules and further on the benchmark selection page.

Selected Benchmark List

These 2297 benchmarks are the official selected benchmarks for SMT-COMP'07 (statistical details follow):

Statistics of Selected Benchmarks

The division breakdown is as follows: 

+-----------+-----+
| division  | #   |
+-----------+-----+
| QF_UF     | 200 |
| QF_RDL    | 169 |
| QF_IDL    | 203 |
| QF_UFIDL  | 203 |
| QF_UFLIA  | 110 |
| QF_LRA    | 202 |
| QF_LIA    | 203 |
| QF_AUFLIA | 206 |
| QF_BV     | 200 |
| QF_AUFBV  | 200 |
| AUFLIA    | 201 |
| AUFLIRA   | 200 |
+-----------+-----+

By category: 

+------------+------+
| category   | #    |
+------------+------+
| check      |   24 |
| crafted    |  418 |
| industrial | 1845 |
| random     |   10 |
+------------+------+

By difficulty: 

+------------+-----+
| difficulty | #   |
+------------+-----+
|          0 | 784 |
|          1 | 643 |
|          2 | 279 |
|          3 | 295 |
|          4 | 114 |
|          5 | 182 |
+------------+-----+

And by solution: 

+----------+------+
| solution | #    |
+----------+------+
| sat      |  971 |
| unsat    | 1326 |
+----------+------+

680 of these 2297 benchmarks are new since SMT-COMP'06.

596 of the 2297 were also selected for SMT-COMP'06 (573 if you don't count benchmarks that are listed in the “check” category this year). The division breakdown for common SMT-COMP'06 and SMT-COMP'07 benchmarks is: 

+-----------+-----+
| name      | #   |
+-----------+-----+
| QF_UF     |  31 |
| QF_RDL    |  98 |
| QF_IDL    |  26 |
| QF_UFIDL  |  58 |
| QF_UFLIA  | 100 |
| QF_LRA    |  56 |
| QF_LIA    |  88 |
| QF_AUFLIA |  90 |
| AUFLIA    |  18 |
| AUFLIRA   |   8 |
+-----------+-----+

Naturally, no overlap exists for QF_UFBV32 (last year's division which is not being repeated), or for this year's new divisions QF_BV and QF_AUFBV.

Home • Intro • Rules • Participants • Results • Tools • Specs • Thanks • SMT-LIB • Previous

Last modified: Tue 17 Feb 2015 14:58 UTC
 Valid XHTML 1.0 Valid CSS!