The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_LinearIntArith division in the Unsat Core Track. Chart
Results were generated on 2025-08-11
Benchmarks: 1069
Time Limit: 1200 seconds
Memory Limit: 30720 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | - | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3580653 | 14543.31 | 14664.01 | 968 | 968 | 101 | 0 | 100 | 1 |
| SMTInterpol | 0 | 3234355 | 24373.32 | 20865.38 | 948 | 948 | 121 | 0 | 113 | 0 |
| cvc5 | 0 | 2189130 | 12716.24 | 12829.74 | 901 | 901 | 168 | 0 | 167 | 1 |
| OpenSMT (min-ucore) | 32 | 2640254 | 13362.51 | 13472.76 | 885 | 885 | 179 | 5 | 140 | 1 |
| OpenSMT | 36 | 3539809 | 13386.20 | 13503.02 | 922 | 922 | 142 | 5 | 101 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3580653 | 14543.31 | 14664.01 | 968 | 968 | 101 | 0 | 100 | 1 |
| SMTInterpol | 0 | 3234355 | 24373.32 | 20865.38 | 948 | 948 | 121 | 0 | 113 | 0 |
| cvc5 | 0 | 2189130 | 12716.24 | 12829.74 | 901 | 901 | 168 | 0 | 167 | 1 |
| OpenSMT (min-ucore) | 32 | 2640254 | 13362.51 | 13472.76 | 885 | 885 | 179 | 5 | 140 | 1 |
| OpenSMT | 36 | 3539809 | 13386.20 | 13503.02 | 922 | 922 | 142 | 5 | 101 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3580653 | 14543.31 | 14664.01 | 968 | 968 | 101 | 0 | 100 | 1 |
| SMTInterpol | 0 | 3234355 | 24373.32 | 20865.38 | 948 | 948 | 121 | 0 | 113 | 0 |
| cvc5 | 0 | 2189130 | 12716.24 | 12829.74 | 901 | 901 | 168 | 0 | 167 | 1 |
| OpenSMT (min-ucore) | 32 | 2640254 | 13362.51 | 13472.76 | 885 | 885 | 179 | 5 | 140 | 1 |
| OpenSMT | 36 | 3539809 | 13386.20 | 13503.02 | 922 | 922 | 142 | 5 | 101 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3295984 | 474.23 | 588.97 | 935 | 935 | 0 | 134 | 0 | 0 |
| cvc5 | 0 | 1663253 | 618.57 | 725.87 | 866 | 866 | 0 | 203 | 0 | 0 |
| SMTInterpol | 0 | 1527652 | 2069.54 | 1119.74 | 871 | 871 | 0 | 198 | 0 | 0 |
| OpenSMT (min-ucore) | 25 | 1387342 | 765.96 | 866.24 | 820 | 820 | 31 | 218 | 0 | 0 |
| OpenSMT | 29 | 1753969 | 681.87 | 790.99 | 876 | 876 | 32 | 161 | 0 | 0 |