QF_UF (Unsat Core Track)
Competition results for the QF_UF
logic
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 2061
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | SMTInterpol | - | SMTInterpol | OpenSMT |
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 | 325823 | 3517.275053 | 3724.266506 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 325811 | 3745.765214 | 3952.909711 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 325615 | 25544.892527 | 10848.580388 | 2050 | 0 | 2050 | 11 | 0 | 10 | 0 |
| plat-smt | 0 | 324243 | 6950.596476 | 7158.21511 | 2059 | 0 | 2059 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 229041 | 5127.630451 | 5334.12894 | 2061 | 0 | 2061 | 0 | 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 |
|---|
| SMTInterpol | 0 | 325974 | 45976.634274 | 19245.696193 | 2050 | 0 | 2050 | 11 | 0 | 10 | 0 |
| OpenSMT | 0 | 325823 | 3517.275053 | 3724.266506 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 325811 | 3745.765214 | 3952.909711 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| plat-smt | 0 | 324243 | 6950.596476 | 7158.21511 | 2059 | 0 | 2059 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 229041 | 5127.630451 | 5334.12894 | 2061 | 0 | 2061 | 0 | 0 | 0 | 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 | 325974 | 45976.634274 | 19245.696193 | 2050 | 0 | 2050 | 11 | 0 | 10 | 0 |
| OpenSMT | 0 | 325823 | 3517.275053 | 3724.266506 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| Yices2 | 0 | 325811 | 3745.765214 | 3952.909711 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| plat-smt | 0 | 324243 | 6950.596476 | 7158.21511 | 2059 | 0 | 2059 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 229041 | 5127.630451 | 5334.12894 | 2061 | 0 | 2061 | 0 | 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 |
|---|
| OpenSMT | 0 | 314489 | 1641.948941 | 1845.194451 | 2029 | 0 | 2029 | 0 | 32 | 0 | 0 |
| Yices2 | 0 | 313610 | 670.320069 | 873.649727 | 2031 | 0 | 2031 | 0 | 30 | 0 | 0 |
| SMTInterpol | 0 | 301618 | 18525.061915 | 7541.946338 | 2000 | 0 | 2000 | 0 | 61 | 0 | 0 |
| plat-smt | 0 | 296007 | 1165.060524 | 1367.869658 | 2025 | 0 | 2025 | 0 | 36 | 0 | 0 |
| cvc5 | 0 | 217899 | 1249.799213 | 1452.466678 | 2028 | 0 | 2028 | 0 | 33 | 0 | 0 |