QF_AUFBV (Model Validation Track)
Competition results for the QF_AUFBV
logic
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 25
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| Bitwuzla | Bitwuzla | Bitwuzla | - | Bitwuzla |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 24 | 682.356556 | 684.958289 | 24 | 24 | 0 | 1 | 0 | 0 | 1 |
| cvc5 | 0 | 13 | 1520.561312 | 1522.202864 | 13 | 13 | 0 | 12 | 0 | 10 | 2 |
| SMTInterpol | 0 | 3 | 429.440649 | 380.250857 | 3 | 3 | 0 | 22 | 0 | 15 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 24 | 682.356556 | 684.958289 | 24 | 24 | 0 | 1 | 0 | 0 | 1 |
| cvc5 | 0 | 13 | 1520.561312 | 1522.202864 | 13 | 13 | 0 | 12 | 0 | 10 | 2 |
| SMTInterpol | 0 | 3 | 429.440649 | 380.250857 | 3 | 3 | 0 | 22 | 0 | 15 | 0 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 24 | 682.356556 | 684.958289 | 24 | 24 | 0 | 1 | 0 | 0 | 1 |
| cvc5 | 0 | 13 | 1520.561312 | 1522.202864 | 13 | 13 | 0 | 12 | 0 | 10 | 2 |
| SMTInterpol | 0 | 3 | 429.440649 | 380.250857 | 3 | 3 | 0 | 22 | 0 | 15 | 0 |
24 seconds Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 15 | 22.622016 | 24.141582 | 15 | 15 | 0 | 0 | 10 | 0 | 0 |
| cvc5 | 0 | 10 | 44.995321 | 46.017479 | 10 | 10 | 0 | 0 | 15 | 0 | 0 |
| SMTInterpol | 0 | 2 | 6.104977 | 2.430764 | 2 | 2 | 0 | 6 | 17 | 0 | 0 |