The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFDTLIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 147 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 147 | 23110.799 | 23328.546 | 147 | 93 | 54 | 0 | 0 | 0 | |
| CVC4 | 0 | 147 | 23164.987 | 23515.546 | 147 | 93 | 54 | 0 | 0 | 0 | |
| Vampire | 0 | 54 | 112771.215 | 112020.667 | 54 | 0 | 54 | 93 | 93 | 0 | |
| Alt-Ergo | 0 | 53 | 52229.293 | 49071.433 | 53 | 0 | 53 | 94 | 40 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 482.985 | 341.519 | 0 | 0 | 0 | 147 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 147 | 23110.799 | 23328.546 | 147 | 93 | 54 | 0 | 0 | 0 | |
| CVC4 | 0 | 147 | 23164.987 | 23515.546 | 147 | 93 | 54 | 0 | 0 | 0 | |
| Alt-Ergo | 0 | 54 | 53028.373 | 48374.45 | 54 | 0 | 54 | 93 | 39 | 0 | |
| Vampire | 0 | 54 | 116371.495 | 112003.377 | 54 | 0 | 54 | 93 | 93 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 482.985 | 341.519 | 0 | 0 | 0 | 147 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 93 | 23093.255 | 23310.991 | 93 | 93 | 0 | 54 | 0 | 0 |
| CVC4 | 0 | 93 | 23149.376 | 23499.95 | 93 | 93 | 0 | 54 | 0 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 308.535 | 213.579 | 0 | 0 | 0 | 147 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 46812.671 | 46804.228 | 0 | 0 | 0 | 147 | 39 | 0 |
| Vampire | 0 | 0 | 115200.28 | 111582.71 | 0 | 0 | 0 | 147 | 93 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 54 | 15.611 | 15.595 | 54 | 0 | 54 | 93 | 0 | 0 |
| 2018-CVC4n | 0 | 54 | 17.544 | 17.556 | 54 | 0 | 54 | 93 | 0 | 0 |
| Vampire | 0 | 54 | 1171.215 | 420.667 | 54 | 0 | 54 | 93 | 93 | 0 |
| Alt-Ergo | 0 | 54 | 6215.702 | 1570.222 | 54 | 0 | 54 | 93 | 39 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 174.45 | 127.939 | 0 | 0 | 0 | 147 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 99 | 1181.877 | 1182.282 | 99 | 45 | 54 | 48 | 48 | 0 | |
| 2018-CVC4n | 0 | 99 | 1182.86 | 1182.783 | 99 | 45 | 54 | 48 | 48 | 0 | |
| Vampire | 0 | 49 | 2560.365 | 2447.418 | 49 | 0 | 49 | 98 | 98 | 0 | |
| Alt-Ergo | 0 | 47 | 1126.043 | 1113.98 | 47 | 0 | 47 | 100 | 46 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 482.985 | 341.519 | 0 | 0 | 0 | 147 | 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.