QF_Equality_LinearArith (Unsat Core Track)
Competition results for the QF_Equality_LinearArith
division
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 588
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 |
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 | 902116 | 21686.386868 | 21743.67681 | 519 | 0 | 519 | 44 | 25 | 41 | 0 |
| OpenSMT | 0 | 598340 | 27426.171736 | 27485.057484 | 514 | 0 | 514 | 49 | 25 | 46 | 0 |
| SMTInterpol | 0 | 250811 | 8391.676323 | 4518.686916 | 496 | 0 | 496 | 92 | 0 | 92 | 0 |
| cvc5 | 0 | 198295 | 1842.897048 | 1892.19097 | 487 | 0 | 487 | 101 | 0 | 101 | 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 | 902116 | 21686.386868 | 21743.67681 | 519 | 0 | 519 | 44 | 25 | 41 | 0 |
| OpenSMT | 0 | 598340 | 27426.171736 | 27485.057484 | 514 | 0 | 514 | 49 | 25 | 46 | 0 |
| SMTInterpol | 0 | 319508 | 17438.824764 | 8479.698424 | 496 | 0 | 496 | 92 | 0 | 92 | 0 |
| cvc5 | 0 | 198295 | 1842.897048 | 1892.19097 | 487 | 0 | 487 | 101 | 0 | 101 | 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 | 902116 | 21686.386868 | 21743.67681 | 519 | 0 | 519 | 44 | 25 | 41 | 0 |
| OpenSMT | 0 | 598340 | 27426.171736 | 27485.057484 | 514 | 0 | 514 | 49 | 25 | 46 | 0 |
| SMTInterpol | 0 | 319508 | 17438.824764 | 8479.698424 | 496 | 0 | 496 | 92 | 0 | 92 | 0 |
| cvc5 | 0 | 198295 | 1842.897048 | 1892.19097 | 487 | 0 | 487 | 101 | 0 | 101 | 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 | 208639 | 147.849392 | 194.291509 | 463 | 0 | 463 | 3 | 122 | 0 | 0 |
| cvc5 | 0 | 33173 | 195.475598 | 243.414848 | 479 | 0 | 479 | 0 | 109 | 0 | 0 |
| SMTInterpol | 0 | 4487 | 1227.285654 | 543.080958 | 479 | 0 | 479 | 0 | 109 | 0 | 0 |
| OpenSMT | 0 | 3826 | 161.377198 | 207.246516 | 454 | 0 | 454 | 3 | 131 | 0 | 0 |