QF_Datatypes (Single Query Track)
Competition results for the QF_Datatypes
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 552
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Algaroba | Algaroba | cvc5 | Z3-alpha | Algaroba |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Algaroba | 0 | 333 | 55824.509836 | 55875.297606 | 333 | 120 | 213 | 219 | 0 | 219 | 0 |
| cvc5 | 0 | 326 | 81847.631657 | 81908.634224 | 326 | 122 | 204 | 226 | 0 | 226 | 0 |
| Z3-alpha | 0 | 322 | 90552.656871 | 90614.203436 | 322 | 38 | 284 | 230 | 0 | 230 | 0 |
| SMTInterpol | 0 | 199 | 41546.305193 | 25750.119048 | 221 | 31 | 190 | 331 | 0 | 329 | 2 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Algaroba | 0 | 333 | 55824.509836 | 55875.297606 | 333 | 120 | 213 | 219 | 0 | 219 | 0 |
| cvc5 | 0 | 326 | 81847.631657 | 81908.634224 | 326 | 122 | 204 | 226 | 0 | 226 | 0 |
| Z3-alpha | 0 | 322 | 90552.656871 | 90614.203436 | 322 | 38 | 284 | 230 | 0 | 230 | 0 |
| SMTInterpol | 0 | 221 | 78434.36746 | 45992.205033 | 221 | 31 | 190 | 331 | 0 | 329 | 2 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 122 | 15452.125794 | 15470.66373 | 122 | 122 | 0 | 27 | 403 | 27 | 0 |
| Algaroba | 0 | 120 | 8068.455924 | 8083.317698 | 120 | 120 | 0 | 29 | 403 | 29 | 0 |
| Z3-alpha | 0 | 38 | 23080.879687 | 23092.266752 | 38 | 38 | 0 | 111 | 403 | 111 | 0 |
| SMTInterpol | 0 | 31 | 9504.491268 | 7859.718174 | 31 | 31 | 0 | 118 | 403 | 118 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 284 | 67471.777184 | 67521.936683 | 284 | 0 | 284 | 45 | 223 | 45 | 0 |
| Algaroba | 0 | 213 | 47756.053912 | 47791.979908 | 213 | 0 | 213 | 116 | 223 | 116 | 0 |
| cvc5 | 0 | 204 | 66395.505863 | 66437.970495 | 204 | 0 | 204 | 125 | 223 | 125 | 0 |
| SMTInterpol | 0 | 190 | 68929.876192 | 38132.486859 | 190 | 0 | 190 | 139 | 223 | 137 | 2 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Algaroba | 0 | 166 | 890.302363 | 907.46217 | 166 | 56 | 110 | 0 | 386 | 0 | 0 |
| SMTInterpol | 0 | 108 | 1050.286773 | 440.415569 | 108 | 10 | 98 | 0 | 444 | 0 | 0 |
| cvc5 | 0 | 97 | 371.951713 | 381.884146 | 97 | 28 | 69 | 0 | 455 | 0 | 0 |
| Z3-alpha | 0 | 89 | 226.531785 | 235.598513 | 89 | 3 | 86 | 0 | 463 | 0 | 0 |