The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ALIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 116 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 116 | 56.223 | 55.591 | 116 | 54 | 62 | 0 | 0 | 0 | |
| Yices2-fixedn | 0 | 116 | 68.043 | 68.548 | 116 | 54 | 62 | 0 | 0 | 0 | |
| Yices2 | 0 | 116 | 69.148 | 68.544 | 116 | 54 | 62 | 0 | 0 | 0 | |
| MathSAT5n | 0 | 116 | 102.499 | 102.516 | 116 | 54 | 62 | 0 | 0 | 0 | |
| z3n | 0 | 116 | 621.208 | 621.279 | 116 | 54 | 62 | 0 | 0 | 0 | |
| SMTInterpol | 0 | 116 | 1036.445 | 573.192 | 116 | 54 | 62 | 0 | 0 | 0 | |
| SMTInterpol-fixedn | 0 | 116 | 1065.72 | 575.918 | 116 | 54 | 62 | 0 | 0 | 0 | |
| CVC4 | 0 | 115 | 5085.81 | 5083.448 | 115 | 54 | 61 | 1 | 1 | 0 | |
| Alt-Ergo | 0 | 51 | 70269.95 | 68598.862 | 51 | 0 | 51 | 65 | 56 | 0 | |
| veriT | 0 | 6 | 4.564 | 4.605 | 6 | 0 | 6 | 110 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 116 | 56.223 | 55.591 | 116 | 54 | 62 | 0 | 0 | 0 | |
| Yices2 | 0 | 116 | 69.148 | 68.544 | 116 | 54 | 62 | 0 | 0 | 0 | |
| Yices2-fixedn | 0 | 116 | 68.043 | 68.548 | 116 | 54 | 62 | 0 | 0 | 0 | |
| MathSAT5n | 0 | 116 | 102.499 | 102.516 | 116 | 54 | 62 | 0 | 0 | 0 | |
| SMTInterpol | 0 | 116 | 1036.445 | 573.192 | 116 | 54 | 62 | 0 | 0 | 0 | |
| SMTInterpol-fixedn | 0 | 116 | 1065.72 | 575.918 | 116 | 54 | 62 | 0 | 0 | 0 | |
| z3n | 0 | 116 | 621.208 | 621.279 | 116 | 54 | 62 | 0 | 0 | 0 | |
| CVC4 | 0 | 115 | 5085.84 | 5083.408 | 115 | 54 | 61 | 1 | 1 | 0 | |
| Alt-Ergo | 0 | 52 | 78373.52 | 66856.456 | 52 | 0 | 52 | 64 | 51 | 0 | |
| veriT | 0 | 6 | 4.564 | 4.605 | 6 | 0 | 6 | 110 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 54 | 50.187 | 49.181 | 54 | 54 | 0 | 62 | 0 | 0 |
| Yices2-fixedn | 0 | 54 | 61.338 | 61.374 | 54 | 54 | 0 | 62 | 0 | 0 |
| Yices2 | 0 | 54 | 62.478 | 61.507 | 54 | 54 | 0 | 62 | 0 | 0 |
| MathSAT5n | 0 | 54 | 72.117 | 72.127 | 54 | 54 | 0 | 62 | 0 | 0 |
| SMTInterpol | 0 | 54 | 501.103 | 209.542 | 54 | 54 | 0 | 62 | 0 | 0 |
| SMTInterpol-fixedn | 0 | 54 | 526.189 | 210.948 | 54 | 54 | 0 | 62 | 0 | 0 |
| z3n | 0 | 54 | 587.124 | 587.186 | 54 | 54 | 0 | 62 | 0 | 0 |
| CVC4 | 0 | 54 | 2134.205 | 2131.448 | 54 | 54 | 0 | 62 | 1 | 0 |
| veriT | 0 | 0 | 2.503 | 2.505 | 0 | 0 | 0 | 116 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 62758.233 | 53942.881 | 0 | 0 | 0 | 116 | 51 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 62 | 6.036 | 6.41 | 62 | 0 | 62 | 54 | 0 | 0 |
| Yices2 | 0 | 62 | 6.67 | 7.037 | 62 | 0 | 62 | 54 | 0 | 0 |
| Yices2-fixedn | 0 | 62 | 6.705 | 7.174 | 62 | 0 | 62 | 54 | 0 | 0 |
| MathSAT5n | 0 | 62 | 30.381 | 30.388 | 62 | 0 | 62 | 54 | 0 | 0 |
| z3n | 0 | 62 | 34.083 | 34.092 | 62 | 0 | 62 | 54 | 0 | 0 |
| SMTInterpol | 0 | 62 | 535.342 | 363.65 | 62 | 0 | 62 | 54 | 0 | 0 |
| SMTInterpol-fixedn | 0 | 62 | 539.532 | 364.97 | 62 | 0 | 62 | 54 | 0 | 0 |
| CVC4 | 0 | 61 | 2951.635 | 2951.96 | 61 | 0 | 61 | 55 | 1 | 0 |
| Alt-Ergo | 0 | 52 | 15615.287 | 12913.575 | 52 | 0 | 52 | 64 | 51 | 0 |
| veriT | 0 | 6 | 2.061 | 2.1 | 6 | 0 | 6 | 110 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 116 | 56.223 | 55.591 | 116 | 54 | 62 | 0 | 0 | 0 | |
| Yices2 | 0 | 116 | 69.148 | 68.544 | 116 | 54 | 62 | 0 | 0 | 0 | |
| Yices2-fixedn | 0 | 116 | 68.043 | 68.548 | 116 | 54 | 62 | 0 | 0 | 0 | |
| MathSAT5n | 0 | 115 | 98.241 | 98.257 | 115 | 53 | 62 | 1 | 1 | 0 | |
| SMTInterpol | 0 | 110 | 769.866 | 395.522 | 110 | 53 | 57 | 6 | 6 | 0 | |
| SMTInterpol-fixedn | 0 | 110 | 796.708 | 397.289 | 110 | 53 | 57 | 6 | 6 | 0 | |
| z3n | 0 | 107 | 425.375 | 425.413 | 107 | 45 | 62 | 9 | 9 | 0 | |
| CVC4 | 0 | 95 | 617.103 | 613.885 | 95 | 41 | 54 | 21 | 21 | 0 | |
| Alt-Ergo | 0 | 48 | 2152.706 | 1716.808 | 48 | 0 | 48 | 68 | 65 | 0 | |
| veriT | 0 | 6 | 4.564 | 4.605 | 6 | 0 | 6 | 110 | 0 | 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.