The International Satisfiability Modulo Theories (SMT) Competition.
Page generated on 2026-07-25
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| cvc5 (26.303383) | cvc5 (26.303383) | — | cvc5 (26.303383) | cvc5 (17.691139) |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.336052 |
| QF_NonLinearRealArith | z3-BooledASS | 5.066835 |
| QF_NonLinearRealArith | z3-BooledASS-base | 5.066835 |
| Equality_NonLinearArith | z3-BooledASS | 4.616548 |
| QF_NonLinearRealArith | Yices2 | 4.534646 |
| Equality_NonLinearArith | z3-BooledASS-base | 4.498837 |
| QF_LinearRealArith | OpenSMT | 4.42506 |
| Equality_LinearArith | cvc5 | 4.208953 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 4.136591 |
| Equality_NonLinearArith | cvc5 | 4.086622 |
| QF_Equality_Bitvec | Bitwuzla | 4.030668 |
| QF_LinearRealArith | Yices2 | 3.954995 |
| Equality_LinearArith | z3-BooledASS | 3.90598 |
| Equality_LinearArith | z3-BooledASS-base | 3.88597 |
| Equality | z3-BooledASS-base | 3.677891 |
| Equality | z3-BooledASS | 3.677533 |
| QF_Equality_NonLinearArith | SMTInterpol | 3.475599 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 3.454918 |
| QF_Equality_NonLinearArith | z3-BooledASS | 3.450271 |
| QF_Equality_LinearArith | z3-BooledASS | 3.199606 |
| QF_Equality_LinearArith | z3-BooledASS-base | 3.199606 |
| QF_Equality_LinearArith | Yices2 | 2.609245 |
| Equality_MachineArith | cvc5 | 2.532215 |
| QF_LinearRealArith | cvc5 | 2.482265 |
| QF_LinearRealArith | z3-BooledASS | 2.467619 |
| QF_LinearRealArith | z3-BooledASS-base | 2.467619 |
| Equality_MachineArith | z3-BooledASS-base | 2.305761 |
| QF_LinearIntArith | z3-BooledASS | 2.085011 |
| QF_LinearIntArith | z3-BooledASS-base | 2.085011 |
| QF_Bitvec | Bitwuzla | 2.000822 |
| QF_LinearIntArith | Yices2 | 1.784286 |
| QF_Equality | Yices2 | 1.680968 |
| QF_Equality | z3-BooledASS-base | 1.672567 |
| QF_Equality | z3-BooledASS | 1.672567 |
| Equality | SMTInterpol | 1.492511 |
| QF_NonLinearIntArith | Yices2 | 1.477202 |
| QF_Strings | z3-BooledASS | 1.471756 |
| QF_Strings | z3-BooledASS-base | 1.471756 |
| QF_LinearIntArith | OpenSMT | 1.470179 |
| QF_Strings | cvc5 | 1.40217 |
| QF_Equality_LinearArith | OpenSMT | 1.351136 |
| QF_NonLinearIntArith | cvc5 | 1.264562 |
| QF_Equality_Bitvec | Yices2 | 1.210927 |
| QF_FPArith | Bitwuzla | 1.193529 |
| QF_LinearIntArith | SMTInterpol | 1.127343 |
| QF_Equality_Bitvec | z3-BooledASS-base | 1.105478 |
| QF_Equality_Bitvec | z3-BooledASS | 1.104658 |
| QF_FPArith | cvc5 | 1.098102 |
| Equality_MachineArith | SMTInterpol | 1.070017 |
| Equality_LinearArith | SMTInterpol | 1.069543 |
| QF_NonLinearIntArith | z3-BooledASS-base | 1.00107 |
| QF_Equality | OpenSMT (min-ucore) | 0.998881 |
| QF_NonLinearIntArith | z3-BooledASS | 0.99169 |
| QF_LinearIntArith | cvc5 | 0.982466 |
| QF_Bitvec | z3-BooledASS-base | 0.967715 |
| QF_FPArith | z3-BooledASS-base | 0.91463 |
| QF_LinearRealArith | SMTInterpol | 0.908195 |
| QF_Equality_Bitvec | SMTInterpol | 0.872413 |
| QF_Equality | OpenSMT | 0.86604 |
| QF_Equality | SMTInterpol | 0.797943 |
| QF_Equality | plat-smt | 0.77653 |
| QF_LinearIntArith | OpenSMT (min-ucore) | 0.722998 |
| QF_Bitvec | z3-BooledASS | 0.636078 |
| FPArith | Bitwuzla | 0.591979 |
| FPArith | z3-BooledASS-base | 0.568991 |
| QF_Equality | cvc5 | 0.568251 |
| QF_Datatypes | cvc5 | 0.559615 |
| FPArith | cvc5 | 0.546459 |
| QF_Equality_NonLinearArith | Yices2 | 0.509119 |
| QF_Equality_NonLinearArith | cvc5 | 0.413973 |
| Equality_MachineArith | z3-BooledASS | 0.356038 |
| QF_Bitvec | cvc5 | 0.329659 |
| QF_Equality_Bitvec | cvc5 | 0.3125 |
| QF_FPArith | z3-BooledASS | 0.191135 |
| QF_Bitvec | SMTInterpol | 0.166672 |
| Arith | cvc5 | 0.135101 |
| QF_Datatypes | z3-BooledASS | 0.118617 |
| QF_Datatypes | z3-BooledASS-base | 0.118546 |
| Equality_NonLinearArith | SMTInterpol | 0.074513 |
| QF_Equality_LinearArith | cvc5 | 0.024714 |
| Bitvec | cvc5 | 0.016906 |
| Bitvec | Bitwuzla | 0.011661 |
| Bitvec | z3-BooledASS-base | 0.009835 |
| Bitvec | z3-BooledASS | 0.009835 |
| QF_Equality_LinearArith | SMTInterpol | 0.009646 |
| Arith | z3-BooledASS-base | 0.008118 |
| Arith | z3-BooledASS | 0.008118 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | 0.006974 |
| QF_NonLinearRealArith | cvc5 | 0.002799 |
| QF_NonLinearRealArith | SMTInterpol | 0.002181 |
| QF_NonLinearIntArith | SMTInterpol | 0.000763 |
| QF_Datatypes | SMTInterpol | 0.00035 |
| Arith | SMTInterpol | 0.000248 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 5.1e-05 |
| Equality_MachineArith | Bitwuzla | 2e-06 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| Bitvec | SMTInterpol | 0 |
| FPArith | Bitwuzla-fixed | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| FPArith | z3-BooledASS | 0 |
| Bitvec | Bitwuzla-fixed | 0 |
| Equality_MachineArith | Bitwuzla-fixed | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.179104 |
| QF_Bitvec | Yices2 | -12.299175 |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.336052 |
| QF_NonLinearRealArith | z3-BooledASS | 5.066835 |
| QF_NonLinearRealArith | z3-BooledASS-base | 5.066835 |
| Equality_NonLinearArith | z3-BooledASS | 4.616548 |
| QF_NonLinearRealArith | Yices2 | 4.534646 |
| Equality_NonLinearArith | z3-BooledASS-base | 4.498837 |
| QF_LinearRealArith | OpenSMT | 4.42506 |
| Equality_LinearArith | cvc5 | 4.208953 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 4.136591 |
| Equality_NonLinearArith | cvc5 | 4.086622 |
| QF_Equality_Bitvec | Bitwuzla | 4.030668 |
| QF_LinearRealArith | Yices2 | 3.954995 |
| Equality_LinearArith | z3-BooledASS | 3.90598 |
| Equality_LinearArith | z3-BooledASS-base | 3.88597 |
| Equality | z3-BooledASS-base | 3.677891 |
| Equality | z3-BooledASS | 3.677533 |
| QF_Equality_NonLinearArith | SMTInterpol | 3.475599 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 3.454918 |
| QF_Equality_NonLinearArith | z3-BooledASS | 3.450271 |
| QF_Equality_LinearArith | z3-BooledASS | 3.199606 |
| QF_Equality_LinearArith | z3-BooledASS-base | 3.199606 |
| QF_Equality_LinearArith | Yices2 | 2.609245 |
| Equality_MachineArith | cvc5 | 2.532215 |
| QF_LinearRealArith | cvc5 | 2.482265 |
| QF_LinearRealArith | z3-BooledASS | 2.467619 |
| QF_LinearRealArith | z3-BooledASS-base | 2.467619 |
| Equality_MachineArith | z3-BooledASS-base | 2.305761 |
| QF_LinearIntArith | z3-BooledASS | 2.085011 |
| QF_LinearIntArith | z3-BooledASS-base | 2.085011 |
| QF_Bitvec | Bitwuzla | 2.000822 |
| QF_LinearIntArith | Yices2 | 1.784286 |
| QF_Equality | Yices2 | 1.680968 |
| QF_Equality | z3-BooledASS-base | 1.672567 |
| QF_Equality | z3-BooledASS | 1.672567 |
| Equality | SMTInterpol | 1.492646 |
| QF_NonLinearIntArith | Yices2 | 1.477202 |
| QF_Strings | z3-BooledASS | 1.471756 |
| QF_Strings | z3-BooledASS-base | 1.471756 |
| QF_LinearIntArith | OpenSMT | 1.470179 |
| QF_Strings | cvc5 | 1.40217 |
| QF_Equality_LinearArith | OpenSMT | 1.351136 |
| QF_NonLinearIntArith | cvc5 | 1.264562 |
| QF_Equality_Bitvec | Yices2 | 1.210927 |
| QF_FPArith | Bitwuzla | 1.193529 |
| QF_LinearIntArith | SMTInterpol | 1.127343 |
| QF_Equality_Bitvec | z3-BooledASS-base | 1.105478 |
| QF_Equality_Bitvec | z3-BooledASS | 1.104658 |
| QF_FPArith | cvc5 | 1.098102 |
| Equality_LinearArith | SMTInterpol | 1.073063 |
| Equality_MachineArith | SMTInterpol | 1.070017 |
| QF_NonLinearIntArith | z3-BooledASS-base | 1.00107 |
| QF_Equality | OpenSMT (min-ucore) | 0.998881 |
| QF_NonLinearIntArith | z3-BooledASS | 0.99169 |
| QF_LinearIntArith | cvc5 | 0.982466 |
| QF_Bitvec | z3-BooledASS-base | 0.967715 |
| QF_FPArith | z3-BooledASS-base | 0.91463 |
| QF_LinearRealArith | SMTInterpol | 0.91361 |
| QF_Equality_Bitvec | SMTInterpol | 0.872413 |
| QF_Equality | OpenSMT | 0.86604 |
| QF_Equality | SMTInterpol | 0.797943 |
| QF_Equality | plat-smt | 0.77653 |
| QF_LinearIntArith | OpenSMT (min-ucore) | 0.722998 |
| QF_Bitvec | z3-BooledASS | 0.636078 |
| FPArith | Bitwuzla | 0.591979 |
| FPArith | z3-BooledASS-base | 0.568991 |
| QF_Equality | cvc5 | 0.568251 |
| QF_Datatypes | cvc5 | 0.559615 |
| FPArith | cvc5 | 0.546459 |
| QF_Equality_NonLinearArith | Yices2 | 0.509119 |
| QF_Equality_NonLinearArith | cvc5 | 0.413973 |
| Equality_MachineArith | z3-BooledASS | 0.356038 |
| QF_Bitvec | cvc5 | 0.329659 |
| QF_Equality_Bitvec | cvc5 | 0.3125 |
| QF_FPArith | z3-BooledASS | 0.191135 |
| QF_Bitvec | SMTInterpol | 0.18335 |
| Arith | cvc5 | 0.135101 |
| QF_Datatypes | z3-BooledASS | 0.118617 |
| QF_Datatypes | z3-BooledASS-base | 0.118546 |
| Equality_NonLinearArith | SMTInterpol | 0.074513 |
| QF_Equality_LinearArith | cvc5 | 0.024714 |
| Bitvec | cvc5 | 0.016906 |
| Bitvec | Bitwuzla | 0.011661 |
| Bitvec | z3-BooledASS-base | 0.009835 |
| Bitvec | z3-BooledASS | 0.009835 |
| QF_Equality_LinearArith | SMTInterpol | 0.009646 |
| Arith | z3-BooledASS-base | 0.008118 |
| Arith | z3-BooledASS | 0.008118 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | 0.006974 |
| QF_NonLinearRealArith | cvc5 | 0.002799 |
| QF_NonLinearRealArith | SMTInterpol | 0.002181 |
| QF_NonLinearIntArith | SMTInterpol | 0.000763 |
| QF_Datatypes | SMTInterpol | 0.000436 |
| Arith | SMTInterpol | 0.000248 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 5.1e-05 |
| Equality_MachineArith | Bitwuzla | 2e-06 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| Bitvec | SMTInterpol | 0 |
| FPArith | Bitwuzla-fixed | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| FPArith | z3-BooledASS | 0 |
| Bitvec | Bitwuzla-fixed | 0 |
| Equality_MachineArith | Bitwuzla-fixed | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.179104 |
| QF_Bitvec | Yices2 | -12.299175 |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 5.336052 |
| QF_NonLinearRealArith | z3-BooledASS | 5.066835 |
| QF_NonLinearRealArith | z3-BooledASS-base | 5.066835 |
| Equality_NonLinearArith | z3-BooledASS | 4.616548 |
| QF_NonLinearRealArith | Yices2 | 4.534646 |
| Equality_NonLinearArith | z3-BooledASS-base | 4.498837 |
| QF_LinearRealArith | OpenSMT | 4.42506 |
| Equality_LinearArith | cvc5 | 4.208953 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 4.136591 |
| Equality_NonLinearArith | cvc5 | 4.086622 |
| QF_Equality_Bitvec | Bitwuzla | 4.030668 |
| QF_LinearRealArith | Yices2 | 3.954995 |
| Equality_LinearArith | z3-BooledASS | 3.90598 |
| Equality_LinearArith | z3-BooledASS-base | 3.88597 |
| Equality | z3-BooledASS-base | 3.677891 |
| Equality | z3-BooledASS | 3.677533 |
| QF_Equality_NonLinearArith | SMTInterpol | 3.475599 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 3.454918 |
| QF_Equality_NonLinearArith | z3-BooledASS | 3.450271 |
| QF_Equality_LinearArith | z3-BooledASS | 3.199606 |
| QF_Equality_LinearArith | z3-BooledASS-base | 3.199606 |
| QF_Equality_LinearArith | Yices2 | 2.609245 |
| Equality_MachineArith | cvc5 | 2.532215 |
| QF_LinearRealArith | cvc5 | 2.482265 |
| QF_LinearRealArith | z3-BooledASS | 2.467619 |
| QF_LinearRealArith | z3-BooledASS-base | 2.467619 |
| Equality_MachineArith | z3-BooledASS-base | 2.305761 |
| QF_LinearIntArith | z3-BooledASS | 2.085011 |
| QF_LinearIntArith | z3-BooledASS-base | 2.085011 |
| QF_Bitvec | Bitwuzla | 2.000822 |
| QF_LinearIntArith | Yices2 | 1.784286 |
| QF_Equality | Yices2 | 1.680968 |
| QF_Equality | z3-BooledASS-base | 1.672567 |
| QF_Equality | z3-BooledASS | 1.672567 |
| Equality | SMTInterpol | 1.492646 |
| QF_NonLinearIntArith | Yices2 | 1.477202 |
| QF_Strings | z3-BooledASS | 1.471756 |
| QF_Strings | z3-BooledASS-base | 1.471756 |
| QF_LinearIntArith | OpenSMT | 1.470179 |
| QF_Strings | cvc5 | 1.40217 |
| QF_Equality_LinearArith | OpenSMT | 1.351136 |
| QF_NonLinearIntArith | cvc5 | 1.264562 |
| QF_Equality_Bitvec | Yices2 | 1.210927 |
| QF_FPArith | Bitwuzla | 1.193529 |
| QF_LinearIntArith | SMTInterpol | 1.127343 |
| QF_Equality_Bitvec | z3-BooledASS-base | 1.105478 |
| QF_Equality_Bitvec | z3-BooledASS | 1.104658 |
| QF_FPArith | cvc5 | 1.098102 |
| Equality_LinearArith | SMTInterpol | 1.073063 |
| Equality_MachineArith | SMTInterpol | 1.070017 |
| QF_NonLinearIntArith | z3-BooledASS-base | 1.00107 |
| QF_Equality | OpenSMT (min-ucore) | 0.998881 |
| QF_NonLinearIntArith | z3-BooledASS | 0.99169 |
| QF_LinearIntArith | cvc5 | 0.982466 |
| QF_Bitvec | z3-BooledASS-base | 0.967715 |
| QF_FPArith | z3-BooledASS-base | 0.91463 |
| QF_LinearRealArith | SMTInterpol | 0.91361 |
| QF_Equality_Bitvec | SMTInterpol | 0.872413 |
| QF_Equality | OpenSMT | 0.86604 |
| QF_Equality | SMTInterpol | 0.797943 |
| QF_Equality | plat-smt | 0.77653 |
| QF_LinearIntArith | OpenSMT (min-ucore) | 0.722998 |
| QF_Bitvec | z3-BooledASS | 0.636078 |
| FPArith | Bitwuzla | 0.591979 |
| FPArith | z3-BooledASS-base | 0.568991 |
| QF_Equality | cvc5 | 0.568251 |
| QF_Datatypes | cvc5 | 0.559615 |
| FPArith | cvc5 | 0.546459 |
| QF_Equality_NonLinearArith | Yices2 | 0.509119 |
| QF_Equality_NonLinearArith | cvc5 | 0.413973 |
| Equality_MachineArith | z3-BooledASS | 0.356038 |
| QF_Bitvec | cvc5 | 0.329659 |
| QF_Equality_Bitvec | cvc5 | 0.3125 |
| QF_FPArith | z3-BooledASS | 0.191135 |
| QF_Bitvec | SMTInterpol | 0.18335 |
| Arith | cvc5 | 0.135101 |
| QF_Datatypes | z3-BooledASS | 0.118617 |
| QF_Datatypes | z3-BooledASS-base | 0.118546 |
| Equality_NonLinearArith | SMTInterpol | 0.074513 |
| QF_Equality_LinearArith | cvc5 | 0.024714 |
| Bitvec | cvc5 | 0.016906 |
| Bitvec | Bitwuzla | 0.011661 |
| Bitvec | z3-BooledASS-base | 0.009835 |
| Bitvec | z3-BooledASS | 0.009835 |
| QF_Equality_LinearArith | SMTInterpol | 0.009646 |
| Arith | z3-BooledASS-base | 0.008118 |
| Arith | z3-BooledASS | 0.008118 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | 0.006974 |
| QF_NonLinearRealArith | cvc5 | 0.002799 |
| QF_NonLinearRealArith | SMTInterpol | 0.002181 |
| QF_NonLinearIntArith | SMTInterpol | 0.000763 |
| QF_Datatypes | SMTInterpol | 0.000436 |
| Arith | SMTInterpol | 0.000248 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 5.1e-05 |
| Equality_MachineArith | Bitwuzla | 2e-06 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| Bitvec | SMTInterpol | 0 |
| FPArith | Bitwuzla-fixed | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| FPArith | z3-BooledASS | 0 |
| Bitvec | Bitwuzla-fixed | 0 |
| Equality_MachineArith | Bitwuzla-fixed | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.179104 |
| QF_Bitvec | Yices2 | -12.299175 |
| Division | Solver | Contribution |
|---|---|---|
| Equality | cvc5 | 4.769378 |
| Equality_NonLinearArith | z3-BooledASS | 4.33791 |
| Equality_NonLinearArith | z3-BooledASS-base | 4.324857 |
| Equality_LinearArith | cvc5 | 3.940835 |
| Equality_LinearArith | z3-BooledASS | 3.869918 |
| Equality_LinearArith | z3-BooledASS-base | 3.855606 |
| Equality | z3-BooledASS | 3.582186 |
| Equality | z3-BooledASS-base | 3.565756 |
| QF_LinearRealArith | OpenSMT | 2.845995 |
| Equality_MachineArith | cvc5 | 2.477962 |
| Equality_MachineArith | z3-BooledASS-base | 2.253861 |
| QF_LinearRealArith | OpenSMT (min-ucore) | 1.758847 |
| QF_Equality | Yices2 | 1.576534 |
| QF_Equality | z3-BooledASS-base | 1.569987 |
| QF_Equality | z3-BooledASS | 1.569987 |
| QF_LinearRealArith | Yices2 | 1.438212 |
| QF_Strings | z3-BooledASS | 1.427753 |
| QF_Strings | z3-BooledASS-base | 1.427753 |
| QF_LinearIntArith | Yices2 | 1.409128 |
| QF_Strings | cvc5 | 1.354806 |
| QF_NonLinearIntArith | Yices2 | 1.349978 |
| QF_Bitvec | Bitwuzla | 1.305933 |
| Equality_NonLinearArith | cvc5 | 1.259926 |
| Equality | SMTInterpol | 1.191931 |
| QF_Equality_Bitvec | Bitwuzla | 1.127285 |
| QF_Equality_Bitvec | Yices2 | 1.088423 |
| QF_NonLinearIntArith | cvc5 | 1.05192 |
| QF_Equality_Bitvec | z3-BooledASS-base | 1.046782 |
| QF_Equality_Bitvec | z3-BooledASS | 1.046782 |
| QF_FPArith | Bitwuzla | 1.027053 |
| QF_LinearIntArith | z3-BooledASS-base | 1.016865 |
| QF_LinearIntArith | z3-BooledASS | 1.016865 |
| Equality_LinearArith | SMTInterpol | 1.005266 |
| QF_NonLinearIntArith | z3-BooledASS-base | 0.969901 |
| QF_NonLinearIntArith | z3-BooledASS | 0.961118 |
| QF_NonLinearRealArith | z3-BooledASS-base | 0.914248 |
| Equality_MachineArith | SMTInterpol | 0.90937 |
| QF_NonLinearRealArith | z3-BooledASS | 0.877739 |
| QF_Equality | OpenSMT | 0.866005 |
| QF_Bitvec | z3-BooledASS-base | 0.823008 |
| QF_FPArith | cvc5 | 0.787405 |
| QF_Equality | SMTInterpol | 0.726559 |
| QF_FPArith | z3-BooledASS-base | 0.715688 |
| QF_Equality | plat-smt | 0.640973 |
| QF_Bitvec | z3-BooledASS | 0.636078 |
| QF_LinearIntArith | OpenSMT | 0.630402 |
| FPArith | Bitwuzla | 0.591979 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.573925 |
| QF_Equality_Bitvec | SMTInterpol | 0.562308 |
| QF_LinearIntArith | cvc5 | 0.549122 |
| FPArith | cvc5 | 0.546459 |
| QF_Equality | cvc5 | 0.499171 |
| QF_Equality_NonLinearArith | Yices2 | 0.451602 |
| QF_LinearIntArith | OpenSMT (min-ucore) | 0.39477 |
| QF_NonLinearRealArith | Yices2 | 0.379115 |
| Equality_MachineArith | z3-BooledASS | 0.354129 |
| QF_Equality_LinearArith | Yices2 | 0.325073 |
| QF_LinearRealArith | cvc5 | 0.282922 |
| QF_LinearRealArith | z3-BooledASS | 0.26472 |
| QF_LinearRealArith | z3-BooledASS-base | 0.26472 |
| QF_Equality | OpenSMT (min-ucore) | 0.245452 |
| QF_LinearIntArith | SMTInterpol | 0.243534 |
| QF_Equality_NonLinearArith | z3-BooledASS | 0.190871 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 0.190871 |
| QF_FPArith | z3-BooledASS | 0.18713 |
| QF_LinearRealArith | SMTInterpol | 0.113996 |
| Equality_NonLinearArith | SMTInterpol | 0.069917 |
| QF_Equality_NonLinearArith | cvc5 | 0.06357 |
| QF_Bitvec | cvc5 | 0.060251 |
| Arith | cvc5 | 0.023419 |
| QF_Bitvec | SMTInterpol | 0.019243 |
| FPArith | z3-BooledASS-base | 0.018435 |
| QF_Equality_LinearArith | z3-BooledASS | 0.016503 |
| QF_Equality_LinearArith | z3-BooledASS-base | 0.016503 |
| Bitvec | Bitwuzla | 0.011661 |
| QF_Equality_Bitvec | cvc5 | 0.010991 |
| Bitvec | z3-BooledASS-base | 0.009835 |
| Bitvec | z3-BooledASS | 0.009835 |
| Arith | z3-BooledASS | 0.008118 |
| Arith | z3-BooledASS-base | 0.008118 |
| Bitvec | cvc5 | 0.007387 |
| QF_Equality_LinearArith | cvc5 | 0.003749 |
| QF_NonLinearRealArith | SMTInterpol | 0.002181 |
| QF_NonLinearRealArith | cvc5 | 0.001866 |
| QF_NonLinearIntArith | SMTInterpol | 0.000763 |
| QF_Equality_LinearArith | SMTInterpol | 0.000591 |
| Arith | SMTInterpol | 0.000248 |
| QF_Equality_LinearArith | OpenSMT | 5e-05 |
| QF_Datatypes | z3-BooledASS | 4.8e-05 |
| QF_Datatypes | z3-BooledASS-base | 4.8e-05 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 3.2e-05 |
| QF_Equality_LinearArith | OpenSMT (min-ucore) | 1.7e-05 |
| QF_Datatypes | SMTInterpol | 2e-06 |
| Equality_MachineArith | Bitwuzla | 1e-06 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0 |
| QF_Datatypes | cvc5 | 0 |
| Bitvec | UltimateEliminator+MathSAT | 0 |
| Bitvec | SMTInterpol | 0 |
| FPArith | Bitwuzla-fixed | 0 |
| FPArith | UltimateEliminator+MathSAT | 0 |
| FPArith | z3-BooledASS | 0 |
| Bitvec | Bitwuzla-fixed | 0 |
| Equality_MachineArith | Bitwuzla-fixed | 0 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0 |
| Equality | UltimateEliminator+MathSAT | 0 |
| Arith | UltimateEliminator+MathSAT | -6.179104 |
| QF_Bitvec | Yices2 | -12.299175 |