QF_Equality (Unsat Core Track)
Competition results for the QF_Equality
division
in the Unsat Core Track.
Results were generated on 2024-07-08
Benchmarks: 2263
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Yices2 | Yices2 | - | Yices2 | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 364451 | 3774.553079 | 4001.917381 | 2263 | 0 | 2263 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 326218 | 3717.974177 | 3945.185415 | 2263 | 0 | 2263 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 326099 | 26109.70474 | 11088.548458 | 2252 | 0 | 2252 | 11 | 0 | 10 | 0 |
| plat-smt | 0 | 324243 | 6950.596476 | 7158.21511 | 2059 | 0 | 2059 | 2 | 202 | 2 | 0 |
| cvc5 | 0 | 261293 | 5234.755 | 5461.440795 | 2263 | 0 | 2263 | 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 |
|---|
| Yices2 | 0 | 364451 | 3774.553079 | 4001.917381 | 2263 | 0 | 2263 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 326458 | 46541.446487 | 19485.664263 | 2252 | 0 | 2252 | 11 | 0 | 10 | 0 |
| OpenSMT | 0 | 326218 | 3717.974177 | 3945.185415 | 2263 | 0 | 2263 | 0 | 0 | 0 | 0 |
| plat-smt | 0 | 324243 | 6950.596476 | 7158.21511 | 2059 | 0 | 2059 | 2 | 202 | 2 | 0 |
| cvc5 | 0 | 261293 | 5234.755 | 5461.440795 | 2263 | 0 | 2263 | 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 |
|---|
| Yices2 | 0 | 364451 | 3774.553079 | 4001.917381 | 2263 | 0 | 2263 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 326458 | 46541.446487 | 19485.664263 | 2252 | 0 | 2252 | 11 | 0 | 10 | 0 |
| OpenSMT | 0 | 326218 | 3717.974177 | 3945.185415 | 2263 | 0 | 2263 | 0 | 0 | 0 | 0 |
| plat-smt | 0 | 324243 | 6950.596476 | 7158.21511 | 2059 | 0 | 2059 | 2 | 202 | 2 | 0 |
| cvc5 | 0 | 261293 | 5234.755 | 5461.440795 | 2263 | 0 | 2263 | 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 |
|---|
| Yices2 | 0 | 352250 | 699.107935 | 922.657397 | 2233 | 0 | 2233 | 0 | 30 | 0 | 0 |
| OpenSMT | 0 | 314884 | 1780.028627 | 2003.391894 | 2230 | 0 | 2230 | 0 | 33 | 0 | 0 |
| SMTInterpol | 0 | 302102 | 19089.874128 | 7781.914408 | 2202 | 0 | 2202 | 0 | 61 | 0 | 0 |
| plat-smt | 0 | 296007 | 1165.060524 | 1367.869658 | 2025 | 0 | 2025 | 0 | 238 | 0 | 0 |
| cvc5 | 0 | 250151 | 1356.923763 | 1579.778533 | 2230 | 0 | 2230 | 0 | 33 | 0 | 0 |