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
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | - | OpenSMT | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 163822 | 8427.117041 | 8449.808488 | 202 | 0 | 202 | 2 | 0 | 2 | 0 |
| 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 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 163822 | 8427.117041 | 8449.808488 | 202 | 0 | 202 | 2 | 0 | 2 | 0 |
| 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 | 108937 | 47436.617869 | 42040.360571 | 169 | 0 | 169 | 35 | 0 | 35 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 163822 | 8427.117041 | 8449.808488 | 202 | 0 | 202 | 2 | 0 | 2 | 0 |
| 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 | 108937 | 47436.617869 | 42040.360571 | 169 | 0 | 169 | 35 | 0 | 35 | 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 | 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 |