The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the ABV logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 2487 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 896 | 30896.198 | 32020.04 | 896 | 413 | 483 | 1591 | 750 | 0 |
| 2022-z3-4.8.17n | 0 | 350 | 1420.957 | 1420.571 | 350 | 338 | 12 | 2137 | 136 | 0 |
| Bitwuzla Fixedn | 0 | 51 | 1.334 | 1.355 | 51 | 31 | 20 | 2436 | 47 | 0 |
| Bitwuzla | 0 | 51 | 1.353 | 1.374 | 51 | 31 | 20 | 2436 | 47 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 60.835 | 32.324 | 9 | 1 | 8 | 2478 | 1 | 1 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 106 | 2267.606 | 1364.754 | 106 | 21 | 85 | 2381 | 490 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 896 | 30896.198 | 32020.04 | 896 | 413 | 483 | 1591 | 750 | 0 |
| 2022-z3-4.8.17n | 0 | 350 | 1420.957 | 1420.571 | 350 | 338 | 12 | 2137 | 136 | 0 |
| Bitwuzla Fixedn | 0 | 51 | 1.334 | 1.355 | 51 | 31 | 20 | 2436 | 47 | 0 |
| Bitwuzla | 0 | 51 | 1.353 | 1.374 | 51 | 31 | 20 | 2436 | 47 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 60.835 | 32.324 | 9 | 1 | 8 | 2478 | 1 | 1 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 106 | 2267.606 | 1364.754 | 106 | 21 | 85 | 2381 | 439 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 413 | 29321.474 | 30443.737 | 413 | 413 | 0 | 242 | 1832 | 750 | 0 |
| 2022-z3-4.8.17n | 0 | 338 | 935.126 | 934.651 | 338 | 338 | 0 | 317 | 1832 | 136 | 0 |
| Bitwuzla | 0 | 31 | 0.414 | 0.429 | 31 | 31 | 0 | 624 | 1832 | 47 | 0 |
| Bitwuzla Fixedn | 0 | 31 | 0.416 | 0.431 | 31 | 31 | 0 | 624 | 1832 | 47 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 12.14 | 7.103 | 1 | 1 | 0 | 654 | 1832 | 1 | 1 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 21 | 1078.287 | 888.47 | 21 | 21 | 0 | 634 | 1832 | 439 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 483 | 1574.725 | 1576.302 | 483 | 0 | 483 | 1 | 2003 | 750 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 85 | 1189.319 | 476.284 | 85 | 0 | 85 | 399 | 2003 | 439 | 0 |
| Bitwuzla Fixedn | 0 | 20 | 0.918 | 0.924 | 20 | 0 | 20 | 464 | 2003 | 47 | 0 |
| Bitwuzla | 0 | 20 | 0.94 | 0.944 | 20 | 0 | 20 | 464 | 2003 | 47 | 0 |
| 2022-z3-4.8.17n | 0 | 12 | 485.831 | 485.92 | 12 | 0 | 12 | 472 | 2003 | 136 | 0 |
| UltimateEliminator+MathSAT | 0 | 8 | 48.695 | 25.221 | 8 | 0 | 8 | 476 | 2003 | 1 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 754 | 903.307 | 886.723 | 754 | 284 | 470 | 1733 | 1678 | 0 |
| 2022-z3-4.8.17n | 0 | 346 | 67.154 | 66.548 | 346 | 335 | 11 | 2141 | 157 | 0 |
| Bitwuzla Fixedn | 0 | 51 | 1.334 | 1.355 | 51 | 31 | 20 | 2436 | 47 | 0 |
| Bitwuzla | 0 | 51 | 1.353 | 1.374 | 51 | 31 | 20 | 2436 | 47 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 60.835 | 32.324 | 9 | 1 | 8 | 2478 | 3 | 1 |
| UltimateIntBlastingWrapper+SMTInterpol | 7 | 104 | 1422.978 | 540.83 | 104 | 20 | 84 | 2383 | 607 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.