The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the UFBVDTNIA logic in the Single Query Track. Chart
Results were generated on 2026-07-25
Benchmarks: 157
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 SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 157 (base +0) | 30.96 | 50.15 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 157 | 33.45 | 52.76 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz ne | 0 | 157 (base +0) | 36.23 | 55.69 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 100 | 339.37 | 138.00 | 100 | 0 | 100 | 57 | 0 | 19 | 0 |
| z3-BooledASS-base n | 0 | 157 | 31.56 | 50.90 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz-base n | 0 | 157 | 33.34 | 52.61 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 157 (base +0) | 30.96 | 50.15 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 157 | 33.45 | 52.76 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz ne | 0 | 157 (base +0) | 36.23 | 55.69 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 100 | 339.37 | 138.00 | 100 | 0 | 100 | 57 | 0 | 19 | 0 |
| z3-BooledASS-base n | 0 | 157 | 31.56 | 50.90 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz-base n | 0 | 157 | 33.34 | 52.61 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 157 (base +0) | 30.96 | 50.15 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 157 | 33.45 | 52.76 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz ne | 0 | 157 (base +0) | 36.23 | 55.69 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 100 | 339.37 | 138.00 | 100 | 0 | 100 | 57 | 0 | 19 | 0 |
| z3-BooledASS-base n | 0 | 157 | 31.56 | 50.90 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz-base n | 0 | 157 | 33.34 | 52.61 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-BooledASS ne | 0 | 157 (base +0) | 30.96 | 50.15 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 157 | 33.45 | 52.76 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz ne | 0 | 157 (base +0) | 36.23 | 55.69 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 100 | 339.37 | 138.00 | 100 | 0 | 100 | 0 | 57 | 0 | 0 |
| z3-BooledASS-base n | 0 | 157 | 31.56 | 50.90 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |
| cvc5-cvc5-xyz-base n | 0 | 157 | 33.34 | 52.61 | 157 | 0 | 157 | 0 | 0 | 0 | 0 |