The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFBVFP logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 57 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 | 35 | 902.557 | 902.748 | 35 | 9 | 26 | 22 | 21 | 0 |
| Bitwuzla Fixedn | 0 | 35 | 909.984 | 907.243 | 35 | 9 | 26 | 22 | 21 | 0 |
| cvc5 | 0 | 19 | 2738.417 | 3203.178 | 19 | 0 | 19 | 38 | 33 | 0 |
| 2022-z3-4.8.17n | 0 | 7 | 2246.517 | 2246.913 | 7 | 2 | 5 | 50 | 44 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 57 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 35 | 902.557 | 902.748 | 35 | 9 | 26 | 22 | 21 | 0 |
| Bitwuzla Fixedn | 0 | 35 | 909.984 | 907.243 | 35 | 9 | 26 | 22 | 21 | 0 |
| cvc5 | 0 | 19 | 2738.417 | 3203.178 | 19 | 0 | 19 | 38 | 33 | 0 |
| 2022-z3-4.8.17n | 0 | 7 | 2246.517 | 2246.913 | 7 | 2 | 5 | 50 | 44 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 57 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 9 | 212.931 | 212.982 | 9 | 9 | 0 | 0 | 48 | 21 | 0 |
| Bitwuzla Fixedn | 0 | 9 | 216.06 | 213.29 | 9 | 9 | 0 | 0 | 48 | 21 | 0 |
| 2022-z3-4.8.17n | 0 | 2 | 4.031 | 4.028 | 2 | 2 | 0 | 7 | 48 | 44 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 9 | 48 | 33 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 9 | 48 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 26 | 689.626 | 689.765 | 26 | 0 | 26 | 1 | 30 | 21 | 0 |
| Bitwuzla Fixedn | 0 | 26 | 693.924 | 693.954 | 26 | 0 | 26 | 1 | 30 | 21 | 0 |
| cvc5 | 0 | 19 | 2738.417 | 3203.178 | 19 | 0 | 19 | 8 | 30 | 33 | 0 |
| 2022-z3-4.8.17n | 0 | 5 | 2242.486 | 2242.885 | 5 | 0 | 5 | 22 | 30 | 44 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 27 | 30 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 26 | 94.657 | 91.872 | 26 | 7 | 19 | 31 | 31 | 0 |
| Bitwuzla | 0 | 26 | 92.042 | 92.054 | 26 | 7 | 19 | 31 | 31 | 0 |
| cvc5 | 0 | 14 | 120.913 | 120.982 | 14 | 0 | 14 | 43 | 43 | 0 |
| 2022-z3-4.8.17n | 0 | 3 | 9.937 | 9.932 | 3 | 2 | 1 | 54 | 52 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 57 | 16 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.