QF_UFIDL (Single Query Track)
Competition results for the QF_UFIDL
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | OpenSMT | OpenSMT | OpenSMT |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 273 | 20638.16 | 20675.06 | 273 | 100 | 173 | 27 | 0 | 27 | 0 |
| cvc5 | 0 | 237 | 27640.78 | 27674.46 | 237 | 87 | 150 | 63 | 0 | 63 | 0 |
| Yices2 | 0 | 227 | 15279.35 | 15309.39 | 227 | 70 | 157 | 73 | 0 | 73 | 0 |
| SMTInterpol | 0 | 205 | 5793.79 | 3783.10 | 205 | 91 | 114 | 95 | 0 | 81 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 273 | 20638.16 | 20675.06 | 273 | 100 | 173 | 27 | 0 | 27 | 0 |
| cvc5 | 0 | 237 | 27640.78 | 27674.46 | 237 | 87 | 150 | 63 | 0 | 63 | 0 |
| Yices2 | 0 | 227 | 15279.35 | 15309.39 | 227 | 70 | 157 | 73 | 0 | 73 | 0 |
| SMTInterpol | 0 | 205 | 5793.79 | 3783.10 | 205 | 91 | 114 | 95 | 0 | 81 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 100 | 3479.67 | 3492.61 | 100 | 100 | 0 | 4 | 196 | 4 | 0 |
| SMTInterpol | 0 | 91 | 3079.54 | 2445.14 | 91 | 91 | 0 | 13 | 196 | 13 | 0 |
| cvc5 | 0 | 87 | 10294.54 | 10306.96 | 87 | 87 | 0 | 17 | 196 | 17 | 0 |
| Yices2 | 0 | 70 | 6918.15 | 6927.81 | 70 | 70 | 0 | 34 | 196 | 34 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 173 | 17158.49 | 17182.45 | 173 | 0 | 173 | 23 | 104 | 23 | 0 |
| Yices2 | 0 | 157 | 8361.20 | 8381.58 | 157 | 0 | 157 | 39 | 104 | 39 | 0 |
| cvc5 | 0 | 150 | 17346.23 | 17367.50 | 150 | 0 | 150 | 46 | 104 | 46 | 0 |
| SMTInterpol | 0 | 114 | 2714.25 | 1337.96 | 114 | 0 | 114 | 82 | 104 | 68 | 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 |
|---|
| OpenSMT | 0 | 194 | 642.96 | 667.08 | 194 | 82 | 112 | 0 | 106 | 0 | 0 |
| SMTInterpol | 0 | 188 | 2154.22 | 926.26 | 188 | 84 | 104 | 0 | 112 | 0 | 0 |
| Yices2 | 0 | 186 | 142.78 | 165.66 | 186 | 53 | 133 | 0 | 114 | 0 | 0 |
| cvc5 | 0 | 146 | 363.77 | 381.69 | 146 | 52 | 94 | 0 | 154 | 0 | 0 |