QF_IDL (Single Query Track)
Competition results for the QF_IDL
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 1208
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Z3-alpha | Z3-alpha | Z3-alpha | Z3-alpha | Yices2 |
Sequential 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 | 1047 | 55678.317145 | 55795.358142 | 1047 | 661 | 386 | 161 | 0 | 161 | 0 |
| Yices2 | 0 | 996 | 32416.192725 | 32524.125519 | 996 | 645 | 351 | 212 | 0 | 212 | 0 |
| cvc5 | 0 | 933 | 70249.5933 | 70360.253334 | 933 | 549 | 384 | 275 | 0 | 273 | 2 |
| OpenSMT | 0 | 909 | 54654.611506 | 54758.728101 | 909 | 581 | 328 | 299 | 0 | 299 | 0 |
| SMTInterpol | 0 | 712 | 87239.751962 | 66345.96422 | 721 | 438 | 283 | 487 | 0 | 487 | 0 |
Parallel 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 | 1047 | 55678.317145 | 55795.358142 | 1047 | 661 | 386 | 161 | 0 | 161 | 0 |
| Yices2 | 0 | 996 | 32416.192725 | 32524.125519 | 996 | 645 | 351 | 212 | 0 | 212 | 0 |
| cvc5 | 0 | 933 | 70249.5933 | 70360.253334 | 933 | 549 | 384 | 275 | 0 | 273 | 2 |
| OpenSMT | 0 | 909 | 54654.611506 | 54758.728101 | 909 | 581 | 328 | 299 | 0 | 299 | 0 |
| SMTInterpol | 0 | 721 | 102384.430303 | 73688.271317 | 721 | 438 | 283 | 487 | 0 | 487 | 0 |
SAT 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 | 661 | 35011.605409 | 35085.460443 | 661 | 661 | 0 | 66 | 481 | 66 | 0 |
| Yices2 | 0 | 645 | 20188.56495 | 20258.665732 | 645 | 645 | 0 | 82 | 481 | 82 | 0 |
| OpenSMT | 0 | 581 | 40829.149106 | 40897.42511 | 581 | 581 | 0 | 146 | 481 | 146 | 0 |
| cvc5 | 0 | 549 | 48121.152386 | 48188.061313 | 549 | 549 | 0 | 178 | 481 | 176 | 2 |
| SMTInterpol | 0 | 438 | 69551.383031 | 53589.011136 | 438 | 438 | 0 | 289 | 481 | 289 | 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 | 386 | 20666.711736 | 20709.897699 | 386 | 0 | 386 | 44 | 778 | 44 | 0 |
| cvc5 | 0 | 384 | 22128.440913 | 22172.192021 | 384 | 0 | 384 | 46 | 778 | 46 | 0 |
| Yices2 | 0 | 351 | 12227.627775 | 12265.459787 | 351 | 0 | 351 | 79 | 778 | 79 | 0 |
| OpenSMT | 0 | 328 | 13825.462401 | 13861.302991 | 328 | 0 | 328 | 102 | 778 | 102 | 0 |
| SMTInterpol | 0 | 283 | 32833.047273 | 20099.26018 | 283 | 0 | 283 | 147 | 778 | 147 | 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 |
|---|
| Yices2 | 0 | 874 | 1364.673028 | 1452.249434 | 874 | 571 | 303 | 0 | 334 | 0 | 0 |
| Z3-alpha | 0 | 839 | 2178.626063 | 2262.811218 | 839 | 545 | 294 | 0 | 369 | 0 | 0 |
| OpenSMT | 0 | 629 | 2407.43479 | 2470.753721 | 629 | 352 | 277 | 0 | 579 | 0 | 0 |
| cvc5 | 0 | 615 | 2272.293001 | 2334.201793 | 615 | 325 | 290 | 0 | 593 | 0 | 0 |
| SMTInterpol | 0 | 437 | 5382.126759 | 2344.92673 | 437 | 245 | 192 | 0 | 771 | 0 | 0 |