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 2019-07-23 17:56:09 +0000
Benchmarks: 275 Time Limit: 2400 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 | 275 | 23099.697 | 23380.668 | 275 | 93 | 182 | 0 | 0 | 0 | |
| CVC4 | 0 | 275 | 46216.901 | 46638.225 | 275 | 93 | 182 | 0 | 0 | 0 | |
| Alt-Ergo | 0 | 181 | 111747.563 | 105360.729 | 181 | 0 | 181 | 94 | 43 | 0 | |
| Vampire | 0 | 181 | 230014.351 | 226730.238 | 181 | 0 | 181 | 94 | 94 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 275 | 23099.697 | 23380.668 | 275 | 93 | 182 | 0 | 0 | 0 | |
| CVC4 | 0 | 275 | 46216.901 | 46638.225 | 275 | 93 | 182 | 0 | 0 | 0 | |
| Vampire | 0 | 182 | 245286.341 | 225137.223 | 182 | 0 | 182 | 93 | 93 | 0 | |
| Alt-Ergo | 0 | 181 | 111747.563 | 105360.729 | 181 | 0 | 181 | 94 | 43 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 93 | 23090.726 | 23371.745 | 93 | 93 | 0 | 182 | 0 | 0 |
| CVC4 | 0 | 93 | 46207.251 | 46628.633 | 93 | 93 | 0 | 182 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 100812.65 | 100804.261 | 0 | 0 | 0 | 275 | 43 | 0 |
| Vampire | 0 | 0 | 237600.48 | 223182.29 | 0 | 0 | 0 | 275 | 93 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 182 | 8.971 | 8.923 | 182 | 0 | 182 | 93 | 0 | 0 |
| CVC4 | 0 | 182 | 9.651 | 9.592 | 182 | 0 | 182 | 93 | 0 | 0 |
| Vampire | 0 | 182 | 7685.861 | 1954.933 | 182 | 0 | 182 | 93 | 93 | 0 |
| Alt-Ergo | 0 | 181 | 10934.913 | 4556.468 | 181 | 0 | 181 | 94 | 43 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-CVC4n | 0 | 227 | 1174.469 | 1174.324 | 227 | 45 | 182 | 48 | 48 | 0 | |
| CVC4 | 0 | 227 | 1175.658 | 1175.503 | 227 | 45 | 182 | 48 | 48 | 0 | |
| Alt-Ergo | 0 | 176 | 1214.053 | 1175.023 | 176 | 0 | 176 | 99 | 48 | 0 | |
| Vampire | 0 | 176 | 2869.623 | 2517.603 | 176 | 0 | 176 | 99 | 99 | 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.