The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the NIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 17 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | Vampire | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 16 | 391.879 | 391.914 | 16 | 12 | 4 | 1 | 0 | 0 | |
| z3n | 0 | 15 | 578.667 | 578.884 | 15 | 12 | 3 | 2 | 0 | 0 | |
| CVC4 | 0 | 12 | 3069.886 | 3127.545 | 12 | 11 | 1 | 5 | 2 | 0 | |
| UltimateEliminator+MathSAT | 0 | 8 | 84.403 | 47.826 | 8 | 7 | 1 | 9 | 0 | 0 | |
| Vampire | 0 | 4 | 15993.967 | 15701.64 | 4 | 0 | 4 | 13 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 16 | 391.879 | 391.914 | 16 | 12 | 4 | 1 | 0 | 0 | |
| z3n | 0 | 15 | 578.667 | 578.884 | 15 | 12 | 3 | 2 | 0 | 0 | |
| CVC4 | 0 | 12 | 3127.316 | 3127.415 | 12 | 11 | 1 | 5 | 2 | 0 | |
| UltimateEliminator+MathSAT | 0 | 8 | 84.403 | 47.826 | 8 | 7 | 1 | 9 | 0 | 0 | |
| Vampire | 0 | 4 | 15993.967 | 15701.64 | 4 | 0 | 4 | 13 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 12 | 0.673 | 0.674 | 12 | 12 | 0 | 5 | 0 | 0 |
| z3n | 0 | 12 | 0.74 | 0.74 | 12 | 12 | 0 | 5 | 0 | 0 |
| CVC4 | 0 | 11 | 696.05 | 696.077 | 11 | 11 | 0 | 6 | 2 | 0 |
| UltimateEliminator+MathSAT | 0 | 7 | 57.101 | 33.617 | 7 | 7 | 0 | 10 | 0 | 0 |
| Vampire | 0 | 0 | 14400.0 | 14400.0 | 0 | 0 | 0 | 17 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 4 | 391.206 | 391.24 | 4 | 0 | 4 | 13 | 0 | 0 |
| Vampire | 0 | 4 | 1593.967 | 1301.64 | 4 | 0 | 4 | 13 | 13 | 0 |
| z3n | 0 | 3 | 577.928 | 578.144 | 3 | 0 | 3 | 14 | 0 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 27.302 | 14.209 | 1 | 0 | 1 | 16 | 0 | 0 |
| CVC4 | 0 | 1 | 2431.266 | 2431.337 | 1 | 0 | 1 | 16 | 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 | 16 | 25.433 | 25.434 | 16 | 12 | 4 | 1 | 1 | 0 | |
| z3n | 0 | 15 | 49.324 | 49.325 | 15 | 12 | 3 | 2 | 2 | 0 | |
| CVC4 | 0 | 10 | 123.266 | 123.271 | 10 | 9 | 1 | 7 | 5 | 0 | |
| UltimateEliminator+MathSAT | 0 | 8 | 84.403 | 47.826 | 8 | 7 | 1 | 9 | 0 | 0 | |
| Vampire | 0 | 3 | 338.507 | 338.593 | 3 | 0 | 3 | 14 | 14 | 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.