QF_LinearIntArith (Model Validation Track)
Competition results for the QF_LinearIntArith
division
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 4888
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| OpenSMT | OpenSMT | OpenSMT | - | Yices2 |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 4551 | 259322.481666 | 259840.293042 | 4551 | 4551 | 0 | 336 | 1 | 335 | 0 |
| cvc5 | 0 | 4528 | 126735.120139 | 127207.780682 | 4528 | 4528 | 0 | 360 | 0 | 358 | 2 |
| Yices2 | 0 | 4483 | 73471.882919 | 73935.380976 | 4483 | 4483 | 0 | 405 | 0 | 401 | 0 |
| SMTInterpol | 0 | 4231 | 198203.58162 | 163655.356675 | 4239 | 4239 | 0 | 649 | 0 | 628 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 4551 | 259322.481666 | 259840.293042 | 4551 | 4551 | 0 | 336 | 1 | 335 | 0 |
| cvc5 | 0 | 4528 | 126735.120139 | 127207.780682 | 4528 | 4528 | 0 | 360 | 0 | 358 | 2 |
| Yices2 | 0 | 4483 | 73471.882919 | 73935.380976 | 4483 | 4483 | 0 | 405 | 0 | 401 | 0 |
| SMTInterpol | 0 | 4239 | 210645.622313 | 170639.082516 | 4239 | 4239 | 0 | 649 | 0 | 628 | 0 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 4551 | 259322.481666 | 259840.293042 | 4551 | 4551 | 0 | 336 | 1 | 335 | 0 |
| cvc5 | 0 | 4528 | 126735.120139 | 127207.780682 | 4528 | 4528 | 0 | 360 | 0 | 358 | 2 |
| Yices2 | 0 | 4483 | 73471.882919 | 73935.380976 | 4483 | 4483 | 0 | 405 | 0 | 401 | 0 |
| SMTInterpol | 0 | 4239 | 210645.622313 | 170639.082516 | 4239 | 4239 | 0 | 649 | 0 | 628 | 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 | 4226 | 3424.907891 | 3847.337473 | 4226 | 4226 | 0 | 0 | 662 | 0 | 0 |
| cvc5 | 0 | 3710 | 5472.511472 | 5843.300381 | 3710 | 3710 | 0 | 0 | 1178 | 0 | 0 |
| OpenSMT | 0 | 3513 | 5177.093749 | 5528.954189 | 3513 | 3513 | 0 | 1 | 1374 | 0 | 0 |
| SMTInterpol | 0 | 3432 | 19126.317086 | 8688.394171 | 3432 | 3432 | 0 | 0 | 1456 | 0 | 0 |