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 2019-07-23 17:56:09 +0000
Benchmarks: 7 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | — | CVC4 | MathSAT-na-ext |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 7 | 583.432 | 583.5 | 7 | 0 | 7 | 0 | 0 | 0 | |
| MathSAT-na-ext | 0 | 7 | 588.174 | 588.162 | 7 | 0 | 7 | 0 | 0 | 0 | |
| MathSAT-default | 0 | 7 | 650.693 | 650.719 | 7 | 0 | 7 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 6 | 2409.807 | 2410.237 | 6 | 0 | 6 | 1 | 1 | 0 | |
| Z3n | 0 | 6 | 2548.144 | 2548.836 | 6 | 0 | 6 | 1 | 1 | 0 | |
| Alt-Ergo | 0 | 5 | 6248.82 | 5164.965 | 5 | 0 | 5 | 2 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 7 | 583.432 | 583.5 | 7 | 0 | 7 | 0 | 0 | 0 | |
| MathSAT-na-ext | 0 | 7 | 588.174 | 588.162 | 7 | 0 | 7 | 0 | 0 | 0 | |
| MathSAT-default | 0 | 7 | 650.693 | 650.719 | 7 | 0 | 7 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 6 | 2410.167 | 2410.167 | 6 | 0 | 6 | 1 | 1 | 0 | |
| Z3n | 0 | 6 | 2548.774 | 2548.816 | 6 | 0 | 6 | 1 | 1 | 0 | |
| Alt-Ergo | 0 | 5 | 6248.82 | 5164.965 | 5 | 0 | 5 | 2 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 1 | 0 |
| Alt-Ergo | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 2 | 0 |
| CVC4 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| MathSAT-default | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| MathSAT-na-ext | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Z3n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 7 | 583.432 | 583.5 | 7 | 0 | 7 | 0 | 0 | 0 |
| MathSAT-na-ext | 0 | 7 | 588.174 | 588.162 | 7 | 0 | 7 | 0 | 0 | 0 |
| MathSAT-default | 0 | 7 | 650.693 | 650.719 | 7 | 0 | 7 | 0 | 0 | 0 |
| 2018-Z3n | 0 | 6 | 2410.167 | 2410.167 | 6 | 0 | 6 | 1 | 1 | 0 |
| Z3n | 0 | 6 | 2548.774 | 2548.816 | 6 | 0 | 6 | 1 | 1 | 0 |
| Alt-Ergo | 0 | 5 | 6248.82 | 5164.965 | 5 | 0 | 5 | 2 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 6 | 34.167 | 34.167 | 6 | 0 | 6 | 1 | 1 | 0 | |
| Z3n | 0 | 5 | 57.166 | 57.166 | 5 | 0 | 5 | 2 | 2 | 0 | |
| MathSAT-na-ext | 0 | 5 | 89.526 | 89.529 | 5 | 0 | 5 | 2 | 2 | 0 | |
| MathSAT-default | 0 | 5 | 102.251 | 102.259 | 5 | 0 | 5 | 2 | 2 | 0 | |
| CVC4 | 0 | 3 | 105.459 | 105.459 | 3 | 0 | 3 | 4 | 4 | 0 | |
| Alt-Ergo | 0 | 3 | 260.75 | 137.629 | 3 | 0 | 3 | 4 | 4 | 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.