QF_UFNRA (Model Validation Track)
Competition results for the QF_UFNRA
logic
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 31
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
---|
cvc5 | cvc5 | cvc5 | - | cvc5 |
Sequential Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
---|
cvc5 | 0 | 27 | 5401.40026 | 5405.387439 | 27 | 27 | 0 | 4 | 0 | 4 | 0 |
SMTInterpol | 0 | 2 | 0.852762 | 0.827033 | 2 | 2 | 0 | 29 | 0 | 0 | 0 |
Yices2 | 3 | 28 | 44.353723 | 47.157414 | 28 | 28 | 0 | 3 | 0 | 0 | 0 |
Parallel Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
---|
cvc5 | 0 | 27 | 5401.40026 | 5405.387439 | 27 | 27 | 0 | 4 | 0 | 4 | 0 |
SMTInterpol | 0 | 2 | 0.852762 | 0.827033 | 2 | 2 | 0 | 29 | 0 | 0 | 0 |
Yices2 | 3 | 28 | 44.353723 | 47.157414 | 28 | 28 | 0 | 3 | 0 | 0 | 0 |
SAT Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
---|
cvc5 | 0 | 27 | 5401.40026 | 5405.387439 | 27 | 27 | 0 | 4 | 0 | 4 | 0 |
SMTInterpol | 0 | 2 | 0.852762 | 0.827033 | 2 | 2 | 0 | 29 | 0 | 0 | 0 |
Yices2 | 3 | 28 | 44.353723 | 47.157414 | 28 | 28 | 0 | 3 | 0 | 0 | 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 |
---|
cvc5 | 0 | 10 | 24.22963 | 25.23512 | 10 | 10 | 0 | 0 | 21 | 0 | 0 |
SMTInterpol | 0 | 2 | 0.852762 | 0.827033 | 2 | 2 | 0 | 29 | 0 | 0 | 0 |
Yices2 | 3 | 28 | 44.353723 | 47.157414 | 28 | 28 | 0 | 3 | 0 | 0 | 0 |