QF_Equality_Bitvec (Single Query Track)
Competition results for the QF_Equality_Bitvec
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 8025
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | Yices2 |
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 | 7905 | 30492.688824 | 31289.831894 | 7905 | 5415 | 2490 | 44 | 76 | 38 | 5 |
| Yices2 | 0 | 7836 | 54048.81765 | 54843.667354 | 7836 | 5401 | 2435 | 113 | 76 | 110 | 2 |
| SMTInterpol | 0 | 6580 | 513934.543045 | 438318.073979 | 6586 | 4400 | 2186 | 1439 | 0 | 1260 | 0 |
| Z3-alpha | 0 | 289 | 29722.660528 | 29757.500041 | 289 | 141 | 148 | 86 | 7650 | 78 | 4 |
| cvc5 | 1 | 7783 | 54832.00586 | 55621.98747 | 7784 | 5367 | 2417 | 241 | 0 | 210 | 30 |
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 | 7905 | 30492.688824 | 31289.831894 | 7905 | 5415 | 2490 | 44 | 76 | 38 | 5 |
| Yices2 | 0 | 7836 | 54048.81765 | 54843.667354 | 7836 | 5401 | 2435 | 113 | 76 | 110 | 2 |
| SMTInterpol | 0 | 6586 | 521349.841714 | 445373.053786 | 6586 | 4400 | 2186 | 1439 | 0 | 1260 | 0 |
| Z3-alpha | 0 | 289 | 29722.660528 | 29757.500041 | 289 | 141 | 148 | 86 | 7650 | 78 | 4 |
| cvc5 | 1 | 7783 | 54832.00586 | 55621.98747 | 7784 | 5367 | 2417 | 241 | 0 | 210 | 30 |
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 | 5415 | 10604.906258 | 11147.676785 | 5415 | 5415 | 0 | 8 | 2602 | 5 | 2 |
| Yices2 | 0 | 5401 | 16517.491708 | 17061.229049 | 5401 | 5401 | 0 | 22 | 2602 | 20 | 1 |
| cvc5 | 0 | 5331 | 21675.56698 | 22212.932744 | 5331 | 5331 | 0 | 102 | 2592 | 86 | 15 |
| SMTInterpol | 0 | 4400 | 384293.473541 | 326389.378865 | 4400 | 4400 | 0 | 1033 | 2592 | 883 | 0 |
| Z3-alpha | 0 | 141 | 8201.469617 | 8216.843842 | 141 | 141 | 0 | 48 | 7836 | 42 | 2 |
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 | 2490 | 19887.782565 | 20142.155109 | 2490 | 0 | 2490 | 23 | 5512 | 23 | 0 |
| Yices2 | 0 | 2435 | 37531.325942 | 37782.438305 | 2435 | 0 | 2435 | 78 | 5512 | 77 | 1 |
| SMTInterpol | 0 | 2186 | 137056.368173 | 118983.674921 | 2186 | 0 | 2186 | 330 | 5509 | 318 | 0 |
| Z3-alpha | 0 | 148 | 21521.190911 | 21540.656199 | 148 | 0 | 148 | 25 | 7852 | 24 | 1 |
| cvc5 | 1 | 2414 | 26850.137001 | 27096.798436 | 2415 | 1 | 2414 | 101 | 5509 | 96 | 5 |
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 | 7680 | 2324.368786 | 3092.364829 | 7680 | 5326 | 2354 | 1 | 344 | 0 | 0 |
| Bitwuzla | 0 | 7622 | 3111.934068 | 3873.829311 | 7622 | 5349 | 2273 | 1 | 402 | 0 | 0 |
| cvc5 | 0 | 7458 | 5849.179648 | 6593.844029 | 7458 | 5212 | 2246 | 1 | 566 | 0 | 0 |
| SMTInterpol | 0 | 5032 | 28631.809158 | 11700.074801 | 5032 | 3266 | 1766 | 56 | 2937 | 0 | 0 |
| Z3-alpha | 0 | 195 | 551.423578 | 571.03195 | 195 | 119 | 76 | 0 | 7830 | 0 | 0 |