The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFIDL division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 300 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 298 | 5406.047 | 5406.477 | 298 | 76 | 222 | 2 | 2 | 0 | |
| 2018-Yicesn | 0 | 298 | 5418.913 | 5419.472 | 298 | 76 | 222 | 2 | 2 | 0 | |
| Z3n | 0 | 298 | 5631.745 | 5631.496 | 298 | 76 | 222 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 285 | 50037.164 | 48281.097 | 285 | 76 | 209 | 15 | 15 | 0 | |
| veriT | 0 | 278 | 62289.678 | 62294.447 | 278 | 76 | 202 | 22 | 17 | 0 | |
| CVC4 | 0 | 276 | 81633.348 | 81642.172 | 276 | 76 | 200 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 298 | 5406.307 | 5406.357 | 298 | 76 | 222 | 2 | 2 | 0 | |
| 2018-Yicesn | 0 | 298 | 5419.263 | 5419.342 | 298 | 76 | 222 | 2 | 2 | 0 | |
| Z3n | 0 | 298 | 5632.375 | 5631.466 | 298 | 76 | 222 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 285 | 50037.164 | 48281.097 | 285 | 76 | 209 | 15 | 15 | 0 | |
| veriT | 0 | 278 | 62292.618 | 62293.757 | 278 | 76 | 202 | 22 | 17 | 0 | |
| CVC4 | 0 | 276 | 81639.118 | 81641.402 | 276 | 76 | 200 | 24 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 76 | 5.939 | 5.956 | 76 | 76 | 0 | 224 | 2 | 0 |
| 2018-Yicesn | 0 | 76 | 9.587 | 9.609 | 76 | 76 | 0 | 224 | 2 | 0 |
| Z3n | 0 | 76 | 11.291 | 11.292 | 76 | 76 | 0 | 224 | 2 | 0 |
| veriT | 0 | 76 | 14.017 | 14.0 | 76 | 76 | 0 | 224 | 17 | 0 |
| CVC4 | 0 | 76 | 61.443 | 61.45 | 76 | 76 | 0 | 224 | 24 | 0 |
| SMTInterpol | 0 | 76 | 303.882 | 111.376 | 76 | 76 | 0 | 224 | 15 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 222 | 5400.368 | 5400.401 | 222 | 0 | 222 | 78 | 2 | 0 |
| 2018-Yicesn | 0 | 222 | 5409.676 | 5409.733 | 222 | 0 | 222 | 78 | 2 | 0 |
| Z3n | 0 | 222 | 5621.085 | 5620.173 | 222 | 0 | 222 | 78 | 2 | 0 |
| SMTInterpol | 0 | 209 | 49733.283 | 48169.721 | 209 | 0 | 209 | 91 | 15 | 0 |
| veriT | 0 | 202 | 62278.601 | 62279.757 | 202 | 0 | 202 | 98 | 17 | 0 |
| CVC4 | 0 | 200 | 81577.675 | 81579.952 | 200 | 0 | 200 | 100 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 294 | 307.8 | 307.838 | 294 | 76 | 218 | 6 | 6 | 0 | |
| 2018-Yicesn | 0 | 294 | 316.706 | 316.752 | 294 | 76 | 218 | 6 | 6 | 0 | |
| Z3n | 0 | 291 | 375.46 | 374.479 | 291 | 76 | 215 | 9 | 9 | 0 | |
| SMTInterpol | 0 | 256 | 3305.323 | 2033.401 | 256 | 76 | 180 | 44 | 44 | 0 | |
| veriT | 0 | 254 | 1526.776 | 1526.755 | 254 | 76 | 178 | 46 | 46 | 0 | |
| CVC4 | 0 | 207 | 2814.217 | 2814.236 | 207 | 76 | 131 | 93 | 93 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.