QF_UFLIA (Model Validation Track)
Competition results for the QF_UFLIA
logic
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| SMTInterpol | SMTInterpol | SMTInterpol | - | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 300 | 2033.710941 | 1139.843274 | 300 | 300 | 0 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 299 | 1436.060455 | 1466.48896 | 299 | 299 | 0 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 297 | 693.295923 | 723.181362 | 297 | 297 | 0 | 3 | 0 | 3 | 0 |
| OpenSMT | 0 | 296 | 2628.885196 | 2658.719076 | 296 | 296 | 0 | 4 | 0 | 4 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 300 | 2033.710941 | 1139.843274 | 300 | 300 | 0 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 299 | 1436.060455 | 1466.48896 | 299 | 299 | 0 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 297 | 693.295923 | 723.181362 | 297 | 297 | 0 | 3 | 0 | 3 | 0 |
| OpenSMT | 0 | 296 | 2628.885196 | 2658.719076 | 296 | 296 | 0 | 4 | 0 | 4 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 300 | 2033.710941 | 1139.843274 | 300 | 300 | 0 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 299 | 1436.060455 | 1466.48896 | 299 | 299 | 0 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 297 | 693.295923 | 723.181362 | 297 | 297 | 0 | 3 | 0 | 3 | 0 |
| OpenSMT | 0 | 296 | 2628.885196 | 2658.719076 | 296 | 296 | 0 | 4 | 0 | 4 | 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 | 292 | 85.460627 | 114.757394 | 292 | 292 | 0 | 0 | 8 | 0 | 0 |
| SMTInterpol | 0 | 292 | 1110.887907 | 466.080414 | 292 | 292 | 0 | 0 | 8 | 0 | 0 |
| cvc5 | 0 | 291 | 211.054849 | 240.167293 | 291 | 291 | 0 | 0 | 9 | 0 | 0 |
| OpenSMT | 0 | 286 | 472.701107 | 501.34411 | 286 | 286 | 0 | 0 | 14 | 0 | 0 |