QF_LinearIntArith (Single Query Track)
Competition results for the QF_LinearIntArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 6040
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | Z3-alpha | cvc5 | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 5423 | 339753.965604 | 340382.911206 | 5423 | 3330 | 2093 | 610 | 7 | 600 | 0 |
| cvc5 | 0 | 5388 | 292007.439135 | 292616.068567 | 5388 | 3276 | 2112 | 652 | 0 | 643 | 2 |
| Yices2 | 0 | 5366 | 96776.114299 | 97334.781322 | 5366 | 3295 | 2071 | 674 | 0 | 658 | 10 |
| Z3-alpha | 0 | 5222 | 238943.545117 | 239518.659323 | 5222 | 3348 | 1874 | 818 | 0 | 772 | 39 |
| SMTInterpol | 0 | 5046 | 331778.607247 | 244682.243841 | 5065 | 3010 | 2055 | 975 | 0 | 969 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 5423 | 339753.965604 | 340382.911206 | 5423 | 3330 | 2093 | 610 | 7 | 600 | 0 |
| cvc5 | 0 | 5388 | 292007.439135 | 292616.068567 | 5388 | 3276 | 2112 | 652 | 0 | 643 | 2 |
| Yices2 | 0 | 5366 | 96776.114299 | 97334.781322 | 5366 | 3295 | 2071 | 674 | 0 | 658 | 10 |
| Z3-alpha | 0 | 5222 | 238943.545117 | 239518.659323 | 5222 | 3348 | 1874 | 818 | 0 | 772 | 39 |
| SMTInterpol | 0 | 5065 | 362118.322403 | 262067.913723 | 5065 | 3010 | 2055 | 975 | 0 | 969 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 3348 | 133582.80608 | 133946.438517 | 3348 | 3348 | 0 | 339 | 2353 | 334 | 4 |
| OpenSMT | 0 | 3330 | 249988.304371 | 250384.471705 | 3330 | 3330 | 0 | 356 | 2354 | 355 | 0 |
| Yices2 | 0 | 3295 | 74281.11651 | 74627.98039 | 3295 | 3295 | 0 | 392 | 2353 | 392 | 0 |
| cvc5 | 0 | 3276 | 157086.411782 | 157452.395547 | 3276 | 3276 | 0 | 411 | 2353 | 409 | 2 |
| SMTInterpol | 0 | 3010 | 219476.647041 | 173484.205733 | 3010 | 3010 | 0 | 677 | 2353 | 677 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 2112 | 134921.027353 | 135163.67302 | 2112 | 0 | 2112 | 147 | 3781 | 146 | 0 |
| OpenSMT | 0 | 2093 | 89765.661233 | 89998.439501 | 2093 | 0 | 2093 | 161 | 3786 | 158 | 0 |
| Yices2 | 0 | 2071 | 22494.997789 | 22706.800932 | 2071 | 0 | 2071 | 188 | 3781 | 188 | 0 |
| SMTInterpol | 0 | 2055 | 142641.675362 | 88583.70799 | 2055 | 0 | 2055 | 204 | 3781 | 204 | 0 |
| Z3-alpha | 0 | 1874 | 105360.739037 | 105572.220806 | 1874 | 0 | 1874 | 385 | 3781 | 361 | 24 |
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 | 5043 | 5057.446171 | 5562.07042 | 5043 | 3049 | 1994 | 6 | 991 | 0 | 0 |
| Z3-alpha | 0 | 4139 | 6949.395388 | 7363.571561 | 4139 | 2789 | 1350 | 6 | 1895 | 0 | 0 |
| OpenSMT | 0 | 3868 | 10757.322669 | 11146.152188 | 3868 | 2311 | 1557 | 10 | 2162 | 0 | 0 |
| cvc5 | 0 | 3756 | 7954.236682 | 8330.662493 | 3756 | 2369 | 1387 | 6 | 2278 | 0 | 0 |
| SMTInterpol | 0 | 3507 | 32071.16388 | 13674.31315 | 3507 | 2202 | 1305 | 6 | 2527 | 0 | 0 |