QF_NonLinearRealArith (Model Validation Track)
Competition results for the QF_NonLinearRealArith
division
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 2766
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| SMT-RAT | SMT-RAT | SMT-RAT | - | SMT-RAT |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 2471 | 28629.114019 | 28880.659594 | 2471 | 2471 | 0 | 295 | 0 | 164 | 0 |
| cvc5 | 0 | 1976 | 13039.017861 | 13239.588365 | 1976 | 1976 | 0 | 790 | 0 | 167 | 0 |
| SMTInterpol | 0 | 20 | 3613.608667 | 3184.852273 | 20 | 20 | 0 | 2746 | 0 | 1 | 0 |
| Yices2 | 435 | 2072 | 6743.97419 | 6953.19663 | 2072 | 2072 | 0 | 694 | 0 | 119 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 2471 | 28629.114019 | 28880.659594 | 2471 | 2471 | 0 | 295 | 0 | 164 | 0 |
| cvc5 | 0 | 1976 | 13039.017861 | 13239.588365 | 1976 | 1976 | 0 | 790 | 0 | 167 | 0 |
| SMTInterpol | 0 | 20 | 3613.608667 | 3184.852273 | 20 | 20 | 0 | 2746 | 0 | 1 | 0 |
| Yices2 | 435 | 2072 | 6743.97419 | 6953.19663 | 2072 | 2072 | 0 | 694 | 0 | 119 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 2471 | 28629.114019 | 28880.659594 | 2471 | 2471 | 0 | 295 | 0 | 164 | 0 |
| cvc5 | 0 | 1976 | 13039.017861 | 13239.588365 | 1976 | 1976 | 0 | 790 | 0 | 167 | 0 |
| SMTInterpol | 0 | 20 | 3613.608667 | 3184.852273 | 20 | 20 | 0 | 2746 | 0 | 1 | 0 |
| Yices2 | 435 | 2072 | 6743.97419 | 6953.19663 | 2072 | 2072 | 0 | 694 | 0 | 119 | 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 |
|---|
| SMT-RAT | 0 | 2388 | 693.493476 | 932.344886 | 2388 | 2388 | 0 | 125 | 253 | 0 | 0 |
| cvc5 | 0 | 1919 | 913.427119 | 1105.209201 | 1919 | 1919 | 0 | 616 | 231 | 0 | 0 |
| SMTInterpol | 0 | 8 | 39.199381 | 15.832264 | 8 | 8 | 0 | 2740 | 18 | 0 | 0 |
| Yices2 | 432 | 2041 | 712.648246 | 917.039202 | 2041 | 2041 | 0 | 569 | 156 | 0 | 0 |