The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTNIRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 736 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | Vampire | — | Vampire | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 659 | 20491.701 | 20496.183 | 659 | 0 | 659 | 77 | 17 | 0 | |
| Alt-Ergo | 0 | 655 | 83181.955 | 80275.433 | 655 | 0 | 655 | 81 | 66 | 0 | |
| Vampire | 0 | 634 | 234147.216 | 155074.081 | 634 | 0 | 634 | 102 | 102 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 2431.864 | 1686.078 | 0 | 0 | 0 | 736 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 673 | 272515.256 | 130248.706 | 673 | 0 | 673 | 63 | 63 | 0 | |
| CVC4 | 0 | 659 | 20495.321 | 20495.173 | 659 | 0 | 659 | 77 | 17 | 0 | |
| Alt-Ergo | 0 | 659 | 88984.895 | 78151.139 | 659 | 0 | 659 | 77 | 62 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 2431.864 | 1686.078 | 0 | 0 | 0 | 736 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Alt-Ergo | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 736 | 62 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 736 | 63 | 0 |
| CVC4 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 736 | 17 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 736 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 673 | 248515.256 | 106248.706 | 673 | 0 | 673 | 63 | 63 | 0 |
| CVC4 | 0 | 659 | 16894.128 | 16893.978 | 659 | 0 | 659 | 77 | 17 | 0 |
| Alt-Ergo | 0 | 659 | 75782.562 | 64950.312 | 659 | 0 | 659 | 77 | 62 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 2367.315 | 1641.792 | 0 | 0 | 0 | 736 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 659 | 503.321 | 503.173 | 659 | 0 | 659 | 77 | 17 | 0 | |
| Alt-Ergo | 0 | 649 | 2457.955 | 1982.62 | 649 | 0 | 649 | 87 | 72 | 0 | |
| Vampire | 0 | 299 | 12033.841 | 11295.428 | 299 | 0 | 299 | 437 | 437 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 2452.587 | 1684.968 | 0 | 0 | 0 | 736 | 1 | 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.