QF_Equality (Single Query Track)
Competition results for the QF_Equality
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 3821
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 3821 | 1454.824084 | 1838.067285 | 3821 | 1605 | 2216 | 0 | 0 | 0 | 0 |
| Z3-alpha | 0 | 3821 | 3566.232006 | 3949.159427 | 3821 | 1605 | 2216 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 3820 | 6297.998865 | 6681.107875 | 3820 | 1605 | 2215 | 1 | 0 | 1 | 0 |
| OpenSMT | 0 | 3820 | 6827.404307 | 7212.992338 | 3820 | 1605 | 2215 | 1 | 0 | 1 | 0 |
| SMTInterpol | 0 | 3740 | 31204.391275 | 13548.884086 | 3756 | 1602 | 2154 | 65 | 0 | 60 | 0 |
| plat-smt | 0 | 3512 | 6743.388633 | 7096.204421 | 3512 | 1450 | 2062 | 9 | 300 | 9 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 3821 | 1454.824084 | 1838.067285 | 3821 | 1605 | 2216 | 0 | 0 | 0 | 0 |
| Z3-alpha | 0 | 3821 | 3566.232006 | 3949.159427 | 3821 | 1605 | 2216 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 3820 | 6297.998865 | 6681.107875 | 3820 | 1605 | 2215 | 1 | 0 | 1 | 0 |
| OpenSMT | 0 | 3820 | 6827.404307 | 7212.992338 | 3820 | 1605 | 2215 | 1 | 0 | 1 | 0 |
| SMTInterpol | 0 | 3756 | 63519.320913 | 27133.468522 | 3756 | 1602 | 2154 | 65 | 0 | 60 | 0 |
| plat-smt | 0 | 3512 | 6743.388633 | 7096.204421 | 3512 | 1450 | 2062 | 9 | 300 | 9 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 1605 | 239.865224 | 400.706088 | 1605 | 1605 | 0 | 0 | 2216 | 0 | 0 |
| OpenSMT | 0 | 1605 | 394.655811 | 555.861641 | 1605 | 1605 | 0 | 0 | 2216 | 0 | 0 |
| Z3-alpha | 0 | 1605 | 408.957382 | 569.603308 | 1605 | 1605 | 0 | 0 | 2216 | 0 | 0 |
| cvc5 | 0 | 1605 | 498.414868 | 658.84332 | 1605 | 1605 | 0 | 0 | 2216 | 0 | 0 |
| SMTInterpol | 0 | 1602 | 4238.620016 | 1793.474986 | 1602 | 1602 | 0 | 3 | 2216 | 0 | 0 |
| plat-smt | 0 | 1450 | 302.089867 | 447.218875 | 1450 | 1450 | 0 | 0 | 2371 | 0 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 2216 | 1214.95886 | 1437.361197 | 2216 | 0 | 2216 | 0 | 1605 | 0 | 0 |
| Z3-alpha | 0 | 2216 | 3157.274624 | 3379.556119 | 2216 | 0 | 2216 | 0 | 1605 | 0 | 0 |
| cvc5 | 0 | 2215 | 5799.583997 | 6022.264556 | 2215 | 0 | 2215 | 1 | 1605 | 1 | 0 |
| OpenSMT | 0 | 2215 | 6432.748496 | 6657.130698 | 2215 | 0 | 2215 | 1 | 1605 | 1 | 0 |
| SMTInterpol | 0 | 2154 | 59280.700896 | 25339.993536 | 2154 | 0 | 2154 | 62 | 1605 | 60 | 0 |
| plat-smt | 0 | 2062 | 6441.298766 | 6648.985546 | 2062 | 0 | 2062 | 9 | 1750 | 9 | 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 | 3820 | 674.456795 | 1057.306097 | 3820 | 1605 | 2215 | 0 | 1 | 0 | 0 |
| Z3-alpha | 0 | 3801 | 1907.904056 | 2288.581505 | 3801 | 1605 | 2196 | 0 | 20 | 0 | 0 |
| OpenSMT | 0 | 3785 | 2211.726052 | 2592.346717 | 3785 | 1605 | 2180 | 0 | 36 | 0 | 0 |
| cvc5 | 0 | 3782 | 1899.463946 | 2277.653158 | 3782 | 1605 | 2177 | 0 | 39 | 0 | 0 |
| SMTInterpol | 0 | 3697 | 23602.063912 | 9669.047148 | 3697 | 1602 | 2095 | 0 | 124 | 0 | 0 |
| plat-smt | 0 | 3473 | 1296.137595 | 1643.942785 | 3473 | 1450 | 2023 | 0 | 348 | 0 | 0 |