The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the BVFP logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 208 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 193 | 661.381 | 661.555 | 193 | 180 | 13 | 15 | 15 | 0 |
| Bitwuzla Fixedn | 0 | 193 | 673.212 | 673.335 | 193 | 180 | 13 | 15 | 15 | 0 |
| cvc5 | 0 | 175 | 10224.928 | 10452.608 | 175 | 168 | 7 | 33 | 33 | 0 |
| 2022-Bitwuzlan | 0 | 152 | 2003.996 | 2004.39 | 152 | 138 | 14 | 56 | 55 | 0 |
| UltimateEliminator+MathSAT | 0 | 28 | 389.788 | 332.72 | 28 | 28 | 0 | 180 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 193 | 661.381 | 661.555 | 193 | 180 | 13 | 15 | 15 | 0 |
| Bitwuzla Fixedn | 0 | 193 | 673.212 | 673.335 | 193 | 180 | 13 | 15 | 15 | 0 |
| cvc5 | 0 | 175 | 10224.928 | 10452.608 | 175 | 168 | 7 | 33 | 33 | 0 |
| 2022-Bitwuzlan | 0 | 152 | 2003.996 | 2004.39 | 152 | 138 | 14 | 56 | 55 | 0 |
| UltimateEliminator+MathSAT | 0 | 28 | 389.788 | 332.72 | 28 | 28 | 0 | 180 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 180 | 348.642 | 348.737 | 180 | 180 | 0 | 0 | 28 | 15 | 0 |
| Bitwuzla Fixedn | 0 | 180 | 355.834 | 355.914 | 180 | 180 | 0 | 0 | 28 | 15 | 0 |
| cvc5 | 0 | 168 | 8496.472 | 8723.728 | 168 | 168 | 0 | 12 | 28 | 33 | 0 |
| 2022-Bitwuzlan | 0 | 138 | 1641.357 | 1641.69 | 138 | 138 | 0 | 42 | 28 | 55 | 0 |
| UltimateEliminator+MathSAT | 0 | 28 | 389.788 | 332.72 | 28 | 28 | 0 | 152 | 28 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 14 | 362.638 | 362.7 | 14 | 0 | 14 | 0 | 194 | 55 | 0 |
| Bitwuzla | 0 | 13 | 312.74 | 312.818 | 13 | 0 | 13 | 1 | 194 | 15 | 0 |
| Bitwuzla Fixedn | 0 | 13 | 317.378 | 317.421 | 13 | 0 | 13 | 1 | 194 | 15 | 0 |
| cvc5 | 0 | 7 | 1728.456 | 1728.88 | 7 | 0 | 7 | 7 | 194 | 33 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 14 | 194 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 189 | 42.232 | 42.277 | 189 | 179 | 10 | 19 | 19 | 0 |
| Bitwuzla Fixedn | 0 | 189 | 42.325 | 42.366 | 189 | 179 | 10 | 19 | 19 | 0 |
| 2022-Bitwuzlan | 0 | 147 | 93.7 | 93.71 | 147 | 135 | 12 | 61 | 60 | 0 |
| cvc5 | 0 | 138 | 33.102 | 33.06 | 138 | 138 | 0 | 70 | 70 | 0 |
| UltimateEliminator+MathSAT | 0 | 22 | 140.1 | 96.991 | 22 | 22 | 0 | 186 | 6 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.