The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2025-08-11
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| cvc5 (45.708019) | cvc5 (45.708019) | cvc5 (11.028006) | cvc5 (15.132984) | cvc5 (32.772523) |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler-Mocha | 4.503171 |
| QF_Strings | Z3-Noodler | 4.378626 |
| QF_Strings | Z3-Noodler-Mocha-base | 4.366658 |
| QF_Strings | OSTRICH | 4.155295 |
| QF_Bitvec | Bitwuzla-MachBV | 3.895111 |
| QF_Bitvec | Bitwuzla | 3.876625 |
| QF_Bitvec | Yices2 | 3.871457 |
| QF_Bitvec | Bitwuzla-MachBV-base | 3.86703 |
| QF_Equality_Bitvec | Bitwuzla | 3.736878 |
| QF_Equality_Bitvec | Yices2 | 3.692774 |
| QF_Strings | cvc5 | 3.640918 |
| QF_Equality | Yices2 | 3.582177 |
| QF_Equality | OpenSMT | 3.580302 |
| QF_Equality | cvc5 | 3.578428 |
| QF_Equality_Bitvec | Z3-Owl | 3.538279 |
| QF_Equality_Bitvec | cvc5 | 3.497113 |
| QF_Bitvec | cvc5 | 3.474071 |
| QF_Equality | SMTInterpol | 3.43742 |
| QF_Equality_Bitvec | Z3-Owl-base | 3.380212 |
| QF_Strings | Z3-alpha-base | 3.350193 |
| QF_Strings | Z3-Noodler-base | 3.334725 |
| QF_Strings | Z3-alpha | 3.334043 |
| QF_LinearIntArith | OpenSMT | 3.102205 |
| QF_FPArith | Bitwuzla | 3.049823 |
| QF_Bitvec | z3siri | 3.047568 |
| QF_LinearIntArith | Yices2 | 2.997634 |
| QF_LinearIntArith | cvc5 | 2.988723 |
| QF_NonLinearRealArith | Z3-alpha | 2.956225 |
| QF_NonLinearRealArith | z3siri-base | 2.937623 |
| QF_NonLinearRealArith | Z3-alpha-base | 2.937623 |
| QF_FPArith | cvc5 | 2.933724 |
| FPArith | Bitwuzla | 2.929808 |
| QF_NonLinearRealArith | z3siri | 2.847523 |
| QF_Equality_LinearArith | SMTInterpol | 2.835018 |
| QF_Bitvec | Z3-alpha | 2.830255 |
| QF_Equality_LinearArith | cvc5 | 2.825566 |
| QF_Bitvec | Z3-alpha-base | 2.814501 |
| QF_Bitvec | z3siri-base | 2.813872 |
| QF_LinearIntArith | Z3-alpha | 2.779898 |
| QF_NonLinearRealArith | cvc5 | 2.772844 |
| QF_Equality_LinearArith | OpenSMT | 2.772299 |
| QF_Bitvec | bv_decide-nokernel | 2.762512 |
| FPArith | cvc5 | 2.751887 |
| QF_NonLinearRealArith | Yices2 | 2.73289 |
| QF_NonLinearIntArith | Z3-alpha | 2.69275 |
| QF_Equality_LinearArith | Yices2 | 2.667285 |
| QF_Bitvec | Z3-Owl | 2.635574 |
| QF_LinearIntArith | Z3-alpha-base | 2.63268 |
| QF_Bitvec | bv_decide | 2.624624 |
| Arith | Z3-alpha-base | 2.60121 |
| QF_Bitvec | Z3-Owl-base | 2.566009 |
| Equality_LinearArith | cvc5 | 2.552562 |
| QF_NonLinearIntArith | z3siri | 2.547756 |
| Bitvec | cvc5 | 2.52806 |
| QF_NonLinearIntArith | Z3-alpha-base | 2.527296 |
| Arith | Z3-alpha | 2.521893 |
| QF_NonLinearIntArith | z3siri-base | 2.512135 |
| QF_LinearRealArith | Yices2 | 2.484686 |
| QF_LinearRealArith | OpenSMT | 2.478286 |
| QF_NonLinearRealArith | SMT-RAT | 2.416204 |
| QF_LinearIntArith | SMTInterpol | 2.388914 |
| QF_LinearRealArith | cvc5 | 2.370754 |
| QF_LinearRealArith | Z3-alpha-base | 2.364503 |
| QF_Equality_Bitvec | SMTInterpol | 2.262531 |
| QF_NonLinearIntArith | Yices2 | 2.231268 |
| Arith | cvc5 | 2.216909 |
| Arith | YicesQS | 2.216909 |
| Bitvec | YicesQS | 2.189681 |
| QF_LinearRealArith | Z3-alpha | 2.121223 |
| Bitvec | Bitwuzla | 1.963529 |
| QF_NonLinearIntArith | cvc5 | 1.963353 |
| QF_LinearRealArith | SMTInterpol | 1.75944 |
| Equality_NonLinearArith | cvc5 | 1.730677 |
| Arith | UltimateEliminator+MathSAT | 1.649241 |
| Equality_LinearArith | iProver v3.9.3 | 1.498317 |
| QF_Equality_NonLinearArith | Yices2 | 1.424062 |
| QF_FPArith | colibri2 | 1.401006 |
| Equality_MachineArith | cvc5 | 1.322942 |
| QF_Equality_NonLinearArith | cvc5 | 1.020831 |
| QF_Datatypes | cvc5 | 0.991872 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.658486 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.61038 |
| QF_FPArith | Z3-Owl | 0.583862 |
| Equality | cvc5 | 0.546785 |
| QF_FPArith | Z3-Owl-base | 0.512659 |
| Equality_MachineArith | SMTInterpol | 0.35976 |
| QF_Datatypes | SMTInterpol | 0.338675 |
| Equality_NonLinearArith | SMTInterpol | 0.327472 |
| Bitvec | UltimateEliminator+MathSAT | 0.314914 |
| QF_Bitvec | SMTInterpol | 0.299305 |
| Bitvec | SMTInterpol | 0.220255 |
| Equality | iProver v3.9.3 | 0.208337 |
| Arith | iProver v3.9.3 | 0.146281 |
| QF_NonLinearRealArith | SMTInterpol | 0.110033 |
| Arith | SMTInterpol | 0.074297 |
| FPArith | UltimateEliminator+MathSAT | 0.070698 |
| Equality_MachineArith | Bitwuzla | 0.043489 |
| Equality | Yices2 | 0.019418 |
| Equality | SMTInterpol | 0.018703 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.014676 |
| Arith | SMT-RAT | 0.010697 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.00765 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000944 |
| QF_NonLinearIntArith | SMTInterpol | 0.000178 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.40824 |
| Arith | Amaya | -6.44335 |
| Equality_LinearArith | SMTInterpol | -8.457622 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler-Mocha | 4.503171 |
| QF_Strings | Z3-Noodler | 4.378626 |
| QF_Strings | Z3-Noodler-Mocha-base | 4.366658 |
| QF_Strings | OSTRICH | 4.1591 |
| QF_Bitvec | Bitwuzla-MachBV | 3.895111 |
| QF_Bitvec | Bitwuzla | 3.876625 |
| QF_Bitvec | Yices2 | 3.871457 |
| QF_Bitvec | Bitwuzla-MachBV-base | 3.86703 |
| QF_Equality_Bitvec | Bitwuzla | 3.736878 |
| QF_Equality_Bitvec | Yices2 | 3.692774 |
| QF_Strings | cvc5 | 3.640918 |
| QF_Equality | Yices2 | 3.582177 |
| QF_Equality | OpenSMT | 3.580302 |
| QF_Equality | cvc5 | 3.578428 |
| QF_Equality_Bitvec | Z3-Owl | 3.538279 |
| QF_Equality_Bitvec | cvc5 | 3.497113 |
| QF_Bitvec | cvc5 | 3.474071 |
| QF_Equality | SMTInterpol | 3.43742 |
| QF_Equality_Bitvec | Z3-Owl-base | 3.380212 |
| QF_Strings | Z3-alpha | 3.373692 |
| QF_Strings | Z3-alpha-base | 3.350193 |
| QF_Strings | Z3-Noodler-base | 3.334725 |
| QF_LinearIntArith | OpenSMT | 3.102205 |
| QF_Bitvec | Z3-alpha | 3.088303 |
| QF_FPArith | Bitwuzla | 3.049823 |
| QF_Bitvec | z3siri | 3.047568 |
| QF_LinearIntArith | Yices2 | 2.997634 |
| QF_NonLinearRealArith | Z3-alpha | 2.989441 |
| QF_LinearIntArith | cvc5 | 2.988723 |
| QF_NonLinearRealArith | z3siri-base | 2.937623 |
| QF_NonLinearRealArith | Z3-alpha-base | 2.937623 |
| QF_FPArith | cvc5 | 2.933724 |
| FPArith | Bitwuzla | 2.929808 |
| QF_LinearIntArith | Z3-alpha | 2.928916 |
| QF_NonLinearRealArith | z3siri | 2.847523 |
| QF_Equality_LinearArith | SMTInterpol | 2.835018 |
| QF_Equality_LinearArith | cvc5 | 2.825566 |
| QF_Bitvec | Z3-alpha-base | 2.814501 |
| QF_Bitvec | z3siri-base | 2.813872 |
| QF_NonLinearRealArith | cvc5 | 2.772844 |
| QF_Equality_LinearArith | OpenSMT | 2.772299 |
| QF_NonLinearIntArith | Z3-alpha | 2.762918 |
| QF_Bitvec | bv_decide-nokernel | 2.762512 |
| FPArith | cvc5 | 2.751887 |
| QF_NonLinearRealArith | Yices2 | 2.73289 |
| QF_Equality_LinearArith | Yices2 | 2.667285 |
| Arith | Z3-alpha | 2.66414 |
| QF_Bitvec | Z3-Owl | 2.635574 |
| QF_LinearIntArith | Z3-alpha-base | 2.63268 |
| QF_Bitvec | bv_decide | 2.624624 |
| Arith | Z3-alpha-base | 2.60121 |
| QF_Bitvec | Z3-Owl-base | 2.566009 |
| Equality_LinearArith | cvc5 | 2.552562 |
| QF_NonLinearIntArith | z3siri | 2.547756 |
| Bitvec | cvc5 | 2.52806 |
| QF_NonLinearIntArith | Z3-alpha-base | 2.527296 |
| QF_NonLinearIntArith | z3siri-base | 2.512135 |
| QF_LinearRealArith | Yices2 | 2.484686 |
| QF_LinearRealArith | OpenSMT | 2.478286 |
| QF_NonLinearRealArith | SMT-RAT | 2.416204 |
| QF_LinearIntArith | SMTInterpol | 2.392896 |
| QF_LinearRealArith | cvc5 | 2.370754 |
| QF_LinearRealArith | Z3-alpha-base | 2.364503 |
| QF_LinearRealArith | Z3-alpha | 2.35826 |
| QF_Equality_Bitvec | SMTInterpol | 2.270264 |
| QF_NonLinearIntArith | Yices2 | 2.231268 |
| Arith | cvc5 | 2.216909 |
| Arith | YicesQS | 2.216909 |
| Bitvec | YicesQS | 2.189681 |
| Bitvec | Bitwuzla | 1.963529 |
| QF_NonLinearIntArith | cvc5 | 1.963353 |
| QF_LinearRealArith | SMTInterpol | 1.775643 |
| Equality_NonLinearArith | cvc5 | 1.730677 |
| Equality_LinearArith | iProver v3.9.3 | 1.655627 |
| Arith | UltimateEliminator+MathSAT | 1.649241 |
| QF_Equality_NonLinearArith | Yices2 | 1.424062 |
| QF_FPArith | colibri2 | 1.401006 |
| Equality_MachineArith | cvc5 | 1.322942 |
| QF_Equality_NonLinearArith | cvc5 | 1.020831 |
| QF_Datatypes | cvc5 | 0.991872 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.779408 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.658486 |
| QF_FPArith | Z3-Owl | 0.583862 |
| Equality | cvc5 | 0.546785 |
| QF_FPArith | Z3-Owl-base | 0.512659 |
| Equality_MachineArith | SMTInterpol | 0.35976 |
| QF_Datatypes | SMTInterpol | 0.342175 |
| Equality_NonLinearArith | SMTInterpol | 0.327472 |
| Bitvec | UltimateEliminator+MathSAT | 0.314914 |
| QF_Bitvec | SMTInterpol | 0.300949 |
| Equality | iProver v3.9.3 | 0.242307 |
| Bitvec | SMTInterpol | 0.220255 |
| Arith | iProver v3.9.3 | 0.215619 |
| QF_NonLinearRealArith | SMTInterpol | 0.110033 |
| Arith | SMTInterpol | 0.074297 |
| FPArith | UltimateEliminator+MathSAT | 0.070698 |
| Equality_MachineArith | Bitwuzla | 0.043489 |
| Equality | Yices2 | 0.019418 |
| Equality | SMTInterpol | 0.01894 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.014676 |
| Arith | SMT-RAT | 0.010697 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.00765 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000944 |
| QF_NonLinearIntArith | SMTInterpol | 0.000178 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.40824 |
| Arith | Amaya | -6.44335 |
| Equality_LinearArith | SMTInterpol | -8.457622 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler-Mocha | 1.889141 |
| QF_Strings | Z3-Noodler-Mocha-base | 1.888286 |
| QF_Strings | Z3-Noodler | 1.888286 |
| QF_Strings | OSTRICH | 1.779117 |
| QF_Equality_Bitvec | Bitwuzla | 1.599228 |
| QF_Equality_Bitvec | Yices2 | 1.596277 |
| QF_Strings | cvc5 | 1.591024 |
| QF_Equality_Bitvec | Z3-Owl | 1.5384 |
| QF_Equality_Bitvec | Z3-Owl-base | 1.518194 |
| QF_Equality_Bitvec | cvc5 | 1.508428 |
| QF_Strings | Z3-alpha | 1.413881 |
| QF_Strings | Z3-alpha-base | 1.391775 |
| QF_Strings | Z3-Noodler-base | 1.379911 |
| QF_NonLinearIntArith | Z3-alpha | 1.230033 |
| QF_LinearIntArith | Z3-alpha | 1.177754 |
| QF_LinearIntArith | OpenSMT | 1.1666 |
| QF_LinearIntArith | cvc5 | 1.126613 |
| QF_LinearIntArith | Yices2 | 1.12593 |
| QF_NonLinearIntArith | Z3-alpha-base | 1.080035 |
| QF_NonLinearIntArith | z3siri | 1.076957 |
| QF_NonLinearIntArith | z3siri-base | 1.072518 |
| QF_NonLinearIntArith | Yices2 | 1.06231 |
| QF_LinearIntArith | Z3-alpha-base | 1.052031 |
| QF_Equality_NonLinearArith | Yices2 | 0.994213 |
| QF_Equality_LinearArith | SMTInterpol | 0.992795 |
| QF_NonLinearIntArith | cvc5 | 0.971661 |
| QF_Equality_LinearArith | cvc5 | 0.932167 |
| QF_Equality_LinearArith | OpenSMT | 0.880465 |
| QF_Equality_Bitvec | SMTInterpol | 0.861878 |
| QF_Bitvec | Bitwuzla | 0.855285 |
| QF_Bitvec | Bitwuzla-MachBV | 0.854591 |
| QF_Bitvec | Bitwuzla-MachBV-base | 0.854244 |
| QF_Bitvec | Yices2 | 0.852858 |
| QF_Equality_LinearArith | Yices2 | 0.845667 |
| QF_LinearIntArith | SMTInterpol | 0.82596 |
| QF_Bitvec | cvc5 | 0.807071 |
| QF_Bitvec | bv_decide-nokernel | 0.781332 |
| QF_NonLinearRealArith | Z3-alpha | 0.764107 |
| QF_LinearRealArith | OpenSMT | 0.759386 |
| QF_Bitvec | bv_decide | 0.753078 |
| QF_LinearRealArith | Yices2 | 0.748802 |
| QF_NonLinearRealArith | z3siri-base | 0.744241 |
| QF_NonLinearRealArith | Z3-alpha-base | 0.744241 |
| QF_Bitvec | Z3-alpha | 0.741728 |
| QF_NonLinearRealArith | z3siri | 0.723611 |
| QF_LinearRealArith | Z3-alpha-base | 0.717497 |
| QF_Bitvec | Z3-Owl | 0.712621 |
| QF_NonLinearRealArith | Yices2 | 0.702263 |
| QF_Bitvec | z3siri-base | 0.701896 |
| QF_Bitvec | Z3-alpha-base | 0.701896 |
| QF_LinearRealArith | Z3-alpha | 0.696998 |
| QF_LinearRealArith | cvc5 | 0.693611 |
| QF_Bitvec | z3siri | 0.691876 |
| QF_NonLinearRealArith | cvc5 | 0.663463 |
| QF_Equality | SMTInterpol | 0.644702 |
| QF_Equality | cvc5 | 0.644702 |
| QF_Equality | OpenSMT | 0.644702 |
| QF_Equality | Yices2 | 0.644702 |
| QF_Bitvec | Z3-Owl-base | 0.644661 |
| QF_LinearRealArith | SMTInterpol | 0.640531 |
| QF_Equality_NonLinearArith | cvc5 | 0.616151 |
| QF_NonLinearRealArith | SMT-RAT | 0.608739 |
| QF_FPArith | Bitwuzla | 0.455096 |
| QF_FPArith | cvc5 | 0.446085 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.405067 |
| Arith | Z3-alpha | 0.401316 |
| Arith | Z3-alpha-base | 0.39452 |
| Arith | YicesQS | 0.383767 |
| Arith | cvc5 | 0.322369 |
| FPArith | Bitwuzla | 0.306126 |
| FPArith | cvc5 | 0.25246 |
| Arith | UltimateEliminator+MathSAT | 0.231925 |
| QF_FPArith | colibri2 | 0.202265 |
| QF_Datatypes | cvc5 | 0.168897 |
| Bitvec | Bitwuzla | 0.150138 |
| Bitvec | YicesQS | 0.14756 |
| Bitvec | cvc5 | 0.141214 |
| QF_FPArith | Z3-Owl | 0.139625 |
| QF_FPArith | Z3-Owl-base | 0.12028 |
| Equality_MachineArith | cvc5 | 0.064713 |
| Equality | cvc5 | 0.046903 |
| Equality_NonLinearArith | cvc5 | 0.019417 |
| QF_Datatypes | SMTInterpol | 0.019041 |
| QF_Bitvec | SMTInterpol | 0.012495 |
| Equality_LinearArith | cvc5 | 0.011057 |
| Equality | iProver v3.9.3 | 0.010279 |
| FPArith | UltimateEliminator+MathSAT | 0.010138 |
| Equality_MachineArith | Bitwuzla | 0.008531 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.007214 |
| Equality_LinearArith | SMTInterpol | 0.00464 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.00434 |
| Bitvec | UltimateEliminator+MathSAT | 0.002856 |
| Arith | SMTInterpol | 0.000464 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000377 |
| Equality_NonLinearArith | SMTInterpol | 0.000245 |
| Equality | Yices2 | 0.000203 |
| QF_NonLinearRealArith | SMTInterpol | 0.000175 |
| Equality_MachineArith | SMTInterpol | 0.000114 |
| Equality | SMTInterpol | 1.9e-05 |
| Arith | SMT-RAT | 1.9e-05 |
| Bitvec | SMTInterpol | 3e-06 |
| QF_NonLinearIntArith | SMTInterpol | 1e-06 |
| Equality_LinearArith | iProver v3.9.3 | 0 |
| Arith | iProver v3.9.3 | 0 |
| Equality_NonLinearArith | iProver v3.9.3 | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.40824 |
| Arith | Amaya | -6.44335 |
| Division | Solver | Contribution |
|---|---|---|
| Equality_LinearArith | cvc5 | 2.227623 |
| Equality_LinearArith | iProver v3.9.3 | 1.655627 |
| Bitvec | cvc5 | 1.474288 |
| Equality_NonLinearArith | cvc5 | 1.383464 |
| FPArith | Bitwuzla | 1.341849 |
| FPArith | cvc5 | 1.337323 |
| Bitvec | YicesQS | 1.200387 |
| QF_Equality | Yices2 | 1.187513 |
| QF_Equality | OpenSMT | 1.186434 |
| QF_Equality | cvc5 | 1.185355 |
| QF_FPArith | Bitwuzla | 1.148682 |
| QF_Equality | SMTInterpol | 1.1048 |
| QF_Bitvec | Bitwuzla-MachBV | 1.100742 |
| QF_FPArith | cvc5 | 1.091849 |
| QF_Bitvec | Yices2 | 1.090142 |
| QF_Bitvec | Bitwuzla | 1.090142 |
| QF_Bitvec | Bitwuzla-MachBV-base | 1.086229 |
| Bitvec | Bitwuzla | 1.027758 |
| Arith | Z3-alpha | 0.99745 |
| Arith | Z3-alpha-base | 0.96967 |
| QF_Bitvec | cvc5 | 0.932219 |
| Arith | cvc5 | 0.848524 |
| QF_Bitvec | z3siri | 0.835283 |
| QF_Bitvec | Z3-alpha | 0.803032 |
| Equality_MachineArith | cvc5 | 0.802468 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.779408 |
| QF_FPArith | COLIBRI | 0.757579 |
| Arith | YicesQS | 0.755925 |
| QF_NonLinearRealArith | Z3-alpha | 0.730799 |
| QF_NonLinearRealArith | z3siri-base | 0.724636 |
| QF_NonLinearRealArith | Z3-alpha-base | 0.724636 |
| QF_NonLinearRealArith | cvc5 | 0.723611 |
| QF_Bitvec | Z3-alpha-base | 0.705357 |
| QF_Bitvec | z3siri-base | 0.705042 |
| QF_NonLinearRealArith | z3siri | 0.700246 |
| QF_NonLinearRealArith | Yices2 | 0.664444 |
| Arith | UltimateEliminator+MathSAT | 0.644235 |
| QF_Bitvec | Z3-Owl-base | 0.638352 |
| QF_Bitvec | Z3-Owl | 0.607271 |
| QF_Bitvec | bv_decide-nokernel | 0.605519 |
| QF_NonLinearRealArith | SMT-RAT | 0.599381 |
| QF_Bitvec | bv_decide | 0.565908 |
| QF_Strings | Z3-Noodler-Mocha | 0.558917 |
| QF_FPArith | colibri2 | 0.538613 |
| QF_Equality_LinearArith | OpenSMT | 0.52808 |
| QF_Strings | Z3-Noodler | 0.516052 |
| QF_Strings | Z3-Noodler-Mocha-base | 0.511948 |
| QF_Equality_LinearArith | cvc5 | 0.511874 |
| QF_Equality_LinearArith | Yices2 | 0.509198 |
| QF_LinearRealArith | Yices2 | 0.505457 |
| QF_LinearRealArith | cvc5 | 0.499697 |
| QF_Strings | OSTRICH | 0.497803 |
| QF_LinearRealArith | OpenSMT | 0.49397 |
| QF_LinearRealArith | Z3-alpha | 0.491118 |
| QF_LinearRealArith | Z3-alpha-base | 0.476986 |
| QF_Equality_LinearArith | SMTInterpol | 0.472464 |
| QF_LinearIntArith | OpenSMT | 0.464054 |
| QF_LinearIntArith | Yices2 | 0.449261 |
| QF_Equality_Bitvec | Bitwuzla | 0.446885 |
| QF_LinearIntArith | cvc5 | 0.445385 |
| QF_Equality_Bitvec | Yices2 | 0.433255 |
| QF_Strings | Z3-Noodler-base | 0.424357 |
| QF_Strings | Z3-alpha-base | 0.423304 |
| QF_Strings | Z3-alpha | 0.419508 |
| QF_Strings | cvc5 | 0.4183 |
| QF_Equality_Bitvec | cvc5 | 0.412005 |
| QF_Equality_Bitvec | Z3-Owl | 0.410508 |
| QF_LinearIntArith | SMTInterpol | 0.407141 |
| QF_LinearIntArith | Z3-alpha | 0.392081 |
| QF_Equality_Bitvec | Z3-Owl-base | 0.367703 |
| QF_LinearIntArith | Z3-alpha-base | 0.356251 |
| Equality_MachineArith | SMTInterpol | 0.347059 |
| QF_Datatypes | cvc5 | 0.342175 |
| QF_Equality_Bitvec | SMTInterpol | 0.334507 |
| QF_NonLinearIntArith | z3siri | 0.311815 |
| Equality_NonLinearArith | SMTInterpol | 0.309798 |
| QF_NonLinearIntArith | Z3-alpha | 0.305958 |
| QF_NonLinearIntArith | Z3-alpha-base | 0.30305 |
| QF_NonLinearIntArith | z3siri-base | 0.301782 |
| QF_LinearRealArith | SMTInterpol | 0.283237 |
| Equality | cvc5 | 0.273401 |
| Bitvec | UltimateEliminator+MathSAT | 0.257787 |
| Bitvec | SMTInterpol | 0.21869 |
| Arith | iProver v3.9.3 | 0.215619 |
| QF_NonLinearIntArith | Yices2 | 0.214423 |
| QF_Datatypes | SMTInterpol | 0.19978 |
| QF_Bitvec | SMTInterpol | 0.190801 |
| QF_NonLinearIntArith | cvc5 | 0.172614 |
| Equality | iProver v3.9.3 | 0.152775 |
| QF_FPArith | Z3-Owl | 0.152447 |
| QF_FPArith | Z3-Owl-base | 0.1363 |
| QF_NonLinearRealArith | SMTInterpol | 0.101422 |
| Arith | Amaya | 0.076665 |
| Arith | SMTInterpol | 0.063015 |
| QF_Equality_NonLinearArith | cvc5 | 0.050809 |
| QF_Equality_NonLinearArith | Yices2 | 0.038509 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.030633 |
| FPArith | UltimateEliminator+MathSAT | 0.027292 |
| Equality | SMTInterpol | 0.017771 |
| Equality | Yices2 | 0.015653 |
| Equality_MachineArith | Bitwuzla | 0.013497 |
| Arith | SMT-RAT | 0.009824 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.001311 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.000466 |
| QF_NonLinearIntArith | SMTInterpol | 0.000148 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000128 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Equality_LinearArith | SMTInterpol | -8.457622 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler-Mocha | 4.489188 |
| QF_Strings | Z3-Noodler | 4.358861 |
| QF_Strings | Z3-Noodler-Mocha-base | 4.347698 |
| QF_Bitvec | Bitwuzla-MachBV | 3.588967 |
| QF_Equality | Yices2 | 3.576554 |
| QF_Equality_Bitvec | Bitwuzla | 3.568208 |
| QF_Equality | OpenSMT | 3.531731 |
| QF_Bitvec | Bitwuzla | 3.530933 |
| QF_Equality | cvc5 | 3.518711 |
| QF_Bitvec | Bitwuzla-MachBV-base | 3.505604 |
| QF_Bitvec | Yices2 | 3.453825 |
| QF_Equality_Bitvec | Yices2 | 3.384506 |
| QF_Equality | SMTInterpol | 3.373436 |
| QF_Equality_Bitvec | Z3-Owl | 3.23751 |
| QF_Strings | Z3-alpha | 3.139316 |
| QF_Strings | cvc5 | 3.092534 |
| QF_Strings | Z3-Noodler-base | 3.072218 |
| QF_Strings | Z3-alpha-base | 3.066115 |
| QF_Strings | OSTRICH | 3.024859 |
| QF_Equality_Bitvec | Z3-Owl-base | 3.004893 |
| QF_FPArith | Bitwuzla | 2.737822 |
| QF_LinearIntArith | Yices2 | 2.679902 |
| QF_Equality_Bitvec | cvc5 | 2.654697 |
| QF_NonLinearRealArith | Z3-alpha | 2.622561 |
| QF_Equality_LinearArith | SMTInterpol | 2.561301 |
| QF_Bitvec | cvc5 | 2.540237 |
| QF_Equality_LinearArith | Yices2 | 2.513567 |
| QF_NonLinearRealArith | Yices2 | 2.512597 |
| FPArith | Bitwuzla | 2.483116 |
| FPArith | cvc5 | 2.440172 |
| QF_Equality_LinearArith | OpenSMT | 2.373058 |
| QF_Equality_LinearArith | cvc5 | 2.373058 |
| Equality_LinearArith | cvc5 | 2.32693 |
| Arith | Z3-alpha | 2.324045 |
| QF_NonLinearRealArith | cvc5 | 2.277874 |
| QF_LinearIntArith | Z3-alpha | 2.239078 |
| QF_NonLinearIntArith | Z3-alpha | 2.235206 |
| Arith | Z3-alpha-base | 2.210497 |
| Arith | YicesQS | 2.204094 |
| QF_Bitvec | Z3-alpha | 2.104016 |
| QF_FPArith | cvc5 | 2.09898 |
| QF_NonLinearRealArith | Z3-alpha-base | 2.082366 |
| QF_NonLinearRealArith | z3siri-base | 2.082366 |
| QF_NonLinearIntArith | Yices2 | 2.000445 |
| Bitvec | YicesQS | 1.977596 |
| QF_NonLinearIntArith | Z3-alpha-base | 1.954595 |
| QF_NonLinearIntArith | z3siri-base | 1.932556 |
| QF_LinearIntArith | Z3-alpha-base | 1.921698 |
| QF_Bitvec | z3siri | 1.91945 |
| QF_NonLinearRealArith | SMT-RAT | 1.915574 |
| QF_Bitvec | Z3-alpha-base | 1.900787 |
| QF_Bitvec | z3siri-base | 1.897169 |
| QF_NonLinearRealArith | z3siri | 1.844588 |
| QF_LinearRealArith | Yices2 | 1.802814 |
| Bitvec | Bitwuzla | 1.749701 |
| QF_Bitvec | Z3-Owl | 1.71524 |
| QF_LinearRealArith | OpenSMT | 1.679536 |
| QF_LinearIntArith | OpenSMT | 1.635966 |
| Arith | cvc5 | 1.583498 |
| Arith | UltimateEliminator+MathSAT | 1.500558 |
| QF_LinearIntArith | cvc5 | 1.48245 |
| QF_Bitvec | Z3-Owl-base | 1.472935 |
| QF_Equality_Bitvec | SMTInterpol | 1.424737 |
| QF_LinearRealArith | cvc5 | 1.412081 |
| QF_NonLinearIntArith | z3siri | 1.35544 |
| QF_LinearRealArith | Z3-alpha-base | 1.345303 |
| Bitvec | cvc5 | 1.324195 |
| Equality_NonLinearArith | cvc5 | 1.32201 |
| QF_Bitvec | bv_decide-nokernel | 1.287087 |
| QF_FPArith | colibri2 | 1.261642 |
| QF_LinearIntArith | SMTInterpol | 1.184752 |
| QF_LinearRealArith | Z3-alpha | 1.167808 |
| QF_Bitvec | bv_decide | 1.140448 |
| Equality_LinearArith | iProver v3.9.3 | 1.111824 |
| QF_Equality_NonLinearArith | Yices2 | 0.891259 |
| Equality_MachineArith | cvc5 | 0.86174 |
| QF_LinearRealArith | SMTInterpol | 0.831842 |
| QF_NonLinearIntArith | cvc5 | 0.61054 |
| QF_Equality_NonLinearArith | cvc5 | 0.571207 |
| Equality_NonLinearArith | iProver v3.9.3 | 0.37189 |
| Equality_MachineArith | SMTInterpol | 0.319065 |
| Equality_NonLinearArith | SMTInterpol | 0.316808 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.316064 |
| QF_FPArith | Z3-Owl | 0.295625 |
| Bitvec | UltimateEliminator+MathSAT | 0.291017 |
| QF_FPArith | Z3-Owl-base | 0.252326 |
| Bitvec | SMTInterpol | 0.21869 |
| Equality | cvc5 | 0.187987 |
| QF_Bitvec | SMTInterpol | 0.135821 |
| QF_Datatypes | SMTInterpol | 0.123183 |
| Equality | iProver v3.9.3 | 0.11882 |
| QF_NonLinearRealArith | SMTInterpol | 0.104124 |
| QF_Datatypes | cvc5 | 0.093622 |
| Arith | iProver v3.9.3 | 0.089062 |
| Arith | SMTInterpol | 0.072546 |
| FPArith | UltimateEliminator+MathSAT | 0.044172 |
| Equality_MachineArith | Bitwuzla | 0.032099 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.013333 |
| Equality | Yices2 | 0.012972 |
| Arith | SMT-RAT | 0.010697 |
| Equality | SMTInterpol | 0.008524 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.007611 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000944 |
| QF_NonLinearIntArith | SMTInterpol | 0.000137 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.40824 |
| Arith | Amaya | -6.44335 |
| Equality_LinearArith | SMTInterpol | -8.457622 |