QF_BV (Single Query Track)
Competition results for the QF_BV
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 10703
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Bitwuzla | Bitwuzla | STP | Bitwuzla | Bitwuzla |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 10489 | 136684.154526 | 137761.630559 | 10489 | 4907 | 5582 | 214 | 0 | 211 | 3 |
| STP | 0 | 10488 | 169828.228527 | 170916.15918 | 10488 | 4919 | 5569 | 215 | 0 | 212 | 0 |
| Yices2 | 0 | 10388 | 142271.512368 | 143339.280115 | 10388 | 4862 | 5526 | 315 | 0 | 312 | 3 |
| cvc5 | 0 | 9958 | 365361.544544 | 366433.45916 | 9958 | 4773 | 5185 | 745 | 0 | 712 | 32 |
| Z3-alpha | 0 | 9020 | 391942.581441 | 392924.173499 | 9020 | 4427 | 4593 | 1683 | 0 | 1664 | 9 |
| SMTInterpol | 0 | 3339 | 552128.65738 | 442522.52297 | 3548 | 842 | 2706 | 7155 | 0 | 6317 | 134 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 10489 | 136684.154526 | 137761.630559 | 10489 | 4907 | 5582 | 214 | 0 | 211 | 3 |
| STP | 0 | 10488 | 169828.228527 | 170916.15918 | 10488 | 4919 | 5569 | 215 | 0 | 212 | 0 |
| Yices2 | 0 | 10388 | 142271.512368 | 143339.280115 | 10388 | 4862 | 5526 | 315 | 0 | 312 | 3 |
| cvc5 | 0 | 9958 | 365361.544544 | 366433.45916 | 9958 | 4773 | 5185 | 745 | 0 | 712 | 32 |
| Z3-alpha | 0 | 9020 | 391942.581441 | 392924.173499 | 9020 | 4427 | 4593 | 1683 | 0 | 1664 | 9 |
| SMTInterpol | 0 | 3548 | 852576.881037 | 651070.952027 | 3548 | 842 | 2706 | 7155 | 0 | 6317 | 134 |
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 | 4919 | 58214.949551 | 58719.496163 | 4919 | 4919 | 0 | 38 | 5746 | 35 | 0 |
| Bitwuzla | 0 | 4907 | 64503.779278 | 65008.447599 | 4907 | 4907 | 0 | 50 | 5746 | 48 | 2 |
| Yices2 | 0 | 4862 | 64401.745312 | 64902.948059 | 4862 | 4862 | 0 | 95 | 5746 | 92 | 3 |
| cvc5 | 0 | 4773 | 125866.620821 | 126372.253722 | 4773 | 4773 | 0 | 184 | 5746 | 170 | 13 |
| Z3-alpha | 0 | 4427 | 187187.975681 | 187666.416901 | 4427 | 4427 | 0 | 530 | 5746 | 527 | 3 |
| SMTInterpol | 0 | 842 | 161463.213932 | 143147.058681 | 842 | 842 | 0 | 4115 | 5746 | 3454 | 104 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 5582 | 72180.375248 | 72753.18296 | 5582 | 0 | 5582 | 75 | 5046 | 74 | 1 |
| STP | 0 | 5569 | 111613.278976 | 112196.663017 | 5569 | 0 | 5569 | 88 | 5046 | 88 | 0 |
| Yices2 | 0 | 5526 | 77869.767056 | 78436.332056 | 5526 | 0 | 5526 | 131 | 5046 | 131 | 0 |
| cvc5 | 0 | 5185 | 239494.923723 | 240061.205438 | 5185 | 0 | 5185 | 472 | 5046 | 457 | 15 |
| Z3-alpha | 0 | 4593 | 204754.60576 | 205257.756598 | 4593 | 0 | 4593 | 1064 | 5046 | 1049 | 5 |
| SMTInterpol | 0 | 2706 | 691113.667105 | 507923.893346 | 2706 | 0 | 2706 | 2951 | 5046 | 2793 | 22 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 9778 | 17874.335067 | 18855.879781 | 9778 | 4523 | 5255 | 0 | 925 | 0 | 0 |
| Yices2 | 0 | 9743 | 11024.846841 | 12001.68132 | 9743 | 4482 | 5261 | 0 | 960 | 0 | 0 |
| STP | 0 | 9035 | 23227.666979 | 24136.900221 | 9035 | 4581 | 4454 | 0 | 1668 | 0 | 0 |
| cvc5 | 0 | 8353 | 27196.665426 | 28037.397159 | 8353 | 3966 | 4387 | 0 | 2350 | 0 | 0 |
| Z3-alpha | 0 | 7170 | 15231.434193 | 15953.982852 | 7170 | 3580 | 3590 | 0 | 3533 | 0 | 0 |
| SMTInterpol | 0 | 2037 | 32731.166151 | 13363.052275 | 2037 | 392 | 1645 | 362 | 8304 | 0 | 0 |