The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the UFDTNIA logic in the Unsat Core Track. Chart
Results were generated on 2026-07-25
Benchmarks: 500
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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 1107818 (base +15329) | 1171.87 | 1224.15 | 423 | 423 | 77 | 0 | 22 | 0 |
| cvc5 | 0 | 1019842 | 18453.24 | 18505.94 | 411 | 411 | 89 | 0 | 60 | 0 |
| SMTInterpol | 0 | 81717 | 1099.53 | 442.03 | 55 | 55 | 445 | 0 | 231 | 0 |
| z3-BooledASS-base n | 0 | 1092489 | 1178.55 | 1230.57 | 420 | 420 | 80 | 0 | 22 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 1107818 (base +15329) | 1171.87 | 1224.15 | 423 | 423 | 77 | 0 | 22 | 0 |
| cvc5 | 0 | 1019842 | 18453.24 | 18505.94 | 411 | 411 | 89 | 0 | 60 | 0 |
| SMTInterpol | 0 | 81717 | 1099.53 | 442.03 | 55 | 55 | 445 | 0 | 231 | 0 |
| z3-BooledASS-base n | 0 | 1092489 | 1178.55 | 1230.57 | 420 | 420 | 80 | 0 | 22 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 1107818 (base +15329) | 1171.87 | 1224.15 | 423 | 423 | 77 | 0 | 22 | 0 |
| cvc5 | 0 | 1019842 | 18453.24 | 18505.94 | 411 | 411 | 89 | 0 | 60 | 0 |
| SMTInterpol | 0 | 81717 | 1099.53 | 442.03 | 55 | 55 | 445 | 0 | 231 | 0 |
| z3-BooledASS-base n | 0 | 1092489 | 1178.55 | 1230.57 | 420 | 420 | 80 | 0 | 22 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 1072633 (base +1717) | 694.00 | 745.22 | 415 | 415 | 42 | 43 | 0 | 0 |
| cvc5 | 0 | 525033 | 2051.97 | 2091.67 | 320 | 320 | 11 | 169 | 0 | 0 |
| SMTInterpol | 0 | 77561 | 851.51 | 358.36 | 53 | 53 | 0 | 447 | 0 | 0 |
| z3-BooledASS-base n | 0 | 1070916 | 684.24 | 735.44 | 414 | 414 | 45 | 41 | 0 | 0 |