QF_Equality (Single Query Track)
Competition results for the QF_Equality
division
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 3821
Time Limit: 1200 seconds
Memory Limit: 30720 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 | 1646.35 | 2119.78 | 3821 | 1621 | 2200 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 3820 | 7611.09 | 8085.56 | 3820 | 1621 | 2199 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 3819 | 5162.81 | 5633.47 | 3819 | 1621 | 2198 | 2 | 0 | 2 | 0 |
| SMTInterpol | 0 | 3743 | 25386.50 | 11800.75 | 3743 | 1621 | 2122 | 78 | 0 | 24 | 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 | 1646.35 | 2119.78 | 3821 | 1621 | 2200 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 3820 | 7611.09 | 8085.56 | 3820 | 1621 | 2199 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 3819 | 5162.81 | 5633.47 | 3819 | 1621 | 2198 | 2 | 0 | 2 | 0 |
| SMTInterpol | 0 | 3743 | 25386.50 | 11800.75 | 3743 | 1621 | 2122 | 78 | 0 | 24 | 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 | 1621 | 268.99 | 470.12 | 1621 | 1621 | 0 | 0 | 2200 | 0 | 0 |
| OpenSMT | 0 | 1621 | 416.09 | 617.44 | 1621 | 1621 | 0 | 0 | 2200 | 0 | 0 |
| cvc5 | 0 | 1621 | 502.87 | 702.86 | 1621 | 1621 | 0 | 0 | 2200 | 0 | 0 |
| SMTInterpol | 0 | 1621 | 3834.58 | 1832.77 | 1621 | 1621 | 0 | 0 | 2200 | 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 | 2200 | 1377.36 | 1649.66 | 2200 | 0 | 2200 | 0 | 1621 | 0 | 0 |
| OpenSMT | 0 | 2199 | 7195.00 | 7468.13 | 2199 | 0 | 2199 | 1 | 1621 | 1 | 0 |
| cvc5 | 0 | 2198 | 4659.94 | 4930.60 | 2198 | 0 | 2198 | 2 | 1621 | 2 | 0 |
| SMTInterpol | 0 | 2122 | 21551.93 | 9967.99 | 2122 | 0 | 2122 | 78 | 1621 | 24 | 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 | 3818 | 733.61 | 1206.55 | 3818 | 1621 | 2197 | 0 | 3 | 0 | 0 |
| OpenSMT | 0 | 3794 | 2155.86 | 2626.33 | 3794 | 1621 | 2173 | 0 | 27 | 0 | 0 |
| cvc5 | 0 | 3787 | 1941.64 | 2407.95 | 3787 | 1621 | 2166 | 0 | 34 | 0 | 0 |
| SMTInterpol | 0 | 3708 | 19481.10 | 8844.64 | 3708 | 1620 | 2088 | 0 | 113 | 0 | 0 |