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
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| Yices2 | SMTInterpol | - | SMTInterpol | Yices2 |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| 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 |
| OpenSMT | 29 | 325823 | 3517.275053 | 3724.266506 | 2032 | 0 | 2032 | 29 | 0 | 0 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 340498 | 80436.484859 | 32304.329256 | 2050 | 0 | 2050 | 11 | 0 | 10 | 0 |
| plat-smt | 0 | 334341 | 9352.795844 | 9560.721984 | 2059 | 0 | 2059 | 2 | 0 | 2 | 0 |
| Yices2 | 0 | 325811 | 3745.765214 | 3952.909711 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 229041 | 5127.630451 | 5334.12894 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| OpenSMT | 29 | 325823 | 3517.275053 | 3724.266506 | 2032 | 0 | 2032 | 29 | 0 | 0 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 340498 | 80436.484859 | 32304.329256 | 2050 | 0 | 2050 | 11 | 0 | 10 | 0 |
| plat-smt | 0 | 334341 | 9352.795844 | 9560.721984 | 2059 | 0 | 2059 | 2 | 0 | 2 | 0 |
| Yices2 | 0 | 325811 | 3745.765214 | 3952.909711 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 229041 | 5127.630451 | 5334.12894 | 2061 | 0 | 2061 | 0 | 0 | 0 | 0 |
| OpenSMT | 29 | 325823 | 3517.275053 | 3724.266506 | 2032 | 0 | 2032 | 29 | 0 | 0 | 0 |
24 seconds Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| 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 |
| OpenSMT | 29 | 314489 | 1641.948941 | 1845.194451 | 2000 | 0 | 2000 | 29 | 32 | 0 | 0 |