The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_IDL logic in the Unsat Core Track. Chart
Results were generated on 2026-07-25
Benchmarks: 100
Time Limit: 1200 seconds
Memory Limit: 30720 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | - | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 512866 | 8187.40 | 8190.99 | 21 | 21 | 79 | 0 | 79 | 0 |
| SMTInterpol | 0 | 279934 | 425.14 | 261.36 | 9 | 9 | 91 | 0 | 71 | 0 |
| z3-BooledASS ne | 0 | 266101 (base +0) | 8130.86 | 8134.58 | 23 | 23 | 77 | 0 | 77 | 0 |
| OpenSMT | 0 | 170168 | 6215.33 | 6217.25 | 11 | 11 | 89 | 0 | 89 | 0 |
| Yices2 | 0 | 95728 | 5524.81 | 5526.91 | 13 | 13 | 87 | 0 | 87 | 0 |
| OpenSMT (min-ucore) | 0 | 19384 | 7.90 | 8.03 | 1 | 1 | 99 | 0 | 99 | 0 |
| z3-BooledASS-base n | 0 | 266101 | 8071.14 | 8074.78 | 23 | 23 | 77 | 0 | 77 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 512866 | 8187.40 | 8190.99 | 21 | 21 | 79 | 0 | 79 | 0 |
| SMTInterpol | 0 | 279934 | 425.14 | 261.36 | 9 | 9 | 91 | 0 | 71 | 0 |
| z3-BooledASS ne | 0 | 266101 (base +0) | 8130.86 | 8134.58 | 23 | 23 | 77 | 0 | 77 | 0 |
| OpenSMT | 0 | 170168 | 6215.33 | 6217.25 | 11 | 11 | 89 | 0 | 89 | 0 |
| Yices2 | 0 | 95728 | 5524.81 | 5526.91 | 13 | 13 | 87 | 0 | 87 | 0 |
| OpenSMT (min-ucore) | 0 | 19384 | 7.90 | 8.03 | 1 | 1 | 99 | 0 | 99 | 0 |
| z3-BooledASS-base n | 0 | 266101 | 8071.14 | 8074.78 | 23 | 23 | 77 | 0 | 77 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 512866 | 8187.40 | 8190.99 | 21 | 21 | 79 | 0 | 79 | 0 |
| SMTInterpol | 0 | 279934 | 425.14 | 261.36 | 9 | 9 | 91 | 0 | 71 | 0 |
| z3-BooledASS ne | 0 | 266101 (base +0) | 8130.86 | 8134.58 | 23 | 23 | 77 | 0 | 77 | 0 |
| OpenSMT | 0 | 170168 | 6215.33 | 6217.25 | 11 | 11 | 89 | 0 | 89 | 0 |
| Yices2 | 0 | 95728 | 5524.81 | 5526.91 | 13 | 13 | 87 | 0 | 87 | 0 |
| OpenSMT (min-ucore) | 0 | 19384 | 7.90 | 8.03 | 1 | 1 | 99 | 0 | 99 | 0 |
| z3-BooledASS-base n | 0 | 266101 | 8071.14 | 8074.78 | 23 | 23 | 77 | 0 | 77 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 69928 | 27.12 | 27.38 | 2 | 2 | 0 | 98 | 0 | 0 |
| SMTInterpol | 0 | 55544 | 74.70 | 30.94 | 5 | 5 | 0 | 95 | 0 | 0 |
| OpenSMT (min-ucore) | 0 | 19384 | 7.90 | 8.03 | 1 | 1 | 0 | 99 | 0 | 0 |
| z3-BooledASS ne | 0 | 19368 (base +0) | 9.31 | 9.42 | 1 | 1 | 0 | 99 | 0 | 0 |
| OpenSMT | 0 | 19276 | 2.80 | 2.92 | 1 | 1 | 0 | 99 | 0 | 0 |
| z3-BooledASS-base n | 0 | 19368 | 9.79 | 9.91 | 1 | 1 | 0 | 99 | 0 | 0 |