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) |
|---|---|---|---|
| cvc5 (40.380757) | — | — | cvc5 (19.892157) |
| Division | Solver | Contribution |
|---|---|---|
| QF_NonLinearIntArith | SMTInterpol | 6.344821 |
| QF_Equality_NonLinearArith | SMTInterpol | 5.087468 |
| QF_FPArith | Bitwuzla | 5.025228 |
| Arith | cvc5 | 4.616602 |
| Bitvec | Bitwuzla-fixed | 4.589458 |
| QF_Bitvec | Bitwuzla | 4.45671 |
| QF_Bitvec | Yices2 | 4.449346 |
| QF_Bitvec | cvc5 | 4.411831 |
| QF_Equality_LinearArith | cvc5 | 4.371039 |
| QF_Equality_LinearArith | SMTInterpol | 4.254193 |
| QF_FPArith | cvc5 | 4.241677 |
| QF_Equality_Bitvec_Arith | Yices2 | 4.204554 |
| QF_Equality_Bitvec_Arith | SMTInterpol | 4.184729 |
| QF_Equality_Bitvec_Arith | cvc5 | 4.176811 |
| QF_Equality | SMTInterpol | 3.993568 |
| QF_Equality | cvc5 | 3.993568 |
| QF_Equality | Yices2 | 3.993568 |
| QF_Equality | plat-smt | 3.993568 |
| QF_Equality | OpenSMT | 3.989516 |
| QF_LinearIntArith | Yices2 | 3.973386 |
| Arith | SMTInterpol | 3.923107 |
| Bitvec | cvc5 | 3.902681 |
| QF_LinearIntArith | SMTInterpol | 3.819661 |
| QF_Equality_Bitvec | Bitwuzla | 3.58159 |
| QF_Equality_Bitvec | Yices2 | 3.509744 |
| QF_Equality_NonLinearArith | cvc5 | 3.404443 |
| Equality_MachineArith | Bitwuzla | 3.355834 |
| Equality_MachineArith | Bitwuzla-fixed | 3.355834 |
| QF_Equality_LinearArith | Yices2 | 3.159073 |
| FPArith | Bitwuzla-fixed | 2.832493 |
| FPArith | Bitwuzla | 2.832493 |
| Arith | UltimateEliminator+MathSAT | 2.595415 |
| QF_Equality_Bitvec | cvc5 | 2.342459 |
| Bitvec | SMTInterpol | 1.829858 |
| QF_Bitvec | SMTInterpol | 1.687138 |
| QF_LinearRealArith | OpenSMT | 1.475766 |
| QF_LinearRealArith | Yices2 | 1.177932 |
| Equality_LinearArith | cvc5 | 1.165668 |
| Bitvec | UltimateEliminator+MathSAT | 1.087227 |
| FPArith | cvc5 | 1.076246 |
| Equality_LinearArith | SMTInterpol | 1.034998 |
| QF_Equality_Bitvec | SMTInterpol | 1.034938 |
| QF_NonLinearIntArith | cvc5 | 0.961798 |
| QF_LinearRealArith | cvc5 | 0.659715 |
| FPArith | UltimateEliminator+MathSAT | 0.588268 |
| QF_Equality_NonLinearArith | Yices2 | 0.494846 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.436152 |
| Equality_MachineArith | cvc5 | 0.436152 |
| QF_LinearRealArith | SMTInterpol | 0.374684 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.344278 |
| Equality_NonLinearArith | cvc5 | 0.328816 |
| QF_LinearIntArith | cvc5 | 0.271065 |
| Equality_NonLinearArith | SMTInterpol | 0.198631 |
| QF_Equality_LinearArith | OpenSMT | 0.039598 |
| QF_LinearIntArith | OpenSMT | 0.024076 |
| Equality | cvc5 | 0.020186 |
| Equality | SMTInterpol | 0.00557 |
| QF_NonLinearIntArith | Yices2 | 0.003745 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 2e-05 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | z3-BooledASS | 0 |
| QF_Equality_Bitvec | z3-BooledASS | 0 |
| QF_Equality_LinearArith | z3-BooledASS | 0 |
| Equality_NonLinearArith | z3-BooledASS | 0 |
| QF_Equality_Bitvec_Arith | z3-BooledASS | 0 |
| Equality | z3-BooledASS | 0 |
| QF_Bitvec | z3-BooledASS | 0 |
| Equality_LinearArith | z3-BooledASS | 0 |
| QF_Equality | z3-BooledASS | 0 |
| QF_Equality_NonLinearArith | z3-BooledASS | 0 |
| QF_NonLinearIntArith | z3-BooledASS | 0 |
| QF_LinearIntArith | z3-BooledASS | 0 |
| Bitvec | z3-BooledASS | 0 |
| Arith | z3-BooledASS | 0 |
| QF_LinearRealArith | z3-BooledASS | 0 |
| FPArith | z3-BooledASS | 0 |
| Equality_MachineArith | z3-BooledASS | 0 |
| QF_Equality_Bitvec | z3-BooledASS-base | 0 |
| Arith | z3-BooledASS-base | 0 |
| QF_Bitvec | z3-BooledASS-base | 0 |
| FPArith | z3-BooledASS-base | 0 |
| Equality_LinearArith | z3-BooledASS-base | 0 |
| QF_LinearRealArith | z3-BooledASS-base | 0 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 0 |
| QF_FPArith | z3-BooledASS-base | 0 |
| QF_Equality_Bitvec_Arith | z3-BooledASS-base | 0 |
| Equality_MachineArith | z3-BooledASS-base | 0 |
| QF_NonLinearIntArith | z3-BooledASS-base | 0 |
| Bitvec | z3-BooledASS-base | 0 |
| QF_Equality_LinearArith | z3-BooledASS-base | 0 |
| QF_Equality | z3-BooledASS-base | 0 |
| QF_LinearIntArith | z3-BooledASS-base | 0 |
| Equality_NonLinearArith | z3-BooledASS-base | 0 |
| Equality | z3-BooledASS-base | 0 |
| Bitvec | Bitwuzla | -9.178916 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Equality_Bitvec_Arith | Yices2 | 4.08777 |
| QF_Equality | cvc5 | 3.993568 |
| QF_Equality | Yices2 | 3.993568 |
| QF_Equality | plat-smt | 3.993568 |
| QF_Equality | SMTInterpol | 3.991947 |
| QF_Equality | OpenSMT | 3.986276 |
| Arith | SMTInterpol | 3.776142 |
| QF_Equality_Bitvec_Arith | cvc5 | 3.401492 |
| QF_FPArith | Bitwuzla | 3.006298 |
| Arith | cvc5 | 2.90951 |
| QF_Bitvec | Yices2 | 2.584252 |
| QF_FPArith | cvc5 | 2.509636 |
| QF_Equality_Bitvec_Arith | SMTInterpol | 2.35521 |
| Bitvec | cvc5 | 1.918922 |
| QF_Bitvec | Bitwuzla | 1.813089 |
| Bitvec | Bitwuzla-fixed | 1.520488 |
| QF_Equality_Bitvec | Yices2 | 1.471043 |
| QF_Bitvec | cvc5 | 1.340236 |
| QF_Equality_Bitvec | Bitwuzla | 1.292841 |
| FPArith | cvc5 | 1.076246 |
| Equality_LinearArith | cvc5 | 0.996049 |
| Bitvec | SMTInterpol | 0.984567 |
| Arith | UltimateEliminator+MathSAT | 0.983402 |
| QF_Equality_Bitvec | cvc5 | 0.865859 |
| Bitvec | UltimateEliminator+MathSAT | 0.576386 |
| Equality_LinearArith | SMTInterpol | 0.454479 |
| Equality_MachineArith | cvc5 | 0.436152 |
| FPArith | Bitwuzla | 0.42218 |
| FPArith | Bitwuzla-fixed | 0.42218 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.358872 |
| QF_Bitvec | SMTInterpol | 0.322659 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.314705 |
| QF_Equality_Bitvec | SMTInterpol | 0.302931 |
| Equality_NonLinearArith | cvc5 | 0.265707 |
| Equality_MachineArith | Bitwuzla-fixed | 0.253805 |
| Equality_MachineArith | Bitwuzla | 0.253805 |
| QF_Equality_NonLinearArith | cvc5 | 0.146803 |
| QF_Equality_LinearArith | Yices2 | 0.065104 |
| Equality_NonLinearArith | SMTInterpol | 0.063016 |
| FPArith | UltimateEliminator+MathSAT | 0.053626 |
| QF_Equality_NonLinearArith | Yices2 | 0.032425 |
| QF_Equality_LinearArith | cvc5 | 0.021303 |
| QF_Equality_LinearArith | SMTInterpol | 0.021064 |
| QF_LinearIntArith | Yices2 | 0.01389 |
| Equality | cvc5 | 0.010673 |
| Equality | SMTInterpol | 0.001561 |
| QF_Equality_LinearArith | OpenSMT | 0.000208 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 5.6e-05 |
| QF_NonLinearIntArith | Yices2 | 4.4e-05 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 2e-05 |
| QF_NonLinearIntArith | SMTInterpol | 1e-06 |
| QF_NonLinearIntArith | cvc5 | 0 |
| QF_LinearIntArith | OpenSMT | 0 |
| QF_LinearIntArith | cvc5 | 0 |
| QF_LinearIntArith | SMTInterpol | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | z3-BooledASS | 0 |
| QF_Equality_Bitvec | z3-BooledASS | 0 |
| QF_Equality_LinearArith | z3-BooledASS | 0 |
| Equality_NonLinearArith | z3-BooledASS | 0 |
| QF_Equality_Bitvec_Arith | z3-BooledASS | 0 |
| Equality | z3-BooledASS | 0 |
| QF_Bitvec | z3-BooledASS | 0 |
| Equality_LinearArith | z3-BooledASS | 0 |
| QF_Equality | z3-BooledASS | 0 |
| QF_Equality_NonLinearArith | z3-BooledASS | 0 |
| QF_NonLinearIntArith | z3-BooledASS | 0 |
| QF_LinearIntArith | z3-BooledASS | 0 |
| Bitvec | z3-BooledASS | 0 |
| Arith | z3-BooledASS | 0 |
| QF_LinearRealArith | z3-BooledASS | 0 |
| FPArith | z3-BooledASS | 0 |
| Equality_MachineArith | z3-BooledASS | 0 |
| QF_Equality_Bitvec | z3-BooledASS-base | 0 |
| Arith | z3-BooledASS-base | 0 |
| QF_Bitvec | z3-BooledASS-base | 0 |
| FPArith | z3-BooledASS-base | 0 |
| Equality_LinearArith | z3-BooledASS-base | 0 |
| QF_LinearRealArith | z3-BooledASS-base | 0 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 0 |
| QF_FPArith | z3-BooledASS-base | 0 |
| QF_Equality_Bitvec_Arith | z3-BooledASS-base | 0 |
| Equality_MachineArith | z3-BooledASS-base | 0 |
| QF_NonLinearIntArith | z3-BooledASS-base | 0 |
| Bitvec | z3-BooledASS-base | 0 |
| QF_Equality_LinearArith | z3-BooledASS-base | 0 |
| QF_Equality | z3-BooledASS-base | 0 |
| QF_LinearIntArith | z3-BooledASS-base | 0 |
| Equality_NonLinearArith | z3-BooledASS-base | 0 |
| Equality | z3-BooledASS-base | 0 |
| Bitvec | Bitwuzla | -9.178916 |