The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2026-07-25
| Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|
| Yices2 | - | - | Yices2 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Equality_LinearArith | Yices2 | 0.021764 | 0.064475 |
| Equality_NonLinearArith | cvc5 | 0.011748 | 0.018578 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.009855 | 0.043939 |
| QF_Equality_LinearArith | cvc5 | 0.004777 | 0.003974 |
| QF_NonLinearIntArith | SMTInterpol | 0.004276 | -0.000272 |
| Equality_NonLinearArith | SMTInterpol | 0.002079 | -0.012596 |
| Equality_LinearArith | cvc5 | 0.001747 | 0.028579 |
| QF_Equality_Bitvec | Bitwuzla | 0.001715 | 0.052945 |
| QF_Equality_LinearArith | SMTInterpol | 0.00096 | 0.00752 |
| QF_Equality_Bitvec_Arith | cvc5 | 0.000214 | -0.006707 |
| QF_LinearRealArith | OpenSMT | 0.000203 | 0.000678 |
| QF_LinearIntArith | Yices2 | 0.000188 | 0.003684 |
| QF_Equality_Bitvec_Arith | Yices2 | 0.000126 | 0.092054 |
| QF_Bitvec | Bitwuzla | 8.9e-05 | 0.014191 |
| QF_Equality_Bitvec | Yices2 | 8.2e-05 | 0.110076 |
| QF_LinearRealArith | Yices2 | 6.8e-05 | 0 |
| QF_Equality_NonLinearArith | Yices2 | 4.8e-05 | 0.022935 |
| QF_Bitvec | Yices2 | 3.1e-05 | 0.016364 |
| QF_NonLinearIntArith | cvc5 | 2e-05 | 0.00057 |
| Division | Solver | Correct Score | Time Score |
|---|---|---|---|
| QF_Equality_LinearArith | Yices2 | 0.13033 | 0.069413 |
| QF_Equality_Bitvec | SMTInterpol | 0.041546 | -0.002765 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.030263 | 0.01479 |
| QF_Equality_NonLinearArith | cvc5 | 0.021759 | 0.000929 |
| QF_Bitvec | Yices2 | 0.014024 | 0.026187 |
| Equality_NonLinearArith | cvc5 | 0.012663 | -0.058259 |
| QF_LinearIntArith | Yices2 | 0.009651 | -0.008488 |
| Equality_LinearArith | cvc5 | 0.008733 | -0.007554 |
| QF_Equality_Bitvec_Arith | Yices2 | 0.008674 | 0.049199 |
| QF_NonLinearIntArith | Yices2 | 0.007004 | -0.002214 |
| QF_Equality_LinearArith | cvc5 | 0.006217 | -0.003505 |
| QF_Equality_Bitvec | Yices2 | 0.005848 | 0.072403 |
| QF_Equality_Bitvec | cvc5 | 0.005761 | 0.001411 |
| QF_NonLinearIntArith | SMTInterpol | 0.00472 | -0.010839 |
| QF_Equality_LinearArith | SMTInterpol | 0.003422 | -0.008167 |
| Equality_NonLinearArith | SMTInterpol | 0.003046 | 0.001936 |
| QF_Equality_Bitvec | Bitwuzla | 0.001222 | -0.003359 |
| FPArith | cvc5 | 0.000578 | 0.000739 |
| Arith | SMTInterpol | 0.000238 | -0.000574 |