QF_LinearRealArith (Unsat Core Track)
Competition results for the QF_LinearRealArith
division
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 204
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 | 152690 | 20139.639204 | 20161.602082 | 166 | 0 | 166 | 38 | 0 | 38 | 0 |
| cvc5 | 0 | 141909 | 24285.657892 | 24309.66161 | 194 | 0 | 194 | 10 | 0 | 10 | 0 |
| SMTInterpol | 0 | 108368 | 44952.201213 | 39793.931699 | 169 | 0 | 169 | 35 | 0 | 35 | 0 |
| OpenSMT | 2 | 163822 | 8427.117041 | 8449.808488 | 200 | 0 | 200 | 4 | 0 | 2 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 170765 | 65773.338564 | 65808.420714 | 166 | 0 | 166 | 38 | 0 | 38 | 0 |
| SMTInterpol | 0 | 168549 | 91320.929102 | 84102.923068 | 169 | 0 | 169 | 35 | 0 | 35 | 0 |
| cvc5 | 0 | 161066 | 36295.805637 | 36326.903208 | 194 | 0 | 194 | 10 | 0 | 10 | 0 |
| OpenSMT | 2 | 167443 | 10828.539618 | 10852.321082 | 200 | 0 | 200 | 4 | 0 | 2 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 170765 | 65773.338564 | 65808.420714 | 166 | 0 | 166 | 38 | 0 | 38 | 0 |
| SMTInterpol | 0 | 168549 | 91320.929102 | 84102.923068 | 169 | 0 | 169 | 35 | 0 | 35 | 0 |
| cvc5 | 0 | 161066 | 36295.805637 | 36326.903208 | 194 | 0 | 194 | 10 | 0 | 10 | 0 |
| OpenSMT | 2 | 167443 | 10828.539618 | 10852.321082 | 200 | 0 | 200 | 4 | 0 | 2 | 0 |
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 | 106706 | 613.715135 | 622.61336 | 87 | 0 | 87 | 0 | 117 | 0 | 0 |
| OpenSMT | 0 | 95813 | 808.135665 | 822.368894 | 140 | 0 | 140 | 0 | 64 | 0 | 0 |
| cvc5 | 0 | 34158 | 697.048152 | 704.33352 | 72 | 0 | 72 | 0 | 132 | 0 | 0 |
| SMTInterpol | 0 | 20920 | 763.391416 | 354.596901 | 31 | 0 | 31 | 0 | 173 | 0 | 0 |