QF_UFBV (Single Query Track)
Competition results for the QF_UFBV
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 300
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 | Bitwuzla | 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 | 288 | 11430.144149 | 11461.170549 | 288 | 162 | 126 | 12 | 0 | 9 | 3 |
| cvc5 | 0 | 250 | 25539.183605 | 25570.40723 | 250 | 143 | 107 | 50 | 0 | 32 | 18 |
| Yices2 | 0 | 240 | 34680.868921 | 34711.892203 | 240 | 155 | 85 | 60 | 0 | 59 | 1 |
| Z3-alpha | 0 | 231 | 25700.472333 | 25728.617586 | 231 | 125 | 106 | 69 | 0 | 63 | 2 |
| SMTInterpol | 0 | 96 | 18829.527548 | 14664.88375 | 97 | 70 | 27 | 203 | 0 | 136 | 0 |
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 | 288 | 11430.144149 | 11461.170549 | 288 | 162 | 126 | 12 | 0 | 9 | 3 |
| cvc5 | 0 | 250 | 25539.183605 | 25570.40723 | 250 | 143 | 107 | 50 | 0 | 32 | 18 |
| Yices2 | 0 | 240 | 34680.868921 | 34711.892203 | 240 | 155 | 85 | 60 | 0 | 59 | 1 |
| Z3-alpha | 0 | 231 | 25700.472333 | 25728.617586 | 231 | 125 | 106 | 69 | 0 | 63 | 2 |
| SMTInterpol | 0 | 97 | 20086.519573 | 15829.946898 | 97 | 70 | 27 | 203 | 0 | 136 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 162 | 6112.95715 | 6130.173569 | 162 | 162 | 0 | 2 | 136 | 2 | 0 |
| Yices2 | 0 | 155 | 6288.294878 | 6305.313882 | 155 | 155 | 0 | 9 | 136 | 9 | 0 |
| cvc5 | 0 | 143 | 7211.424456 | 7227.853665 | 143 | 143 | 0 | 21 | 136 | 10 | 11 |
| Z3-alpha | 0 | 125 | 6441.727676 | 6455.291192 | 125 | 125 | 0 | 39 | 136 | 33 | 2 |
| SMTInterpol | 0 | 70 | 16080.458927 | 12673.766581 | 70 | 70 | 0 | 94 | 136 | 38 | 0 |
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 | 126 | 5317.186999 | 5330.99698 | 126 | 0 | 126 | 1 | 173 | 1 | 0 |
| cvc5 | 0 | 107 | 18327.759149 | 18342.553564 | 107 | 0 | 107 | 20 | 173 | 18 | 2 |
| Z3-alpha | 0 | 106 | 19258.744656 | 19273.326394 | 106 | 0 | 106 | 21 | 173 | 21 | 0 |
| Yices2 | 0 | 85 | 28392.574043 | 28406.578321 | 85 | 0 | 85 | 42 | 173 | 41 | 1 |
| SMTInterpol | 0 | 27 | 4006.060646 | 3156.180318 | 27 | 0 | 27 | 100 | 173 | 91 | 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 |
|---|
| Bitwuzla | 0 | 208 | 898.21637 | 919.22916 | 208 | 130 | 78 | 0 | 92 | 0 | 0 |
| Yices2 | 0 | 167 | 252.603214 | 269.340846 | 167 | 129 | 38 | 0 | 133 | 0 | 0 |
| Z3-alpha | 0 | 146 | 454.840607 | 469.533141 | 146 | 105 | 41 | 0 | 154 | 0 | 0 |
| cvc5 | 0 | 132 | 634.232122 | 647.557454 | 132 | 97 | 35 | 0 | 168 | 0 | 0 |
| SMTInterpol | 0 | 24 | 724.459421 | 269.881754 | 24 | 11 | 13 | 4 | 272 | 0 | 0 |