QF_LinearIntArith (Unsat Core Track)
Competition results for the QF_LinearIntArith
division
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 1067
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| Yices2 | Yices2 | - | Yices2 | Yices2 |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 4.146043e+06 | 8529.638184 | 8626.159291 | 959 | 0 | 959 | 108 | 0 | 107 | 1 |
| cvc5 | 0 | 3.959993e+06 | 17795.21271 | 17891.059916 | 924 | 0 | 924 | 143 | 0 | 140 | 0 |
| SMTInterpol | 1 | 4.162055e+06 | 22528.575145 | 16381.359559 | 957 | 0 | 957 | 110 | 0 | 109 | 0 |
| OpenSMT | 41 | 3.000644e+06 | 9100.433155 | 9195.795545 | 907 | 0 | 907 | 155 | 5 | 112 | 1 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 6.434213e+06 | 137023.546904 | 137159.036157 | 959 | 0 | 959 | 108 | 0 | 107 | 1 |
| cvc5 | 0 | 6.166773e+06 | 185928.600182 | 186134.435299 | 924 | 0 | 924 | 143 | 0 | 140 | 0 |
| SMTInterpol | 1 | 6.282912e+06 | 180959.476811 | 148022.706679 | 957 | 0 | 957 | 110 | 0 | 109 | 0 |
| OpenSMT | 41 | 6.400489e+06 | 143603.737454 | 143742.78852 | 907 | 0 | 907 | 155 | 5 | 112 | 1 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 6.434213e+06 | 137023.546904 | 137159.036157 | 959 | 0 | 959 | 108 | 0 | 107 | 1 |
| cvc5 | 0 | 6.166773e+06 | 185928.600182 | 186134.435299 | 924 | 0 | 924 | 143 | 0 | 140 | 0 |
| SMTInterpol | 1 | 6.282912e+06 | 180959.476811 | 148022.706679 | 957 | 0 | 957 | 110 | 0 | 109 | 0 |
| OpenSMT | 41 | 6.400489e+06 | 143603.737454 | 143742.78852 | 907 | 0 | 907 | 155 | 5 | 112 | 1 |
24 seconds 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 | 457.297614 | 551.516107 | 940 | 0 | 940 | 0 | 127 | 0 | 0 |
| cvc5 | 0 | 2.571684e+06 | 561.913926 | 648.281722 | 864 | 0 | 864 | 0 | 203 | 0 | 0 |
| SMTInterpol | 0 | 1.248566e+06 | 2202.160568 | 1077.122189 | 878 | 0 | 878 | 0 | 189 | 0 | 0 |
| OpenSMT | 34 | 1.490758e+06 | 757.850854 | 848.856704 | 873 | 0 | 873 | 35 | 159 | 0 | 0 |