The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTLIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 277 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 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 196 | 199077.794 | 205137.569 | 196 | 0 | 196 | 81 | 81 | 0 | |
| CVC4 | 0 | 195 | 150008.078 | 152487.472 | 195 | 0 | 195 | 82 | 82 | 0 | |
| Vampire | 0 | 126 | 187106.552 | 183702.459 | 126 | 0 | 126 | 151 | 151 | 0 | |
| Alt-Ergo | 0 | 33 | 293692.395 | 293026.695 | 33 | 0 | 33 | 244 | 244 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 906.745 | 641.357 | 0 | 0 | 0 | 277 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 196 | 203161.694 | 205130.979 | 196 | 0 | 196 | 81 | 81 | 0 | |
| CVC4 | 0 | 195 | 151304.678 | 152483.712 | 195 | 0 | 195 | 82 | 82 | 0 | |
| Vampire | 0 | 127 | 187798.802 | 182993.415 | 127 | 0 | 127 | 150 | 150 | 0 | |
| Alt-Ergo | 0 | 36 | 309733.045 | 290551.208 | 36 | 0 | 36 | 241 | 241 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 906.745 | 641.357 | 0 | 0 | 0 | 277 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 277 | 81 | 0 |
| Alt-Ergo | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 277 | 241 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 277 | 150 | 0 |
| CVC4 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 277 | 82 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 277 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-CVC4n | 0 | 196 | 113161.694 | 115130.979 | 196 | 0 | 196 | 81 | 81 | 0 |
| CVC4 | 0 | 195 | 61304.678 | 62483.712 | 195 | 0 | 195 | 82 | 82 | 0 |
| Vampire | 0 | 127 | 97798.802 | 92993.415 | 127 | 0 | 127 | 150 | 150 | 0 |
| Alt-Ergo | 0 | 36 | 219733.045 | 200551.208 | 36 | 0 | 36 | 241 | 241 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 658.145 | 469.765 | 0 | 0 | 0 | 277 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 113 | 6900.739 | 5551.759 | 113 | 0 | 113 | 164 | 164 | 0 | |
| Alt-Ergo | 0 | 30 | 6037.095 | 5956.844 | 30 | 0 | 30 | 247 | 247 | 0 | |
| CVC4 | 0 | 28 | 6036.972 | 6036.975 | 28 | 0 | 28 | 249 | 249 | 0 | |
| 2019-CVC4n | 0 | 27 | 6050.903 | 6050.897 | 27 | 0 | 27 | 250 | 250 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 906.745 | 641.357 | 0 | 0 | 0 | 277 | 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.