QF_LIA (Unsat Core Track)
Competition results for the QF_LIA
logic
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 962
Time Limit: 1200 seconds
Memory Limit: 20480 GB
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 | 4.098831e+06 | 2104.503998 | 2199.489581 | 945 | 0 | 945 | 17 | 0 | 16 | 1 |
| SMTInterpol | 0 | 3.757658e+06 | 16616.860839 | 13689.775913 | 938 | 0 | 938 | 24 | 0 | 24 | 0 |
| cvc5 | 0 | 3.516619e+06 | 9076.464065 | 9168.161449 | 901 | 0 | 901 | 61 | 0 | 58 | 0 |
| OpenSMT | 0 | 2.943126e+06 | 4247.578767 | 4342.75267 | 942 | 0 | 942 | 20 | 0 | 18 | 1 |
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 | 4.098831e+06 | 2104.503998 | 2199.489581 | 945 | 0 | 945 | 17 | 0 | 16 | 1 |
| SMTInterpol | 0 | 3.757658e+06 | 16616.860839 | 13689.775913 | 938 | 0 | 938 | 24 | 0 | 24 | 0 |
| cvc5 | 0 | 3.516619e+06 | 9076.464065 | 9168.161449 | 901 | 0 | 901 | 61 | 0 | 58 | 0 |
| OpenSMT | 0 | 2.943126e+06 | 4247.578767 | 4342.75267 | 942 | 0 | 942 | 20 | 0 | 18 | 1 |
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 | 4.098831e+06 | 2104.503998 | 2199.489581 | 945 | 0 | 945 | 17 | 0 | 16 | 1 |
| SMTInterpol | 0 | 3.757658e+06 | 16616.860839 | 13689.775913 | 938 | 0 | 938 | 24 | 0 | 24 | 0 |
| cvc5 | 0 | 3.516619e+06 | 9076.464065 | 9168.161449 | 901 | 0 | 901 | 61 | 0 | 58 | 0 |
| OpenSMT | 0 | 2.943126e+06 | 4247.578767 | 4342.75267 | 942 | 0 | 942 | 20 | 0 | 18 | 1 |
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 | 4.030771e+06 | 456.306766 | 550.12521 | 936 | 0 | 936 | 0 | 26 | 0 | 0 |
| cvc5 | 0 | 2.552308e+06 | 543.071697 | 629.037842 | 860 | 0 | 860 | 0 | 102 | 0 | 0 |
| OpenSMT | 0 | 1.471471e+06 | 749.89422 | 840.696984 | 906 | 0 | 906 | 1 | 55 | 0 | 0 |
| SMTInterpol | 0 | 1.191913e+06 | 2084.118399 | 1035.437925 | 871 | 0 | 871 | 0 | 91 | 0 | 0 |