QF_BV (Model Validation Track)
Competition results for the QF_BV
logic
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 8215
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| STP | STP | STP | - | STP |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| STP | 0 | 8178 | 57297.084318 | 58127.575467 | 8178 | 8178 | 0 | 37 | 0 | 32 | 0 |
| Bitwuzla | 0 | 8166 | 57488.236948 | 58317.623943 | 8166 | 8166 | 0 | 49 | 0 | 40 | 3 |
| Yices2 | 0 | 8124 | 97925.859938 | 98760.245354 | 8124 | 8124 | 0 | 91 | 0 | 91 | 0 |
| cvc5 | 0 | 7824 | 120629.194128 | 121428.718629 | 7824 | 7824 | 0 | 391 | 0 | 373 | 15 |
| SMTInterpol | 0 | 3951 | 221183.527252 | 189021.068467 | 3960 | 3960 | 0 | 4255 | 0 | 3436 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| STP | 0 | 8178 | 57297.084318 | 58127.575467 | 8178 | 8178 | 0 | 37 | 0 | 32 | 0 |
| Bitwuzla | 0 | 8166 | 57488.236948 | 58317.623943 | 8166 | 8166 | 0 | 49 | 0 | 40 | 3 |
| Yices2 | 0 | 8124 | 97925.859938 | 98760.245354 | 8124 | 8124 | 0 | 91 | 0 | 91 | 0 |
| cvc5 | 0 | 7824 | 120629.194128 | 121428.718629 | 7824 | 7824 | 0 | 391 | 0 | 373 | 15 |
| SMTInterpol | 0 | 3960 | 232371.507225 | 199573.554104 | 3960 | 3960 | 0 | 4255 | 0 | 3436 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| STP | 0 | 8178 | 57297.084318 | 58127.575467 | 8178 | 8178 | 0 | 37 | 0 | 32 | 0 |
| Bitwuzla | 0 | 8166 | 57488.236948 | 58317.623943 | 8166 | 8166 | 0 | 49 | 0 | 40 | 3 |
| Yices2 | 0 | 8124 | 97925.859938 | 98760.245354 | 8124 | 8124 | 0 | 91 | 0 | 91 | 0 |
| cvc5 | 0 | 7824 | 120629.194128 | 121428.718629 | 7824 | 7824 | 0 | 391 | 0 | 373 | 15 |
| SMTInterpol | 0 | 3960 | 232371.507225 | 199573.554104 | 3960 | 3960 | 0 | 4255 | 0 | 3436 | 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 |
|---|
| STP | 0 | 7835 | 11501.346452 | 12287.353546 | 7835 | 7835 | 0 | 0 | 380 | 0 | 0 |
| Bitwuzla | 0 | 7802 | 10269.045206 | 11050.906276 | 7802 | 7802 | 0 | 0 | 413 | 0 | 0 |
| Yices2 | 0 | 7677 | 5406.482586 | 6175.111584 | 7677 | 7677 | 0 | 0 | 538 | 0 | 0 |
| cvc5 | 0 | 7052 | 15988.415247 | 16693.226711 | 7052 | 7052 | 0 | 0 | 1163 | 0 | 0 |
| SMTInterpol | 0 | 3226 | 21593.811779 | 9571.181138 | 3226 | 3226 | 0 | 359 | 4630 | 0 | 0 |