The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFDTLIRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 4439 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 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3958 | 48357.478 | 48365.813 | 3958 | 0 | 3958 | 481 | 39 | 0 | |
| Alt-Ergo | 0 | 3901 | 319435.455 | 303622.359 | 3901 | 0 | 3901 | 538 | 240 | 7 | |
| Vampire | 0 | 3855 | 1124286.672 | 829911.106 | 3855 | 0 | 3855 | 584 | 584 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 14664.401 | 10027.543 | 0 | 0 | 0 | 4439 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3958 | 48364.678 | 48363.963 | 3958 | 0 | 3958 | 481 | 39 | 0 | |
| Vampire | 0 | 3944 | 1181745.532 | 765629.137 | 3944 | 0 | 3944 | 495 | 495 | 0 | |
| Alt-Ergo | 0 | 3903 | 335611.165 | 297697.372 | 3903 | 0 | 3903 | 536 | 229 | 7 | |
| UltimateEliminator+MathSAT | 0 | 0 | 14664.401 | 10027.543 | 0 | 0 | 0 | 4439 | 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 | 4439 | 229 | 7 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 4439 | 495 | 0 |
| CVC4 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 4439 | 39 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 4439 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3958 | 25544.366 | 25543.67 | 3958 | 0 | 3958 | 481 | 39 | 0 |
| Vampire | 0 | 3944 | 851745.532 | 435629.137 | 3944 | 0 | 3944 | 495 | 495 | 0 |
| Alt-Ergo | 0 | 3903 | 162503.893 | 142199.329 | 3903 | 0 | 3903 | 536 | 229 | 7 |
| UltimateEliminator+MathSAT | 0 | 0 | 13768.725 | 9404.325 | 0 | 0 | 0 | 4439 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3954 | 1391.34 | 1390.38 | 3954 | 0 | 3954 | 485 | 43 | 0 | |
| Alt-Ergo | 0 | 3848 | 11020.172 | 8792.48 | 3848 | 0 | 3848 | 591 | 310 | 7 | |
| Vampire | 0 | 2702 | 46922.612 | 44198.405 | 2702 | 0 | 2702 | 1737 | 1737 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 14664.401 | 10027.543 | 0 | 0 | 0 | 4439 | 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.