The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_RDL division as of Fri Jul 13 00:02:11 GMT
Benchmarks in this division : 255
Time limit: 1200s
| Sequential Performance | Parallel Performance |
|---|---|
| Yices 2.6.0 | Yices 2.6.0 |
| Solver | Error Score | Correctly Solved Score | CPU time Score | Solved | Unsolved |
|---|---|---|---|---|---|
| CVC4 | 0.000 | 233.075 | 139.804 | 216 | 39 |
| MathSATn | 0.000 | 225.266 | 173.787 | 208 | 47 |
| SMTInterpol | 0.000 | 214.953 | 281.974 | 201 | 54 |
| SMTRAT-Rat | 0.000 | 145.451 | 567.205 | 153 | 102 |
| Yices 2.6.0 | 0.000 | 236.448 | 97.253 | 222 | 33 |
| opensmt2 | 0.000 | 208.483 | 279.425 | 192 | 63 |
| veriT | 0.000 | 231.288 | 134.878 | 214 | 41 |
| z3-4.7.1n | 0.000 | 231.602 | 132.138 | 215 | 40 |
| Solver | Error Score | Correctly Solved Score | CPU time Score | WALL time Score | Solved | Unsolved |
|---|---|---|---|---|---|---|
| CVC4 | 0.000 | 233.075 | 139.805 | 139.818 | 216 | 39 |
| MathSATn | 0.000 | 225.266 | 173.787 | 173.788 | 208 | 47 |
| SMTInterpol | 0.000 | 214.953 | 311.124 | 265.579 | 201 | 54 |
| SMTRAT-Rat | 0.000 | 145.451 | 567.210 | 567.234 | 153 | 102 |
| Yices 2.6.0 | 0.000 | 236.448 | 97.255 | 97.248 | 222 | 33 |
| opensmt2 | 0.000 | 208.483 | 279.426 | 279.458 | 192 | 63 |
| veriT | 0.000 | 231.288 | 134.880 | 134.854 | 214 | 41 |
| z3-4.7.1n | 0.000 | 231.602 | 132.140 | 132.036 | 215 | 40 |
n. Non-competing.
1. Scores are computed according to Section 7 of the rules.