The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the FP division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 986 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 | CVC4 |
Note: the division has disagreements
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 813 | 218799.989 | 218835.144 | 813 | 25 | 788 | 173 | 124 | 31 | |
| z3n | 0 | 806 | 224884.275 | 224889.226 | 806 | 24 | 782 | 180 | 163 | 0 | |
| CVC4 | 0 | 680 | 265293.673 | 265346.017 | 680 | 14 | 666 | 306 | 213 | 0 | |
| UltimateEliminator+MathSAT | 0 | 152 | 3352.29 | 2337.127 | 152 | 11 | 141 | 834 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 813 | 218824.549 | 218829.324 | 813 | 25 | 788 | 173 | 124 | 31 | |
| z3n | 0 | 806 | 224915.435 | 224881.636 | 806 | 24 | 782 | 180 | 163 | 0 | |
| CVC4 | 0 | 680 | 265340.503 | 265336.907 | 680 | 14 | 666 | 306 | 213 | 0 | |
| UltimateEliminator+MathSAT | 0 | 152 | 3352.29 | 2337.127 | 152 | 11 | 141 | 834 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 25 | 1437.935 | 1438.218 | 25 | 25 | 0 | 961 | 124 | 31 |
| z3n | 0 | 24 | 2180.437 | 2180.478 | 24 | 24 | 0 | 962 | 163 | 0 |
| CVC4 | 0 | 14 | 13218.915 | 13218.912 | 14 | 14 | 0 | 972 | 213 | 0 |
| UltimateEliminator+MathSAT | 0 | 11 | 90.779 | 68.864 | 11 | 11 | 0 | 975 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 788 | 84142.153 | 84146.644 | 788 | 0 | 788 | 198 | 124 | 31 |
| z3n | 0 | 782 | 91782.797 | 91748.948 | 782 | 0 | 782 | 204 | 163 | 0 |
| CVC4 | 0 | 666 | 109321.587 | 109317.994 | 666 | 0 | 666 | 320 | 213 | 0 |
| UltimateEliminator+MathSAT | 0 | 141 | 2862.78 | 1989.836 | 141 | 0 | 141 | 845 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 699 | 7794.006 | 7783.352 | 699 | 21 | 678 | 287 | 272 | 0 | |
| 2019-Z3n | 0 | 688 | 8210.327 | 8208.945 | 688 | 18 | 670 | 298 | 249 | 31 | |
| CVC4 | 0 | 613 | 7785.67 | 7780.252 | 613 | 14 | 599 | 373 | 280 | 0 | |
| UltimateEliminator+MathSAT | 0 | 152 | 3352.29 | 2337.127 | 152 | 11 | 141 | 834 | 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.