QF_Datatypes (Model Validation Track)
Competition results for the QF_Datatypes
division
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 1943
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| SMTInterpol | SMTInterpol | SMTInterpol | - | SMTInterpol |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 1818 | 14406.48206 | 12020.251169 | 1821 | 1821 | 0 | 122 | 0 | 120 | 0 |
| cvc5 | 0 | 1301 | 15393.506505 | 15526.961045 | 1301 | 1301 | 0 | 642 | 0 | 28 | 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 | 1821 | 18109.484981 | 15594.058438 | 1821 | 1821 | 0 | 122 | 0 | 120 | 0 |
| cvc5 | 0 | 1301 | 15393.506505 | 15526.961045 | 1301 | 1301 | 0 | 642 | 0 | 28 | 0 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 1821 | 18109.484981 | 15594.058438 | 1821 | 1821 | 0 | 122 | 0 | 120 | 0 |
| cvc5 | 0 | 1301 | 15393.506505 | 15526.961045 | 1301 | 1301 | 0 | 642 | 0 | 28 | 0 |
24 seconds Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 1790 | 987.479712 | 846.77394 | 1790 | 1790 | 0 | 2 | 151 | 0 | 0 |
| cvc5 | 0 | 1196 | 406.733809 | 526.416649 | 1196 | 1196 | 0 | 614 | 133 | 0 | 0 |