QF_Equality_Bitvec (Model Validation Track)
Competition results for the QF_Equality_Bitvec
division
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 384
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Yices2 | Yices2 | Yices2 | - | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 383 | 5305.166298 | 5344.689109 | 383 | 383 | 0 | 1 | 0 | 0 | 0 |
| Bitwuzla | 0 | 382 | 1874.783365 | 1913.351616 | 382 | 382 | 0 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 375 | 10443.506063 | 10482.347893 | 375 | 375 | 0 | 9 | 0 | 8 | 1 |
| SMTInterpol | 0 | 303 | 25195.819206 | 18023.58504 | 304 | 304 | 0 | 80 | 0 | 33 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 383 | 5305.166298 | 5344.689109 | 383 | 383 | 0 | 1 | 0 | 0 | 0 |
| Bitwuzla | 0 | 382 | 1874.783365 | 1913.351616 | 382 | 382 | 0 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 375 | 10443.506063 | 10482.347893 | 375 | 375 | 0 | 9 | 0 | 8 | 1 |
| SMTInterpol | 0 | 304 | 26453.542792 | 19184.174197 | 304 | 304 | 0 | 80 | 0 | 33 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 383 | 5305.166298 | 5344.689109 | 383 | 383 | 0 | 1 | 0 | 0 | 0 |
| Bitwuzla | 0 | 382 | 1874.783365 | 1913.351616 | 382 | 382 | 0 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 375 | 10443.506063 | 10482.347893 | 375 | 375 | 0 | 9 | 0 | 8 | 1 |
| SMTInterpol | 0 | 304 | 26453.542792 | 19184.174197 | 304 | 304 | 0 | 80 | 0 | 33 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 370 | 273.834468 | 310.986732 | 370 | 370 | 0 | 0 | 14 | 0 | 0 |
| Bitwuzla | 0 | 361 | 377.634111 | 413.901607 | 361 | 361 | 0 | 0 | 23 | 0 | 0 |
| cvc5 | 0 | 329 | 537.928809 | 570.902568 | 329 | 329 | 0 | 0 | 55 | 0 | 0 |
| SMTInterpol | 0 | 204 | 4472.982103 | 1619.567467 | 204 | 204 | 0 | 1 | 179 | 0 | 0 |