The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTLIRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 3274 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 2533 | 4953.858 | 4954.825 | 2533 | 69 | 2464 | 741 | 4 | 0 | |
| Alt-Ergo | 0 | 2462 | 138483.55 | 133884.894 | 2462 | 0 | 2462 | 812 | 101 | 4 | |
| UltimateEliminator+MathSAT | 0 | 0 | 10826.928 | 7409.418 | 0 | 0 | 0 | 3274 | 0 | 0 | |
| Vampire | 29 | 2750 | 694675.493 | 628923.599 | 2750 | 10 | 2740 | 524 | 495 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 2533 | 4955.088 | 4954.625 | 2533 | 69 | 2464 | 741 | 4 | 0 | |
| Alt-Ergo | 0 | 2463 | 138826.56 | 133074.278 | 2463 | 0 | 2463 | 811 | 100 | 4 | |
| UltimateEliminator+MathSAT | 0 | 0 | 10826.928 | 7409.418 | 0 | 0 | 0 | 3274 | 0 | 0 | |
| Vampire | 29 | 2751 | 714410.153 | 628462.547 | 2751 | 10 | 2741 | 523 | 494 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 69 | 1.285 | 1.277 | 69 | 69 | 0 | 3205 | 4 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 248.52 | 160.34 | 0 | 0 | 0 | 3274 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 1209.459 | 1203.516 | 0 | 0 | 0 | 3274 | 100 | 4 |
| Vampire | 29 | 10 | 40901.659 | 39381.417 | 10 | 10 | 0 | 3264 | 494 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 2741 | 107107.864 | 40696.82 | 2741 | 0 | 2741 | 533 | 494 | 0 |
| CVC4 | 0 | 2464 | 4940.21 | 4939.792 | 2464 | 0 | 2464 | 810 | 4 | 0 |
| Alt-Ergo | 0 | 2463 | 60897.71 | 57187.223 | 2463 | 0 | 2463 | 811 | 100 | 4 |
| UltimateEliminator+MathSAT | 0 | 0 | 9063.277 | 6214.211 | 0 | 0 | 0 | 3274 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 2533 | 251.088 | 250.625 | 2533 | 69 | 2464 | 741 | 4 | 0 | |
| Alt-Ergo | 0 | 2462 | 4894.803 | 3986.83 | 2462 | 0 | 2462 | 812 | 133 | 4 | |
| UltimateEliminator+MathSAT | 0 | 0 | 10826.928 | 7409.418 | 0 | 0 | 0 | 3274 | 0 | 0 | |
| Vampire | 28 | 2343 | 35296.192 | 29391.507 | 2343 | 0 | 2343 | 931 | 903 | 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.