The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2025-08-11
| Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|
| cvc5 (40.04554) | — | — | cvc5 (21.345731) |
| Division | Solver | Contribution |
|---|---|---|
| QF_NonLinearIntArith | Z3-Inc-Z3++ | 6.434209 |
| QF_NonLinearIntArith | Z3-Inc-Z3++-base | 6.429414 |
| QF_NonLinearIntArith | SMTInterpol | 6.355372 |
| QF_FPArith | Bitwuzla | 5.491563 |
| QF_Equality_LinearArith | SMTInterpol | 4.776099 |
| Arith | cvc5 | 4.616602 |
| QF_Equality_NonLinearArith | SMTInterpol | 4.56956 |
| QF_FPArith | cvc5 | 4.480688 |
| QF_Equality_LinearArith | cvc5 | 4.370449 |
| QF_Equality_Bitvec_Arith | Yices2 | 4.230649 |
| QF_Equality_Bitvec_Arith | SMTInterpol | 4.192061 |
| QF_Equality_Bitvec_Arith | cvc5 | 4.17794 |
| QF_Equality | SMTInterpol | 4.147985 |
| QF_Equality | cvc5 | 4.147985 |
| QF_Equality | Yices2 | 4.147985 |
| QF_Equality | OpenSMT | 4.12736 |
| QF_LinearIntArith | Yices2 | 3.966233 |
| QF_Bitvec | Yices2 | 3.92941 |
| Arith | SMTInterpol | 3.923107 |
| QF_Bitvec | Bitwuzla | 3.914363 |
| Bitvec | cvc5 | 3.903553 |
| QF_LinearIntArith | SMTInterpol | 3.845117 |
| Bitvec | Bitwuzla | 3.736961 |
| QF_Equality_Bitvec | Bitwuzla | 3.679245 |
| QF_Bitvec | cvc5 | 3.65312 |
| QF_Equality_Bitvec | Yices2 | 3.606087 |
| Equality_MachineArith | Bitwuzla | 3.355834 |
| QF_Equality_NonLinearArith | cvc5 | 3.236646 |
| QF_Equality_LinearArith | Yices2 | 2.888878 |
| FPArith | Bitwuzla | 2.848733 |
| QF_Equality_Bitvec | cvc5 | 2.769854 |
| Arith | UltimateEliminator+MathSAT | 2.400864 |
| QF_Equality_Bitvec | SMTInterpol | 1.595122 |
| QF_Bitvec | SMTInterpol | 1.424934 |
| QF_LinearRealArith | OpenSMT | 1.309154 |
| Bitvec | SMTInterpol | 1.276106 |
| QF_LinearRealArith | Yices2 | 1.26906 |
| Bitvec | UltimateEliminator+MathSAT | 1.087227 |
| FPArith | cvc5 | 1.053048 |
| QF_NonLinearIntArith | cvc5 | 1.032245 |
| Equality_LinearArith | cvc5 | 0.956044 |
| Equality_LinearArith | SMTInterpol | 0.895126 |
| QF_LinearRealArith | cvc5 | 0.655896 |
| QF_Equality_NonLinearArith | Yices2 | 0.652514 |
| FPArith | UltimateEliminator+MathSAT | 0.588268 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.436152 |
| Equality_MachineArith | cvc5 | 0.436152 |
| QF_LinearRealArith | SMTInterpol | 0.325943 |
| QF_LinearIntArith | cvc5 | 0.273672 |
| Equality_NonLinearArith | cvc5 | 0.218038 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.193286 |
| Equality_NonLinearArith | SMTInterpol | 0.077666 |
| Equality | cvc5 | 0.063607 |
| QF_Equality_LinearArith | OpenSMT | 0.048962 |
| QF_NonLinearIntArith | Yices2 | 0.035513 |
| QF_LinearIntArith | OpenSMT | 0.029119 |
| Equality | SMTInterpol | 0.014725 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 1e-06 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Division | Solver | Contribution |
|---|---|---|
| QF_FPArith | Bitwuzla | 5.308893 |
| QF_Equality | cvc5 | 4.147985 |
| QF_Equality | Yices2 | 4.147985 |
| QF_Equality | SMTInterpol | 4.145625 |
| QF_Equality | OpenSMT | 4.1203 |
| QF_Equality_Bitvec_Arith | Yices2 | 4.107694 |
| Arith | SMTInterpol | 3.77594 |
| QF_Equality_Bitvec_Arith | cvc5 | 3.565812 |
| Arith | cvc5 | 2.90951 |
| QF_Equality_Bitvec_Arith | SMTInterpol | 2.846672 |
| QF_Equality_NonLinearArith | cvc5 | 2.81151 |
| QF_Equality_NonLinearArith | SMTInterpol | 2.784746 |
| QF_Equality_Bitvec | Yices2 | 2.286554 |
| QF_Equality_Bitvec | Bitwuzla | 2.188269 |
| QF_FPArith | cvc5 | 2.10131 |
| Bitvec | cvc5 | 1.919533 |
| FPArith | Bitwuzla | 1.806747 |
| QF_Bitvec | Yices2 | 1.641175 |
| QF_Bitvec | Bitwuzla | 1.560837 |
| QF_Equality_Bitvec | cvc5 | 1.413855 |
| Bitvec | Bitwuzla | 1.356045 |
| Arith | UltimateEliminator+MathSAT | 1.224504 |
| FPArith | cvc5 | 1.053048 |
| Equality_LinearArith | SMTInterpol | 0.710151 |
| Equality_LinearArith | cvc5 | 0.708667 |
| Bitvec | UltimateEliminator+MathSAT | 0.576386 |
| Bitvec | SMTInterpol | 0.56572 |
| QF_Bitvec | SMTInterpol | 0.491478 |
| FPArith | UltimateEliminator+MathSAT | 0.479962 |
| QF_Equality_Bitvec | SMTInterpol | 0.447876 |
| Equality_MachineArith | cvc5 | 0.436152 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.358872 |
| Equality_MachineArith | Bitwuzla | 0.253805 |
| QF_Equality_NonLinearArith | Yices2 | 0.182834 |
| QF_Bitvec | cvc5 | 0.13861 |
| QF_Equality_LinearArith | Yices2 | 0.108152 |
| Equality_NonLinearArith | cvc5 | 0.097265 |
| QF_Equality_LinearArith | SMTInterpol | 0.025772 |
| QF_Equality_LinearArith | cvc5 | 0.023613 |
| Equality_NonLinearArith | SMTInterpol | 0.02183 |
| Equality | cvc5 | 0.018859 |
| QF_LinearIntArith | Yices2 | 0.01389 |
| Equality | SMTInterpol | 0.002411 |
| QF_Equality_LinearArith | OpenSMT | 0.000392 |
| QF_NonLinearIntArith | Yices2 | 5e-06 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 2e-06 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 1e-06 |
| QF_NonLinearIntArith | SMTInterpol | 1e-06 |
| QF_NonLinearIntArith | Z3-Inc-Z3++-base | 1e-06 |
| QF_NonLinearIntArith | Z3-Inc-Z3++ | 1e-06 |
| QF_NonLinearIntArith | cvc5 | 0 |
| QF_LinearIntArith | OpenSMT | 0 |
| QF_LinearIntArith | cvc5 | 0 |
| QF_LinearIntArith | SMTInterpol | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |