QF_UFLIA (Single Query Track)
Competition results for the QF_UFLIA
logic
in the Single Query 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 | 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 | 286 | 8046.121035 | 6015.162916 | 286 | 219 | 67 | 14 | 0 | 14 | 0 |
| Yices2 | 0 | 277 | 3247.745783 | 3276.518548 | 277 | 211 | 66 | 23 | 0 | 23 | 0 |
| cvc5 | 0 | 274 | 2189.984218 | 2217.718036 | 274 | 210 | 64 | 26 | 0 | 26 | 0 |
| OpenSMT | 0 | 272 | 3672.823115 | 3700.869749 | 272 | 208 | 64 | 28 | 0 | 28 | 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 | 286 | 8046.121035 | 6015.162916 | 286 | 219 | 67 | 14 | 0 | 14 | 0 |
| Yices2 | 0 | 277 | 3247.745783 | 3276.518548 | 277 | 211 | 66 | 23 | 0 | 23 | 0 |
| cvc5 | 0 | 274 | 2189.984218 | 2217.718036 | 274 | 210 | 64 | 26 | 0 | 26 | 0 |
| OpenSMT | 0 | 272 | 3672.823115 | 3700.869749 | 272 | 208 | 64 | 28 | 0 | 28 | 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 | 219 | 5099.324867 | 3745.280603 | 219 | 219 | 0 | 0 | 81 | 0 | 0 |
| Yices2 | 0 | 211 | 2989.942139 | 3011.976822 | 211 | 211 | 0 | 8 | 81 | 8 | 0 |
| cvc5 | 0 | 210 | 1828.341057 | 1849.637552 | 210 | 210 | 0 | 9 | 81 | 9 | 0 |
| OpenSMT | 0 | 208 | 3628.365486 | 3649.99941 | 208 | 208 | 0 | 11 | 81 | 11 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 67 | 2946.796167 | 2269.882312 | 67 | 0 | 67 | 0 | 233 | 0 | 0 |
| Yices2 | 0 | 66 | 257.803644 | 264.541726 | 66 | 0 | 66 | 1 | 233 | 1 | 0 |
| OpenSMT | 0 | 64 | 44.457629 | 50.870339 | 64 | 0 | 64 | 3 | 233 | 3 | 0 |
| cvc5 | 0 | 64 | 361.643162 | 368.080484 | 64 | 0 | 64 | 3 | 233 | 3 | 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 | 266 | 154.795526 | 181.439843 | 266 | 201 | 65 | 0 | 34 | 0 | 0 |
| SMTInterpol | 0 | 265 | 1436.054636 | 591.508077 | 265 | 204 | 61 | 0 | 35 | 0 | 0 |
| cvc5 | 0 | 263 | 314.310508 | 340.593165 | 263 | 203 | 60 | 0 | 37 | 0 | 0 |
| OpenSMT | 0 | 259 | 435.706726 | 461.70868 | 259 | 195 | 64 | 0 | 41 | 0 | 0 |