The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ANIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 94 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 89 | 6884.769 | 6886.772 | 89 | 82 | 7 | 5 | 5 | 0 | |
| CVC4 | 0 | 89 | 7275.399 | 7277.403 | 89 | 82 | 7 | 5 | 5 | 0 | |
| MathSAT5n | 0 | 87 | 617.902 | 617.926 | 87 | 80 | 7 | 7 | 0 | 0 | |
| z3n | 0 | 55 | 51092.496 | 51096.808 | 55 | 48 | 7 | 39 | 39 | 0 | |
| Alt-Ergo | 0 | 5 | 6288.931 | 3497.395 | 5 | 0 | 5 | 89 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 89 | 6886.349 | 6886.612 | 89 | 82 | 7 | 5 | 5 | 0 | |
| CVC4 | 0 | 89 | 7276.739 | 7277.173 | 89 | 82 | 7 | 5 | 5 | 0 | |
| MathSAT5n | 0 | 87 | 617.902 | 617.926 | 87 | 80 | 7 | 7 | 0 | 0 | |
| z3n | 0 | 55 | 51098.086 | 51095.028 | 55 | 48 | 7 | 39 | 39 | 0 | |
| Alt-Ergo | 0 | 5 | 6288.931 | 3497.395 | 5 | 0 | 5 | 89 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 82 | 5182.32 | 5182.416 | 82 | 82 | 0 | 12 | 5 | 0 |
| CVC4 | 0 | 82 | 5706.432 | 5706.748 | 82 | 82 | 0 | 12 | 5 | 0 |
| MathSAT5n | 0 | 80 | 22.1 | 22.106 | 80 | 80 | 0 | 14 | 0 | 0 |
| z3n | 0 | 48 | 49869.038 | 49865.974 | 48 | 48 | 0 | 46 | 39 | 0 |
| Alt-Ergo | 0 | 0 | 2551.6 | 762.06 | 0 | 0 | 0 | 94 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT5n | 0 | 7 | 595.803 | 595.82 | 7 | 0 | 7 | 87 | 0 | 0 |
| z3n | 0 | 7 | 1229.048 | 1229.053 | 7 | 0 | 7 | 87 | 39 | 0 |
| CVC4 | 0 | 7 | 1570.307 | 1570.425 | 7 | 0 | 7 | 87 | 5 | 0 |
| 2019-CVC4n | 0 | 7 | 1704.028 | 1704.196 | 7 | 0 | 7 | 87 | 5 | 0 |
| Alt-Ergo | 0 | 5 | 3737.331 | 2735.335 | 5 | 0 | 5 | 89 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT5n | 0 | 83 | 129.641 | 129.649 | 83 | 80 | 3 | 11 | 4 | 0 | |
| 2019-CVC4n | 0 | 81 | 451.572 | 451.569 | 81 | 78 | 3 | 13 | 13 | 0 | |
| CVC4 | 0 | 81 | 465.638 | 465.71 | 81 | 78 | 3 | 13 | 13 | 0 | |
| z3n | 0 | 43 | 1278.686 | 1274.934 | 43 | 36 | 7 | 51 | 51 | 0 | |
| Alt-Ergo | 0 | 3 | 1015.337 | 395.973 | 3 | 0 | 3 | 91 | 6 | 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.