The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABVFPLRA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:44 +0000
Benchmarks: 25 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | COLIBRI | cvc5 | COLIBRI |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 25 | 401.889 | 401.953 | 25 | 20 | 5 | 0 | 0 | 0 |
| 2021-cvc5n | 0 | 25 | 411.635 | 411.679 | 25 | 20 | 5 | 0 | 0 | 0 |
| COLIBRI | 0 | 24 | 1246.214 | 1238.289 | 24 | 20 | 4 | 1 | 1 | 0 |
| z3-4.8.17n | 0 | 19 | 12329.332 | 12331.488 | 19 | 15 | 4 | 6 | 6 | 0 |
| MathSATn | 0 | 14 | 1214.596 | 1214.988 | 14 | 14 | 0 | 11 | 0 | 0 |
| Bitwuzla | 0 | 9 | 2.31 | 2.441 | 9 | 9 | 0 | 16 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 25 | 401.889 | 401.953 | 25 | 20 | 5 | 0 | 0 | 0 |
| 2021-cvc5n | 0 | 25 | 411.635 | 411.679 | 25 | 20 | 5 | 0 | 0 | 0 |
| COLIBRI | 0 | 24 | 1246.214 | 1238.289 | 24 | 20 | 4 | 1 | 1 | 0 |
| z3-4.8.17n | 0 | 19 | 12330.342 | 12331.198 | 19 | 15 | 4 | 6 | 6 | 0 |
| MathSATn | 0 | 14 | 1214.596 | 1214.988 | 14 | 14 | 0 | 11 | 0 | 0 |
| Bitwuzla | 0 | 9 | 2.31 | 2.441 | 9 | 9 | 0 | 16 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 20 | 30.858 | 22.932 | 20 | 20 | 0 | 0 | 5 | 1 | 0 |
| cvc5 | 0 | 20 | 130.867 | 130.898 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
| 2021-cvc5n | 0 | 20 | 157.807 | 157.823 | 20 | 20 | 0 | 0 | 5 | 0 | 0 |
| z3-4.8.17n | 0 | 15 | 10300.111 | 10300.977 | 15 | 15 | 0 | 5 | 5 | 6 | 0 |
| MathSATn | 0 | 14 | 1213.149 | 1213.536 | 14 | 14 | 0 | 6 | 5 | 0 | 0 |
| Bitwuzla | 0 | 9 | 2.287 | 2.384 | 9 | 9 | 0 | 11 | 5 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2021-cvc5n | 0 | 5 | 253.828 | 253.856 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
| cvc5 | 0 | 5 | 271.022 | 271.056 | 5 | 0 | 5 | 0 | 20 | 0 | 0 |
| COLIBRI | 0 | 4 | 1215.356 | 1215.356 | 4 | 0 | 4 | 1 | 20 | 1 | 0 |
| z3-4.8.17n | 0 | 4 | 2030.231 | 2030.221 | 4 | 0 | 4 | 1 | 20 | 6 | 0 |
| Bitwuzla | 0 | 0 | 0.023 | 0.057 | 0 | 0 | 0 | 5 | 20 | 0 | 0 |
| MathSATn | 0 | 0 | 1.447 | 1.452 | 0 | 0 | 0 | 5 | 20 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 24 | 70.214 | 62.289 | 24 | 20 | 4 | 1 | 1 | 0 |
| 2021-cvc5n | 0 | 21 | 137.812 | 137.817 | 21 | 18 | 3 | 4 | 4 | 0 |
| cvc5 | 0 | 21 | 139.932 | 139.942 | 21 | 18 | 3 | 4 | 4 | 0 |
| MathSATn | 0 | 13 | 48.086 | 48.098 | 13 | 13 | 0 | 12 | 1 | 0 |
| Bitwuzla | 0 | 9 | 2.31 | 2.441 | 9 | 9 | 0 | 16 | 0 | 0 |
| z3-4.8.17n | 0 | 9 | 470.135 | 470.134 | 9 | 8 | 1 | 16 | 16 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.