QF_Equality_NonLinearArith (Single Query Track)
Competition results for the QF_Equality_NonLinearArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 631
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 | 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 | 426 | 15655.845284 | 15701.935059 | 426 | 363 | 63 | 125 | 80 | 124 | 1 |
| cvc5 | 0 | 375 | 35739.123011 | 35784.759024 | 375 | 295 | 80 | 256 | 0 | 256 | 0 |
| SMTInterpol | 0 | 316 | 28173.473993 | 22540.361413 | 316 | 254 | 62 | 315 | 0 | 92 | 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 | 426 | 15655.845284 | 15701.935059 | 426 | 363 | 63 | 125 | 80 | 124 | 1 |
| cvc5 | 0 | 375 | 35739.123011 | 35784.759024 | 375 | 295 | 80 | 256 | 0 | 256 | 0 |
| SMTInterpol | 0 | 316 | 28173.473993 | 22540.361413 | 316 | 254 | 62 | 315 | 0 | 92 | 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 | 363 | 14193.357487 | 14232.824625 | 363 | 363 | 0 | 15 | 253 | 15 | 0 |
| cvc5 | 0 | 295 | 28322.224414 | 28358.178859 | 295 | 295 | 0 | 116 | 220 | 116 | 0 |
| SMTInterpol | 0 | 254 | 22795.724382 | 18512.888139 | 254 | 254 | 0 | 157 | 220 | 20 | 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 | 80 | 7416.898597 | 7426.580165 | 80 | 0 | 80 | 31 | 520 | 31 | 0 |
| Yices2 | 0 | 63 | 1462.487797 | 1469.110434 | 63 | 0 | 63 | 33 | 535 | 32 | 1 |
| SMTInterpol | 0 | 62 | 5377.749611 | 4027.473274 | 62 | 0 | 62 | 49 | 520 | 13 | 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 | 332 | 664.404358 | 697.781401 | 332 | 273 | 59 | 0 | 299 | 0 | 0 |
| cvc5 | 0 | 270 | 719.916074 | 747.04913 | 270 | 209 | 61 | 0 | 361 | 0 | 0 |
| SMTInterpol | 0 | 206 | 1452.409708 | 610.211276 | 206 | 166 | 40 | 178 | 247 | 0 | 0 |