The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABVFPLRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 71 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 | COLIBRI |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 70 | 2081.345 | 2081.878 | 70 | 68 | 2 | 1 | 1 | 0 | |
| COLIBRI | 0 | 68 | 111.089 | 111.602 | 68 | 67 | 1 | 3 | 0 | 0 | |
| MathSAT5n | 0 | 62 | 1222.851 | 1223.797 | 62 | 62 | 0 | 9 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 70 | 2081.555 | 2081.858 | 70 | 68 | 2 | 1 | 1 | 0 | |
| COLIBRI | 0 | 68 | 111.089 | 111.602 | 68 | 67 | 1 | 3 | 0 | 0 | |
| MathSAT5n | 0 | 62 | 1223.711 | 1223.747 | 62 | 62 | 0 | 9 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 68 | 1291.416 | 1291.456 | 68 | 68 | 0 | 3 | 1 | 0 |
| COLIBRI | 0 | 67 | 88.697 | 88.784 | 67 | 67 | 0 | 4 | 0 | 0 |
| MathSAT5n | 0 | 62 | 1223.595 | 1223.631 | 62 | 62 | 0 | 9 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 2 | 790.138 | 790.402 | 2 | 0 | 2 | 69 | 1 | 0 |
| COLIBRI | 0 | 1 | 22.392 | 22.818 | 1 | 0 | 1 | 70 | 0 | 0 |
| MathSAT5n | 0 | 0 | 0.116 | 0.116 | 0 | 0 | 0 | 71 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 67 | 89.054 | 89.564 | 67 | 66 | 1 | 4 | 1 | 0 | |
| CVC4 | 0 | 67 | 145.191 | 145.216 | 67 | 67 | 0 | 4 | 4 | 0 | |
| MathSAT5n | 0 | 62 | 47.711 | 47.747 | 62 | 62 | 0 | 9 | 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.