The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BVFPLRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 168 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | COLIBRI | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT5n | 0 | 157 | 17910.12 | 17913.441 | 157 | 116 | 41 | 11 | 11 | 0 | |
| CVC4 | 0 | 153 | 23735.41 | 23738.077 | 153 | 113 | 40 | 15 | 15 | 0 | |
| COLIBRI | 0 | 138 | 22978.842 | 22980.905 | 138 | 95 | 43 | 30 | 19 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT5n | 0 | 157 | 17912.24 | 17913.001 | 157 | 116 | 41 | 11 | 11 | 0 | |
| CVC4 | 0 | 153 | 23736.93 | 23737.577 | 153 | 113 | 40 | 15 | 15 | 0 | |
| COLIBRI | 0 | 138 | 22980.132 | 22980.485 | 138 | 95 | 43 | 30 | 19 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| MathSAT5n | 0 | 116 | 1642.889 | 1643.075 | 116 | 116 | 0 | 52 | 11 | 0 |
| CVC4 | 0 | 113 | 5036.349 | 5036.542 | 113 | 113 | 0 | 55 | 15 | 0 |
| COLIBRI | 0 | 95 | 14494.86 | 14495.088 | 95 | 95 | 0 | 73 | 19 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 43 | 8485.272 | 8485.396 | 43 | 0 | 43 | 125 | 19 | 0 |
| MathSAT5n | 0 | 41 | 16269.351 | 16269.925 | 41 | 0 | 41 | 127 | 11 | 0 |
| CVC4 | 0 | 40 | 18700.58 | 18701.035 | 40 | 0 | 40 | 128 | 15 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 142 | 724.302 | 724.31 | 142 | 108 | 34 | 26 | 26 | 0 | |
| MathSAT5n | 0 | 142 | 774.081 | 774.131 | 142 | 108 | 34 | 26 | 26 | 0 | |
| COLIBRI | 0 | 137 | 635.445 | 635.791 | 137 | 95 | 42 | 31 | 20 | 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.