QF_LinearIntArith (Model Validation Track)
Competition results for the QF_LinearIntArith
division
in the Model Validation Track. Chart
Results were generated on 2025-08-11
Benchmarks: 4895
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Logics:Winners
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
---|
OpenSMT | OpenSMT | OpenSMT | - | Yices2 |
Sequential Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
---|
OpenSMT | 0 | 4583 | 237974.80 | 238579.07 | 4583 | 4583 | 311 | 1 | 311 | 0 |
Yices2 | 0 | 4534 | 62288.73 | 62853.91 | 4534 | 4534 | 361 | 0 | 360 | 0 |
SMTInterpol | 0 | 4096 | 144744.98 | 119966.73 | 4098 | 4098 | 797 | 0 | 645 | 0 |
cvc5 | 0 | 3815 | 170783.41 | 171275.49 | 3815 | 3815 | 1080 | 0 | 1076 | 4 |
Parallel Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
---|
OpenSMT | 0 | 4583 | 237974.80 | 238579.07 | 4583 | 4583 | 311 | 1 | 311 | 0 |
Yices2 | 0 | 4534 | 62288.73 | 62853.91 | 4534 | 4534 | 361 | 0 | 360 | 0 |
SMTInterpol | 0 | 4098 | 147262.26 | 122049.94 | 4098 | 4098 | 797 | 0 | 645 | 0 |
cvc5 | 0 | 3815 | 170783.41 | 171275.49 | 3815 | 3815 | 1080 | 0 | 1076 | 4 |
SAT Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
---|
OpenSMT | 0 | 4583 | 237974.80 | 238579.07 | 4583 | 4583 | 311 | 1 | 311 | 0 |
Yices2 | 0 | 4534 | 62288.73 | 62853.91 | 4534 | 4534 | 361 | 0 | 360 | 0 |
SMTInterpol | 0 | 4098 | 147262.26 | 122049.94 | 4098 | 4098 | 797 | 0 | 645 | 0 |
cvc5 | 0 | 3815 | 170783.41 | 171275.49 | 3815 | 3815 | 1080 | 0 | 1076 | 4 |
24 seconds Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
---|
Yices2 | 0 | 4308 | 3424.89 | 3954.61 | 4308 | 4308 | 1 | 586 | 0 | 0 |
OpenSMT | 0 | 3621 | 5504.70 | 5950.94 | 3621 | 3621 | 0 | 1274 | 0 | 0 |
SMTInterpol | 0 | 3399 | 15387.82 | 7497.51 | 3399 | 3399 | 120 | 1376 | 0 | 0 |
cvc5 | 0 | 3320 | 3889.86 | 4294.54 | 3320 | 3320 | 0 | 1575 | 0 | 0 |