QF_Equality_NonLinearArith (Single Query Track)
Competition results for the QF_Equality_NonLinearArith
division
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 631
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 | cvc5 | 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 | 450 | 15859.71 | 15917.97 | 450 | 376 | 74 | 101 | 80 | 99 | 2 |
| cvc5 | 0 | 381 | 28356.84 | 28407.67 | 381 | 296 | 85 | 250 | 0 | 250 | 0 |
| SMTInterpol | 0 | 306 | 25908.44 | 22972.61 | 306 | 240 | 66 | 325 | 0 | 104 | 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 | 450 | 15859.71 | 15917.97 | 450 | 376 | 74 | 101 | 80 | 99 | 2 |
| cvc5 | 0 | 381 | 28356.84 | 28407.67 | 381 | 296 | 85 | 250 | 0 | 250 | 0 |
| SMTInterpol | 0 | 306 | 25908.44 | 22972.61 | 306 | 240 | 66 | 325 | 0 | 104 | 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 | 376 | 13511.12 | 13559.88 | 376 | 376 | 0 | 12 | 243 | 10 | 2 |
| cvc5 | 0 | 296 | 24928.26 | 24968.09 | 296 | 296 | 0 | 121 | 214 | 121 | 0 |
| SMTInterpol | 0 | 240 | 21723.91 | 19438.14 | 240 | 240 | 0 | 177 | 214 | 41 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 85 | 3428.58 | 3439.58 | 85 | 0 | 85 | 37 | 509 | 37 | 0 |
| Yices2 | 0 | 74 | 2348.59 | 2358.09 | 74 | 0 | 74 | 34 | 523 | 34 | 0 |
| SMTInterpol | 0 | 66 | 4184.53 | 3534.47 | 66 | 0 | 66 | 56 | 509 | 17 | 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 | 356 | 796.24 | 840.58 | 356 | 288 | 68 | 0 | 275 | 0 | 0 |
| cvc5 | 0 | 285 | 783.27 | 818.52 | 285 | 212 | 73 | 0 | 346 | 0 | 0 |
| SMTInterpol | 0 | 212 | 1006.77 | 462.76 | 212 | 164 | 48 | 172 | 247 | 0 | 0 |