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 (40.373142) | cvc5 (40.373142) | cvc5 (9.533053) | cvc5-cvc5-xyz (13.580344) | cvc5 (28.488905) |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler | 3.478712 |
| QF_Bitvec | Bitwuzla-MachBV | 3.285259 |
| QF_Bitvec | bitwuzla-dandelion-base | 3.243258 |
| QF_Bitvec | Bitwuzla-MachBV-base | 3.240642 |
| QF_Bitvec | Bitwuzla-SPFD-base | 3.240642 |
| QF_Bitvec | Bitwuzla | 3.2328 |
| QF_Bitvec | bitwuzla-dandelion | 3.224968 |
| QF_Strings | OSTRICH | 3.219863 |
| QF_Bitvec | Bitwuzla-SPFD | 3.185949 |
| QF_Equality | OpenSMT-SMTS-seq | 3.147367 |
| QF_Equality | z3-BooledASS-base | 3.147367 |
| QF_Equality | z3-BooledASS | 3.147367 |
| QF_Equality | cvc5 | 3.147367 |
| QF_Equality | OpenSMT-SMTS-seq-base | 3.147367 |
| QF_Equality | OpenSMT | 3.147367 |
| QF_Equality | cvc5-cvc5-xyz | 3.147367 |
| QF_Equality | cvc5-cvc5-xyz-base | 3.147367 |
| QF_Equality | Yices2 | 3.147367 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 3.084196 |
| QF_Equality_Bitvec | Bitwuzla | 3.066851 |
| QF_Equality_Bitvec | bitwuzla-dandelion-base | 3.064378 |
| QF_Bitvec | bv_decide-nokernel | 3.049983 |
| QF_Bitvec | bv_decide | 3.042375 |
| QF_Equality | SMTInterpol | 3.031877 |
| QF_FPArith | Bitwuzla | 3.016382 |
| QF_FPArith | bitwuzla-dandelion-base | 3.008009 |
| QF_Bitvec | cvc5 | 2.976841 |
| QF_Bitvec | cvc5-cvc5-xyz | 2.976841 |
| QF_Bitvec | cvc5-cvc5-xyz-base | 2.974335 |
| QF_Equality_LinearArith | z3-BooledASS-base | 2.936114 |
| QF_Equality_LinearArith | z3-BooledASS | 2.936114 |
| QF_Bitvec | NeuroSym | 2.934378 |
| QF_Equality_Bitvec | Yices2 | 2.929858 |
| FPArith | Bitwuzla | 2.886303 |
| QF_FPArith | cvc5-cvc5-xyz | 2.879715 |
| QF_FPArith | cvc5 | 2.879715 |
| QF_FPArith | cvc5-cvc5-xyz-base | 2.875623 |
| QF_Equality_LinearArith | SMTInterpol | 2.840957 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz-base | 2.812556 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz | 2.810187 |
| QF_Equality_Bitvec | cvc5 | 2.805452 |
| QF_Equality_LinearArith | cvc5 | 2.805274 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz-base | 2.802041 |
| QF_LinearIntArith | QiuQi | 2.785036 |
| QF_Equality_LinearArith | OpenSMT | 2.782683 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq-base | 2.782683 |
| QF_Equality_Bitvec | z3-BooledASS-base | 2.727902 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz | 2.699575 |
| QF_Equality_LinearArith | Yices2 | 2.699575 |
| FPArith | cvc5 | 2.682776 |
| FPArith | cvc5-cvc5-xyz-base | 2.677905 |
| FPArith | cvc5-cvc5-xyz | 2.677905 |
| QF_Bitvec | Z3-GEX | 2.622096 |
| QF_NonLinearRealArith | Z3-GEX | 2.587894 |
| QF_NonLinearRealArith | Z3-alpha2-debug | 2.587894 |
| QF_NonLinearRealArith | Z3-alpha2 | 2.587894 |
| QF_NonLinearRealArith | Z3-GEX-base | 2.582425 |
| QF_NonLinearRealArith | Z3-siri-base | 2.576963 |
| QF_NonLinearRealArith | Z3-siri | 2.571506 |
| QF_LinearIntArith | OpenSMT-SMTS-seq | 2.520381 |
| QF_LinearIntArith | OpenSMT-SMTS-seq-base | 2.50574 |
| QF_LinearIntArith | OpenSMT | 2.494059 |
| QF_LinearIntArith | cvc5 | 2.467874 |
| QF_LinearIntArith | Yices2 | 2.467874 |
| QF_NonLinearIntArith | Z3-Z3++ | 2.455019 |
| QF_NonLinearIntArith | Z3-alpha2 | 2.455019 |
| QF_NonLinearIntArith | Z3-alpha2-debug | 2.44687 |
| Arith | Z3-alpha2-debug | 2.428356 |
| Arith | Z3-alpha2 | 2.428356 |
| QF_NonLinearRealArith | Z3-alpha2-base | 2.426359 |
| QF_NonLinearRealArith | cvc5 | 2.410492 |
| QF_LinearRealArith | OpenSMT | 2.40862 |
| QF_LinearRealArith | Yices2 | 2.40862 |
| QF_LinearIntArith | Z3-alpha2-debug | 2.407315 |
| QF_LinearIntArith | Z3-alpha2 | 2.407315 |
| QF_LinearRealArith | OpenSMT-SMTS-seq-base | 2.401743 |
| QF_Bitvec | Z3-alpha2 | 2.396599 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz-base | 2.394677 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz | 2.394677 |
| QF_Bitvec | Z3-alpha2-debug | 2.39435 |
| QF_NonLinearRealArith | Yices2 | 2.389417 |
| QF_LinearRealArith | OpenSMT-SMTS-seq | 2.381171 |
| QF_FPArith | z3-BooledASS-base | 2.379592 |
| QF_LinearIntArith | Z3-GEX | 2.356006 |
| Bitvec | Bitwuzla-fixed | 2.353264 |
| QF_LinearRealArith | cvc5 | 2.347082 |
| QF_NonLinearRealArith | z3-BooledASS | 2.342336 |
| QF_NonLinearRealArith | z3-BooledASS-base | 2.337133 |
| Bitvec | Bitwuzla | 2.336455 |
| Arith | z3-BooledASS | 2.328853 |
| Arith | z3-BooledASS-base | 2.328853 |
| FPArith | z3-BooledASS-base | 2.32065 |
| Arith | Z3-GEX-base | 2.320298 |
| Arith | Z3-alpha2-base | 2.31176 |
| Bitvec | cvc5-cvc5-xyz | 2.294696 |
| Bitvec | cvc5-cvc5-xyz-base | 2.294696 |
| Bitvec | cvc5 | 2.294696 |
| QF_Bitvec | z3-BooledASS-base | 2.294249 |
| QF_NonLinearIntArith | Z3-GEX | 2.292634 |
| QF_Bitvec | Z3-GEX-base | 2.292049 |
| QF_Bitvec | Z3-alpha2-base | 2.28985 |
| QF_LinearRealArith | z3-BooledASS | 2.286341 |
| QF_LinearRealArith | z3-BooledASS-base | 2.286341 |
| QF_LinearRealArith | Z3-GEX-base | 2.286341 |
| QF_LinearIntArith | z3-BooledASS-base | 2.280079 |
| QF_LinearIntArith | Z3-alpha2-base | 2.274505 |
| Equality_LinearArith | cvc5-cvc5-xyz | 2.26983 |
| Equality_LinearArith | cvc5 | 2.268004 |
| QF_LinearRealArith | cvc5-cvc5-xyz-base | 2.26627 |
| Equality_LinearArith | cvc5-cvc5-xyz-base | 2.266178 |
| QF_LinearIntArith | Z3-GEX-base | 2.263375 |
| QF_LinearRealArith | cvc5-cvc5-xyz | 2.252939 |
| Arith | Z3-GEX | 2.23982 |
| QF_NonLinearIntArith | z3-BooledASS-base | 2.187464 |
| QF_NonLinearIntArith | Z3-siri-base | 2.181693 |
| QF_NonLinearIntArith | Z3-GEX-base | 2.174011 |
| QF_LinearIntArith | cvc5-cvc5-xyz-base | 2.16988 |
| QF_LinearIntArith | cvc5-cvc5-xyz | 2.16716 |
| QF_LinearRealArith | Z3-GEX | 2.141214 |
| Equality_LinearArith | z3-BooledASS-base | 2.118971 |
| QF_LinearIntArith | z3-BooledASS | 2.094365 |
| QF_NonLinearRealArith | SMT-RAT | 2.084393 |
| Bitvec | YicesQS | 2.08362 |
| QF_NonLinearIntArith | Z3-Z3++-base | 2.069757 |
| QF_NonLinearIntArith | Z3-alpha2-base | 2.034338 |
| Equality_LinearArith | z3-BooledASS | 2.029044 |
| Arith | YicesQS | 2.026825 |
| Arith | cvc5-cvc5-xyz-base | 1.971298 |
| Arith | cvc5-cvc5-xyz | 1.971298 |
| Arith | cvc5 | 1.963429 |
| QF_NonLinearIntArith | Yices2 | 1.948034 |
| QF_Equality | plat-smt | 1.938994 |
| QF_LinearIntArith | SMTInterpol | 1.903775 |
| FPArith | bitwuzla-dandelion-base | 1.885442 |
| QF_Strings | cvc5 | 1.871245 |
| QF_Strings | cvc5-cvc5-xyz-base | 1.866304 |
| QF_Strings | cvc5-cvc5-xyz | 1.862779 |
| Bitvec | bitwuzla-dandelion-base | 1.771457 |
| QF_Strings | Z3-GEX | 1.751739 |
| QF_FPArith | colibri2 | 1.744173 |
| QF_Equality_Bitvec | NeuroSym | 1.741379 |
| QF_Strings | Z3-GEX-base | 1.733338 |
| QF_LinearRealArith | SMTInterpol | 1.728548 |
| QF_NonLinearIntArith | cvc5 | 1.695259 |
| QF_Equality_NonLinearArith | Z3-alpha2-debug | 1.681596 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1.681596 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz | 1.674987 |
| QF_Equality_Bitvec | SMTInterpol | 1.669426 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz-base | 1.659863 |
| QF_Strings | z3-BooledASS | 1.650738 |
| QF_Strings | z3-BooledASS-base | 1.650738 |
| Bitvec | bitwuzla-dandelion | 1.642407 |
| QF_Strings | Z3-Noodler-base | 1.634856 |
| Equality_NonLinearArith | cvc5 | 1.619755 |
| Equality_NonLinearArith | cvc5-cvc5-xyz | 1.618589 |
| Equality_NonLinearArith | cvc5-cvc5-xyz-base | 1.618589 |
| QF_NonLinearIntArith | Z3-siri | 1.611597 |
| QF_Equality_NonLinearArith | Z3-alpha2-base | 1.586686 |
| QF_Equality_NonLinearArith | Yices2 | 1.573353 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 1.566707 |
| QF_Equality_NonLinearArith | z3-BooledASS | 1.553458 |
| Bitvec | z3-BooledASS-base | 1.538594 |
| Bitvec | z3-BooledASS | 1.538594 |
| Equality_NonLinearArith | z3-BooledASS-base | 1.505241 |
| Equality_NonLinearArith | z3-BooledASS | 1.499625 |
| QF_Datatypes | cvc5-cvc5-xyz | 1.464269 |
| Equality_MachineArith | cvc5-cvc5-xyz | 1.384531 |
| Equality_MachineArith | cvc5 | 1.38103 |
| Equality_MachineArith | cvc5-cvc5-xyz-base | 1.370554 |
| QF_Equality_Bitvec | z3-BooledASS | 1.35207 |
| Arith | UltimateEliminator+MathSAT | 1.290786 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz | 1.252359 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz-base | 1.24643 |
| QF_Equality_NonLinearArith | cvc5 | 1.240516 |
| QF_Datatypes | cvc5-cvc5-xyz-base | 1.087534 |
| Equality_LinearArith | SMTInterpol | 1.087421 |
| Equality_MachineArith | z3-BooledASS-base | 1.058691 |
| QF_Datatypes | Z3-Z3++ | 1.043598 |
| QF_Datatypes | cvc5 | 1.031211 |
| QF_Datatypes | Z3-alpha2 | 0.970386 |
| QF_FPArith | bitwuzla-dandelion | 0.966221 |
| QF_Datatypes | Z3-alpha2-debug | 0.952499 |
| QF_LinearIntArith | NeuroSym | 0.866634 |
| QF_NonLinearIntArith | z3-BooledASS | 0.839358 |
| QF_Datatypes | Z3-alpha2-base | 0.793578 |
| QF_Datatypes | z3-BooledASS | 0.793578 |
| QF_Datatypes | z3-BooledASS-base | 0.788171 |
| QF_LinearRealArith | Samet | 0.786488 |
| QF_NonLinearIntArith | Xolver | 0.754579 |
| QF_NonLinearRealArith | Xolver | 0.75215 |
| FPArith | z3-BooledASS | 0.603046 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.599611 |
| QF_Bitvec | SMTInterpol | 0.535165 |
| FPArith | Bitwuzla-fixed | 0.486805 |
| Equality | cvc5 | 0.485124 |
| Equality | cvc5-cvc5-xyz-base | 0.485124 |
| Equality | cvc5-cvc5-xyz | 0.485124 |
| QF_Datatypes | Z3-Z3++-base | 0.439306 |
| FPArith | bitwuzla-dandelion | 0.426519 |
| Equality_NonLinearArith | SMTInterpol | 0.330577 |
| Arith | Amaya | 0.327495 |
| QF_Datatypes | SMTInterpol | 0.319802 |
| Equality_MachineArith | SMTInterpol | 0.290747 |
| Bitvec | UltimateEliminator+MathSAT | 0.269011 |
| QF_Bitvec | Roole | 0.241883 |
| Equality_MachineArith | Bitwuzla-fixed | 0.204087 |
| Equality_MachineArith | Bitwuzla | 0.203751 |
| Bitvec | SMTInterpol | 0.202551 |
| QF_Equality_NonLinearArith | Xolver | 0.177786 |
| QF_Bitvec | z3-BooledASS | 0.170865 |
| FPArith | colibri2 | 0.160145 |
| Arith | SMTInterpol | 0.100485 |
| Equality_MachineArith | z3-BooledASS | 0.092885 |
| QF_NonLinearRealArith | SMTInterpol | 0.088561 |
| Equality | z3-BooledASS | 0.080499 |
| Equality | z3-BooledASS-base | 0.079895 |
| Equality_MachineArith | bitwuzla-dandelion-base | 0.064787 |
| FPArith | UltimateEliminator+MathSAT | 0.060985 |
| Equality_MachineArith | bitwuzla-dandelion | 0.048368 |
| Arith | SMT-RAT | 0.018131 |
| Equality | Yices2 | 0.015309 |
| Equality | SMTInterpol | 0.009215 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.007497 |
| QF_FPArith | z3-BooledASS | 0.004086 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.003284 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.001033 |
| QF_NonLinearIntArith | SMTInterpol | 0.000224 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.338173 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq | -6.545539 |
| QF_Bitvec | Yices2 | -6.809667 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler | 3.478712 |
| QF_Bitvec | Bitwuzla-MachBV | 3.285259 |
| QF_Bitvec | bitwuzla-dandelion-base | 3.243258 |
| QF_Bitvec | Bitwuzla-MachBV-base | 3.240642 |
| QF_Bitvec | Bitwuzla-SPFD-base | 3.240642 |
| QF_Bitvec | Bitwuzla | 3.2328 |
| QF_Bitvec | bitwuzla-dandelion | 3.224968 |
| QF_Strings | OSTRICH | 3.219863 |
| QF_Bitvec | Bitwuzla-SPFD | 3.185949 |
| QF_Equality | OpenSMT-SMTS-seq | 3.147367 |
| QF_Equality | z3-BooledASS-base | 3.147367 |
| QF_Equality | z3-BooledASS | 3.147367 |
| QF_Equality | cvc5 | 3.147367 |
| QF_Equality | OpenSMT-SMTS-seq-base | 3.147367 |
| QF_Equality | OpenSMT | 3.147367 |
| QF_Equality | cvc5-cvc5-xyz | 3.147367 |
| QF_Equality | cvc5-cvc5-xyz-base | 3.147367 |
| QF_Equality | Yices2 | 3.147367 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 3.084196 |
| QF_Equality_Bitvec | Bitwuzla | 3.066851 |
| QF_Equality_Bitvec | bitwuzla-dandelion-base | 3.064378 |
| QF_Bitvec | bv_decide-nokernel | 3.049983 |
| QF_Bitvec | bv_decide | 3.042375 |
| QF_Equality | SMTInterpol | 3.031877 |
| QF_FPArith | Bitwuzla | 3.016382 |
| QF_FPArith | bitwuzla-dandelion-base | 3.008009 |
| QF_Bitvec | cvc5 | 2.976841 |
| QF_Bitvec | cvc5-cvc5-xyz | 2.976841 |
| QF_Bitvec | cvc5-cvc5-xyz-base | 2.974335 |
| QF_Equality_LinearArith | z3-BooledASS-base | 2.936114 |
| QF_Equality_LinearArith | z3-BooledASS | 2.936114 |
| QF_Bitvec | NeuroSym | 2.934378 |
| QF_Equality_Bitvec | Yices2 | 2.929858 |
| FPArith | Bitwuzla | 2.886303 |
| QF_FPArith | cvc5-cvc5-xyz | 2.879715 |
| QF_FPArith | cvc5 | 2.879715 |
| QF_FPArith | cvc5-cvc5-xyz-base | 2.875623 |
| QF_Equality_LinearArith | SMTInterpol | 2.844213 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz-base | 2.812556 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz | 2.810187 |
| QF_Equality_Bitvec | cvc5 | 2.805452 |
| QF_Equality_LinearArith | cvc5 | 2.805274 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz-base | 2.802041 |
| QF_LinearIntArith | QiuQi | 2.785036 |
| QF_Equality_LinearArith | OpenSMT | 2.782683 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq-base | 2.782683 |
| QF_Bitvec | Z3-GEX | 2.777252 |
| QF_Equality_Bitvec | z3-BooledASS-base | 2.727902 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz | 2.699575 |
| QF_Equality_LinearArith | Yices2 | 2.699575 |
| FPArith | cvc5 | 2.682776 |
| FPArith | cvc5-cvc5-xyz-base | 2.677905 |
| FPArith | cvc5-cvc5-xyz | 2.677905 |
| QF_NonLinearRealArith | Z3-GEX | 2.626334 |
| QF_NonLinearRealArith | Z3-alpha2-debug | 2.587894 |
| QF_NonLinearRealArith | Z3-alpha2 | 2.587894 |
| QF_NonLinearRealArith | Z3-GEX-base | 2.582425 |
| QF_NonLinearRealArith | Z3-siri-base | 2.576963 |
| QF_NonLinearRealArith | Z3-siri | 2.571506 |
| QF_LinearIntArith | OpenSMT-SMTS-seq | 2.523314 |
| QF_LinearIntArith | OpenSMT-SMTS-seq-base | 2.50574 |
| QF_LinearIntArith | OpenSMT | 2.494059 |
| QF_LinearIntArith | cvc5 | 2.467874 |
| QF_LinearIntArith | Yices2 | 2.467874 |
| QF_LinearIntArith | Z3-GEX | 2.462075 |
| QF_NonLinearIntArith | Z3-Z3++ | 2.455019 |
| QF_NonLinearIntArith | Z3-alpha2 | 2.455019 |
| QF_NonLinearIntArith | Z3-alpha2-debug | 2.448906 |
| Arith | Z3-alpha2-debug | 2.428356 |
| Arith | Z3-alpha2 | 2.428356 |
| QF_NonLinearRealArith | Z3-alpha2-base | 2.426359 |
| QF_NonLinearRealArith | cvc5 | 2.410492 |
| QF_LinearRealArith | OpenSMT | 2.40862 |
| QF_LinearRealArith | Yices2 | 2.40862 |
| QF_LinearIntArith | Z3-alpha2-debug | 2.407315 |
| QF_LinearIntArith | Z3-alpha2 | 2.407315 |
| QF_LinearRealArith | OpenSMT-SMTS-seq-base | 2.401743 |
| Arith | Z3-GEX | 2.397852 |
| QF_Bitvec | Z3-alpha2 | 2.396599 |
| QF_LinearRealArith | OpenSMT-SMTS-seq | 2.394876 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz-base | 2.394677 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz | 2.394677 |
| QF_Bitvec | Z3-alpha2-debug | 2.39435 |
| QF_NonLinearRealArith | Yices2 | 2.389417 |
| QF_FPArith | z3-BooledASS-base | 2.379592 |
| QF_NonLinearIntArith | Z3-GEX | 2.356122 |
| Bitvec | Bitwuzla-fixed | 2.353264 |
| QF_LinearRealArith | cvc5 | 2.347082 |
| QF_NonLinearRealArith | z3-BooledASS | 2.342336 |
| QF_NonLinearRealArith | z3-BooledASS-base | 2.337133 |
| Bitvec | Bitwuzla | 2.336455 |
| Arith | z3-BooledASS | 2.328853 |
| Arith | z3-BooledASS-base | 2.328853 |
| FPArith | z3-BooledASS-base | 2.32065 |
| Arith | Z3-GEX-base | 2.320298 |
| QF_LinearRealArith | Z3-GEX | 2.319987 |
| Arith | Z3-alpha2-base | 2.31176 |
| Bitvec | cvc5-cvc5-xyz | 2.294696 |
| Bitvec | cvc5-cvc5-xyz-base | 2.294696 |
| Bitvec | cvc5 | 2.294696 |
| QF_Bitvec | z3-BooledASS-base | 2.294249 |
| QF_Bitvec | Z3-GEX-base | 2.292049 |
| QF_Bitvec | Z3-alpha2-base | 2.28985 |
| QF_LinearRealArith | z3-BooledASS | 2.286341 |
| QF_LinearRealArith | z3-BooledASS-base | 2.286341 |
| QF_LinearRealArith | Z3-GEX-base | 2.286341 |
| QF_LinearIntArith | z3-BooledASS-base | 2.280079 |
| QF_LinearIntArith | Z3-alpha2-base | 2.274505 |
| Equality_LinearArith | cvc5-cvc5-xyz | 2.26983 |
| Equality_LinearArith | cvc5 | 2.268004 |
| QF_LinearRealArith | cvc5-cvc5-xyz-base | 2.26627 |
| Equality_LinearArith | cvc5-cvc5-xyz-base | 2.266178 |
| QF_LinearIntArith | Z3-GEX-base | 2.263375 |
| QF_LinearRealArith | cvc5-cvc5-xyz | 2.252939 |
| QF_NonLinearIntArith | z3-BooledASS-base | 2.187464 |
| QF_NonLinearIntArith | Z3-siri-base | 2.181693 |
| QF_NonLinearIntArith | Z3-GEX-base | 2.174011 |
| QF_LinearIntArith | cvc5-cvc5-xyz-base | 2.16988 |
| QF_LinearIntArith | cvc5-cvc5-xyz | 2.16716 |
| Equality_LinearArith | z3-BooledASS-base | 2.118971 |
| QF_LinearIntArith | z3-BooledASS | 2.094365 |
| QF_NonLinearRealArith | SMT-RAT | 2.084393 |
| Bitvec | YicesQS | 2.08362 |
| QF_NonLinearIntArith | Z3-Z3++-base | 2.069757 |
| QF_NonLinearIntArith | Z3-alpha2-base | 2.034338 |
| Equality_LinearArith | z3-BooledASS | 2.029044 |
| Arith | YicesQS | 2.026825 |
| Arith | cvc5-cvc5-xyz-base | 1.971298 |
| Arith | cvc5-cvc5-xyz | 1.971298 |
| Arith | cvc5 | 1.963429 |
| QF_NonLinearIntArith | Yices2 | 1.948034 |
| QF_Equality | plat-smt | 1.938994 |
| QF_LinearIntArith | SMTInterpol | 1.911428 |
| FPArith | bitwuzla-dandelion-base | 1.885442 |
| QF_Strings | cvc5 | 1.871245 |
| QF_Strings | cvc5-cvc5-xyz-base | 1.866304 |
| QF_Strings | cvc5-cvc5-xyz | 1.862779 |
| Bitvec | bitwuzla-dandelion-base | 1.771457 |
| QF_Strings | Z3-GEX | 1.764747 |
| QF_LinearRealArith | SMTInterpol | 1.757821 |
| QF_FPArith | colibri2 | 1.744173 |
| QF_Equality_Bitvec | NeuroSym | 1.741379 |
| QF_Strings | Z3-GEX-base | 1.733338 |
| QF_NonLinearIntArith | cvc5 | 1.695259 |
| QF_Equality_NonLinearArith | Z3-alpha2-debug | 1.681596 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1.681596 |
| QF_Equality_Bitvec | SMTInterpol | 1.678566 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz | 1.674987 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz-base | 1.659863 |
| QF_Strings | z3-BooledASS | 1.650738 |
| QF_Strings | z3-BooledASS-base | 1.650738 |
| Bitvec | bitwuzla-dandelion | 1.642407 |
| QF_Strings | Z3-Noodler-base | 1.634856 |
| Equality_NonLinearArith | cvc5 | 1.619755 |
| Equality_NonLinearArith | cvc5-cvc5-xyz | 1.618589 |
| Equality_NonLinearArith | cvc5-cvc5-xyz-base | 1.618589 |
| QF_NonLinearIntArith | Z3-siri | 1.611597 |
| QF_Equality_NonLinearArith | Z3-alpha2-base | 1.586686 |
| QF_Equality_NonLinearArith | Yices2 | 1.573353 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 1.566707 |
| QF_Equality_NonLinearArith | z3-BooledASS | 1.553458 |
| Bitvec | z3-BooledASS-base | 1.538594 |
| Bitvec | z3-BooledASS | 1.538594 |
| Equality_NonLinearArith | z3-BooledASS-base | 1.505241 |
| Equality_NonLinearArith | z3-BooledASS | 1.499625 |
| QF_Datatypes | cvc5-cvc5-xyz | 1.464269 |
| Equality_MachineArith | cvc5-cvc5-xyz | 1.384531 |
| Equality_MachineArith | cvc5 | 1.38103 |
| Equality_MachineArith | cvc5-cvc5-xyz-base | 1.370554 |
| QF_Equality_Bitvec | z3-BooledASS | 1.35207 |
| Arith | UltimateEliminator+MathSAT | 1.290786 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz | 1.252359 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz-base | 1.24643 |
| QF_Equality_NonLinearArith | cvc5 | 1.240516 |
| Equality_LinearArith | SMTInterpol | 1.091217 |
| QF_Datatypes | cvc5-cvc5-xyz-base | 1.087534 |
| Equality_MachineArith | z3-BooledASS-base | 1.058691 |
| QF_Datatypes | Z3-Z3++ | 1.043598 |
| QF_Datatypes | cvc5 | 1.031211 |
| QF_Datatypes | Z3-alpha2 | 0.970386 |
| QF_FPArith | bitwuzla-dandelion | 0.966221 |
| QF_Datatypes | Z3-alpha2-debug | 0.952499 |
| QF_LinearIntArith | NeuroSym | 0.866634 |
| QF_NonLinearIntArith | z3-BooledASS | 0.839358 |
| QF_Datatypes | Z3-alpha2-base | 0.793578 |
| QF_Datatypes | z3-BooledASS | 0.793578 |
| QF_Datatypes | z3-BooledASS-base | 0.788171 |
| QF_LinearRealArith | Samet | 0.786488 |
| QF_NonLinearIntArith | Xolver | 0.754579 |
| QF_NonLinearRealArith | Xolver | 0.75215 |
| FPArith | z3-BooledASS | 0.603046 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.599611 |
| QF_Bitvec | SMTInterpol | 0.537293 |
| FPArith | Bitwuzla-fixed | 0.486805 |
| Equality | cvc5 | 0.485124 |
| Equality | cvc5-cvc5-xyz-base | 0.485124 |
| Equality | cvc5-cvc5-xyz | 0.485124 |
| QF_Datatypes | Z3-Z3++-base | 0.439306 |
| FPArith | bitwuzla-dandelion | 0.426519 |
| QF_Datatypes | SMTInterpol | 0.337226 |
| Equality_NonLinearArith | SMTInterpol | 0.330577 |
| Arith | Amaya | 0.327495 |
| Equality_MachineArith | SMTInterpol | 0.290747 |
| Bitvec | UltimateEliminator+MathSAT | 0.269011 |
| QF_Bitvec | Roole | 0.241883 |
| Equality_MachineArith | Bitwuzla-fixed | 0.204087 |
| Equality_MachineArith | Bitwuzla | 0.203751 |
| Bitvec | SMTInterpol | 0.202551 |
| QF_Equality_NonLinearArith | Xolver | 0.177786 |
| QF_Bitvec | z3-BooledASS | 0.170865 |
| FPArith | colibri2 | 0.160145 |
| Arith | SMTInterpol | 0.100485 |
| Equality_MachineArith | z3-BooledASS | 0.092885 |
| QF_NonLinearRealArith | SMTInterpol | 0.088561 |
| Equality | z3-BooledASS | 0.080499 |
| Equality | z3-BooledASS-base | 0.079895 |
| Equality_MachineArith | bitwuzla-dandelion-base | 0.064787 |
| FPArith | UltimateEliminator+MathSAT | 0.060985 |
| Equality_MachineArith | bitwuzla-dandelion | 0.048368 |
| Arith | SMT-RAT | 0.018131 |
| Equality | Yices2 | 0.015309 |
| Equality | SMTInterpol | 0.009421 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.007497 |
| QF_FPArith | z3-BooledASS | 0.004086 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.003284 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.001033 |
| QF_NonLinearIntArith | SMTInterpol | 0.000224 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.338173 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq | -6.545539 |
| QF_Bitvec | Yices2 | -6.809667 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Equality_Bitvec | bitwuzla-dandelion | 1.222273 |
| QF_Equality_Bitvec | Bitwuzla | 1.222273 |
| QF_Equality_Bitvec | bitwuzla-dandelion-base | 1.219151 |
| QF_Equality_Bitvec | Yices2 | 1.203601 |
| QF_Equality_Bitvec | z3-BooledASS-base | 1.157549 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz-base | 1.148447 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz | 1.146933 |
| QF_Equality_Bitvec | cvc5 | 1.143909 |
| QF_NonLinearIntArith | Z3-Z3++ | 1.124908 |
| QF_LinearIntArith | QiuQi | 1.104585 |
| QF_Strings | Z3-Noodler | 1.068926 |
| QF_NonLinearIntArith | Z3-alpha2-debug | 1.052944 |
| QF_NonLinearIntArith | Z3-alpha2 | 1.052944 |
| QF_NonLinearIntArith | Z3-GEX | 1.038306 |
| QF_Equality_NonLinearArith | Yices2 | 1.03697 |
| QF_LinearIntArith | Z3-GEX | 1.024556 |
| QF_LinearIntArith | OpenSMT-SMTS-seq | 1.005945 |
| QF_LinearIntArith | OpenSMT-SMTS-seq-base | 0.99486 |
| QF_LinearIntArith | OpenSMT | 0.987504 |
| QF_Strings | OSTRICH | 0.981641 |
| QF_NonLinearIntArith | Z3-Z3++-base | 0.980779 |
| QF_LinearIntArith | Z3-alpha2-debug | 0.969234 |
| QF_LinearIntArith | Z3-alpha2 | 0.969234 |
| QF_LinearIntArith | Yices2 | 0.963787 |
| QF_LinearIntArith | cvc5 | 0.945739 |
| QF_Equality_NonLinearArith | Z3-alpha2-debug | 0.931766 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 0.931766 |
| QF_Equality_LinearArith | SMTInterpol | 0.922619 |
| QF_LinearIntArith | Z3-GEX-base | 0.920758 |
| QF_LinearIntArith | z3-BooledASS-base | 0.918987 |
| QF_NonLinearIntArith | Z3-siri-base | 0.917398 |
| QF_LinearIntArith | Z3-alpha2-base | 0.915449 |
| QF_NonLinearIntArith | Yices2 | 0.913662 |
| QF_NonLinearIntArith | Z3-GEX-base | 0.911176 |
| QF_NonLinearIntArith | z3-BooledASS-base | 0.909934 |
| QF_Equality_LinearArith | z3-BooledASS-base | 0.88772 |
| QF_Equality_LinearArith | z3-BooledASS | 0.88772 |
| QF_Equality_NonLinearArith | Z3-alpha2-base | 0.876301 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz-base | 0.871423 |
| QF_Equality_LinearArith | cvc5 | 0.871423 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz | 0.869622 |
| QF_Equality_Bitvec | NeuroSym | 0.869536 |
| QF_LinearIntArith | cvc5-cvc5-xyz-base | 0.866634 |
| QF_LinearIntArith | cvc5-cvc5-xyz | 0.864915 |
| QF_LinearIntArith | z3-BooledASS | 0.859769 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 0.856554 |
| QF_Equality_NonLinearArith | z3-BooledASS | 0.851652 |
| QF_NonLinearIntArith | Z3-alpha2-base | 0.846527 |
| QF_NonLinearIntArith | cvc5 | 0.829847 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz | 0.82393 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq | 0.82344 |
| QF_Equality_LinearArith | OpenSMT | 0.821689 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq-base | 0.821689 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz-base | 0.81216 |
| QF_Bitvec | Bitwuzla-MachBV | 0.791955 |
| QF_Equality_LinearArith | Yices2 | 0.787059 |
| QF_Bitvec | bitwuzla-dandelion | 0.786792 |
| QF_Bitvec | Bitwuzla-MachBV-base | 0.785504 |
| QF_Bitvec | Bitwuzla-SPFD-base | 0.785504 |
| QF_Bitvec | bitwuzla-dandelion-base | 0.785504 |
| QF_Bitvec | Bitwuzla | 0.776515 |
| QF_Bitvec | Bitwuzla-SPFD | 0.773957 |
| QF_Strings | cvc5 | 0.771732 |
| QF_Strings | cvc5-cvc5-xyz-base | 0.768561 |
| QF_Strings | cvc5-cvc5-xyz | 0.761786 |
| QF_Bitvec | cvc5 | 0.743584 |
| QF_Bitvec | cvc5-cvc5-xyz | 0.743584 |
| QF_Bitvec | cvc5-cvc5-xyz-base | 0.742331 |
| QF_Bitvec | bv_decide-nokernel | 0.734839 |
| QF_Bitvec | bv_decide | 0.733595 |
| QF_Strings | Z3-GEX | 0.727483 |
| QF_LinearIntArith | SMTInterpol | 0.718786 |
| QF_LinearRealArith | OpenSMT-SMTS-seq | 0.713546 |
| QF_LinearRealArith | OpenSMT-SMTS-seq-base | 0.713546 |
| QF_LinearRealArith | OpenSMT | 0.713546 |
| QF_Bitvec | NeuroSym | 0.712592 |
| QF_Strings | Z3-GEX-base | 0.711716 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz | 0.711145 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz-base | 0.711145 |
| QF_Equality_NonLinearArith | cvc5 | 0.706679 |
| QF_LinearRealArith | Yices2 | 0.694941 |
| QF_NonLinearIntArith | Xolver | 0.691518 |
| QF_Bitvec | Z3-alpha2 | 0.671501 |
| QF_Bitvec | Z3-alpha2-debug | 0.670311 |
| QF_LinearRealArith | Z3-GEX | 0.669306 |
| QF_NonLinearRealArith | Z3-GEX | 0.663491 |
| QF_LinearRealArith | cvc5 | 0.662071 |
| QF_Bitvec | Z3-GEX | 0.660828 |
| QF_Strings | z3-BooledASS | 0.659569 |
| QF_Strings | z3-BooledASS-base | 0.659569 |
| QF_LinearRealArith | z3-BooledASS | 0.651291 |
| QF_LinearRealArith | z3-BooledASS-base | 0.651291 |
| QF_LinearRealArith | Z3-GEX-base | 0.651291 |
| QF_Strings | Z3-Noodler-base | 0.649544 |
| QF_NonLinearRealArith | Z3-alpha2-debug | 0.646973 |
| QF_NonLinearRealArith | Z3-alpha2 | 0.646973 |
| QF_NonLinearIntArith | Z3-siri | 0.644722 |
| QF_NonLinearRealArith | Z3-siri-base | 0.644241 |
| QF_NonLinearRealArith | Z3-GEX-base | 0.644241 |
| QF_LinearRealArith | cvc5-cvc5-xyz-base | 0.644153 |
| QF_NonLinearRealArith | Z3-siri | 0.641514 |
| QF_Bitvec | z3-BooledASS-base | 0.639739 |
| QF_Bitvec | Z3-GEX-base | 0.639739 |
| QF_NonLinearRealArith | z3-BooledASS | 0.638793 |
| QF_Bitvec | Z3-alpha2-base | 0.638578 |
| FPArith | Bitwuzla | 0.638202 |
| QF_LinearRealArith | cvc5-cvc5-xyz | 0.637055 |
| QF_NonLinearRealArith | z3-BooledASS-base | 0.636077 |
| QF_NonLinearRealArith | Z3-alpha2-base | 0.614562 |
| QF_NonLinearRealArith | Yices2 | 0.601304 |
| QF_Equality | SMTInterpol | 0.592172 |
| QF_Equality | OpenSMT-SMTS-seq | 0.592172 |
| QF_Equality | cvc5 | 0.592172 |
| QF_Equality | cvc5-cvc5-xyz-base | 0.592172 |
| QF_Equality | cvc5-cvc5-xyz | 0.592172 |
| QF_Equality | OpenSMT-SMTS-seq-base | 0.592172 |
| QF_Equality | OpenSMT | 0.592172 |
| QF_Equality | z3-BooledASS-base | 0.592172 |
| QF_Equality | z3-BooledASS | 0.592172 |
| QF_Equality | Yices2 | 0.592172 |
| FPArith | bitwuzla-dandelion-base | 0.589263 |
| QF_LinearRealArith | SMTInterpol | 0.58847 |
| QF_Equality_Bitvec | SMTInterpol | 0.575636 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz-base | 0.562395 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz | 0.562395 |
| QF_NonLinearRealArith | cvc5 | 0.562395 |
| FPArith | cvc5 | 0.553286 |
| FPArith | cvc5-cvc5-xyz-base | 0.551075 |
| FPArith | cvc5-cvc5-xyz | 0.551075 |
| QF_NonLinearRealArith | SMT-RAT | 0.514978 |
| QF_Equality_Bitvec | z3-BooledASS | 0.484186 |
| QF_FPArith | bitwuzla-dandelion-base | 0.482621 |
| QF_FPArith | Bitwuzla | 0.482621 |
| FPArith | z3-BooledASS-base | 0.476481 |
| QF_FPArith | cvc5 | 0.475941 |
| QF_FPArith | cvc5-cvc5-xyz | 0.475941 |
| QF_FPArith | cvc5-cvc5-xyz-base | 0.474279 |
| FPArith | Bitwuzla-fixed | 0.413026 |
| QF_NonLinearIntArith | z3-BooledASS | 0.396728 |
| QF_FPArith | z3-BooledASS-base | 0.375395 |
| Arith | Z3-alpha2-debug | 0.365459 |
| Arith | Z3-alpha2 | 0.365459 |
| Arith | YicesQS | 0.358707 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.352858 |
| QF_LinearIntArith | NeuroSym | 0.349361 |
| Arith | Z3-GEX | 0.348697 |
| QF_Equality | plat-smt | 0.348215 |
| Arith | z3-BooledASS | 0.342103 |
| Arith | z3-BooledASS-base | 0.342103 |
| Arith | Z3-GEX-base | 0.335571 |
| Arith | Z3-alpha2-base | 0.333948 |
| QF_LinearRealArith | Samet | 0.314639 |
| QF_FPArith | colibri2 | 0.288059 |
| Arith | cvc5 | 0.273717 |
| Arith | cvc5-cvc5-xyz | 0.273717 |
| Arith | cvc5-cvc5-xyz-base | 0.273717 |
| QF_FPArith | bitwuzla-dandelion | 0.254164 |
| Arith | UltimateEliminator+MathSAT | 0.175884 |
| Bitvec | bitwuzla-dandelion-base | 0.164957 |
| QF_NonLinearRealArith | Xolver | 0.163802 |
| Bitvec | Bitwuzla-fixed | 0.162735 |
| Bitvec | Bitwuzla | 0.162735 |
| QF_Datatypes | cvc5 | 0.151452 |
| QF_Datatypes | cvc5-cvc5-xyz-base | 0.151452 |
| QF_Datatypes | cvc5-cvc5-xyz | 0.151452 |
| Bitvec | YicesQS | 0.149722 |
| Bitvec | bitwuzla-dandelion | 0.137251 |
| Bitvec | cvc5-cvc5-xyz | 0.135225 |
| Bitvec | cvc5-cvc5-xyz-base | 0.135225 |
| Bitvec | cvc5 | 0.135225 |
| QF_Equality_NonLinearArith | Xolver | 0.131991 |
| Bitvec | z3-BooledASS | 0.11209 |
| Bitvec | z3-BooledASS-base | 0.11026 |
| Equality_MachineArith | Bitwuzla-fixed | 0.088404 |
| Equality_MachineArith | Bitwuzla | 0.088404 |
| Arith | Amaya | 0.056857 |
| Equality_MachineArith | cvc5-cvc5-xyz | 0.055311 |
| Equality_MachineArith | cvc5 | 0.054787 |
| Equality_MachineArith | cvc5-cvc5-xyz-base | 0.054613 |
| Equality_MachineArith | z3-BooledASS-base | 0.039192 |
| Equality | cvc5 | 0.038938 |
| Equality | cvc5-cvc5-xyz-base | 0.038938 |
| Equality | cvc5-cvc5-xyz | 0.038938 |
| QF_Bitvec | Roole | 0.031163 |
| FPArith | colibri2 | 0.02978 |
| QF_Datatypes | Z3-Z3++ | 0.028989 |
| QF_Datatypes | Z3-alpha2 | 0.022195 |
| Equality_LinearArith | z3-BooledASS-base | 0.022154 |
| QF_Datatypes | Z3-alpha2-debug | 0.021298 |
| QF_Datatypes | SMTInterpol | 0.017092 |
| FPArith | UltimateEliminator+MathSAT | 0.015616 |
| Equality_LinearArith | z3-BooledASS | 0.015447 |
| Equality_MachineArith | bitwuzla-dandelion-base | 0.013566 |
| QF_Bitvec | SMTInterpol | 0.01351 |
| Equality_NonLinearArith | z3-BooledASS-base | 0.01219 |
| Equality_LinearArith | cvc5-cvc5-xyz-base | 0.012175 |
| Equality_LinearArith | cvc5 | 0.012175 |
| Equality_LinearArith | cvc5-cvc5-xyz | 0.012175 |
| Equality_NonLinearArith | z3-BooledASS | 0.012089 |
| Equality_MachineArith | z3-BooledASS | 0.010779 |
| FPArith | bitwuzla-dandelion | 0.010537 |
| Equality_MachineArith | bitwuzla-dandelion | 0.008934 |
| Equality_NonLinearArith | cvc5-cvc5-xyz-base | 0.007981 |
| Equality_NonLinearArith | cvc5-cvc5-xyz | 0.007981 |
| Equality_NonLinearArith | cvc5 | 0.007981 |
| QF_Datatypes | Z3-Z3++-base | 0.006739 |
| QF_Datatypes | Z3-alpha2-base | 0.004474 |
| QF_Datatypes | z3-BooledASS-base | 0.004077 |
| QF_Datatypes | z3-BooledASS | 0.004077 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.003825 |
| Equality_LinearArith | SMTInterpol | 0.003388 |
| Bitvec | UltimateEliminator+MathSAT | 0.002176 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.001896 |
| Equality | z3-BooledASS-base | 0.000957 |
| Equality | z3-BooledASS | 0.000957 |
| Arith | SMTInterpol | 0.000787 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000388 |
| Equality | Yices2 | 0.000192 |
| Equality_NonLinearArith | SMTInterpol | 9.3e-05 |
| QF_NonLinearRealArith | SMTInterpol | 4.6e-05 |
| Equality_MachineArith | SMTInterpol | 4.5e-05 |
| Arith | SMT-RAT | 3.1e-05 |
| Equality | SMTInterpol | 1.8e-05 |
| FPArith | z3-BooledASS | 9e-06 |
| Bitvec | SMTInterpol | 8e-06 |
| QF_NonLinearIntArith | SMTInterpol | 4e-06 |
| QF_FPArith | z3-BooledASS | 1e-06 |
| QF_Bitvec | z3-BooledASS | 1e-06 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.338173 |
| QF_Bitvec | Yices2 | -6.809667 |
| Division | Solver | Contribution |
|---|---|---|
| Equality_LinearArith | cvc5-cvc5-xyz | 1.949524 |
| Equality_LinearArith | cvc5 | 1.947831 |
| Equality_LinearArith | cvc5-cvc5-xyz-base | 1.946139 |
| Equality_LinearArith | z3-BooledASS-base | 1.707799 |
| Equality_LinearArith | z3-BooledASS | 1.690413 |
| Equality_NonLinearArith | cvc5 | 1.40034 |
| Equality_NonLinearArith | cvc5-cvc5-xyz | 1.399256 |
| Equality_NonLinearArith | cvc5-cvc5-xyz-base | 1.399256 |
| Bitvec | cvc5-cvc5-xyz-base | 1.315829 |
| Bitvec | cvc5-cvc5-xyz | 1.315829 |
| Bitvec | cvc5 | 1.315829 |
| Bitvec | Bitwuzla-fixed | 1.278326 |
| Bitvec | Bitwuzla | 1.265945 |
| Equality_NonLinearArith | z3-BooledASS-base | 1.24651 |
| Equality_NonLinearArith | z3-BooledASS | 1.242422 |
| Bitvec | YicesQS | 1.116268 |
| QF_FPArith | Bitwuzla | 1.085898 |
| QF_FPArith | bitwuzla-dandelion-base | 1.080876 |
| QF_FPArith | cvc5-cvc5-xyz-base | 1.014225 |
| QF_FPArith | cvc5-cvc5-xyz | 1.014225 |
| QF_FPArith | cvc5 | 1.014225 |
| QF_Equality | OpenSMT-SMTS-seq | 1.009131 |
| QF_Equality | z3-BooledASS-base | 1.009131 |
| QF_Equality | z3-BooledASS | 1.009131 |
| QF_Equality | cvc5 | 1.009131 |
| QF_Equality | OpenSMT-SMTS-seq-base | 1.009131 |
| QF_Equality | OpenSMT | 1.009131 |
| QF_Equality | cvc5-cvc5-xyz | 1.009131 |
| QF_Equality | cvc5-cvc5-xyz-base | 1.009131 |
| QF_Equality | Yices2 | 1.009131 |
| Equality_LinearArith | SMTInterpol | 0.973006 |
| QF_Equality | SMTInterpol | 0.944204 |
| Arith | Z3-GEX | 0.917753 |
| Arith | Z3-alpha2-debug | 0.909708 |
| Arith | Z3-alpha2 | 0.909708 |
| Arith | Z3-GEX-base | 0.891075 |
| Arith | Z3-alpha2-base | 0.888429 |
| Equality_MachineArith | cvc5-cvc5-xyz | 0.88638 |
| Arith | z3-BooledASS | 0.885787 |
| Arith | z3-BooledASS-base | 0.885787 |
| Equality_MachineArith | cvc5 | 0.885679 |
| Equality_MachineArith | cvc5-cvc5-xyz-base | 0.877991 |
| QF_FPArith | z3-BooledASS-base | 0.864709 |
| Bitvec | bitwuzla-dandelion-base | 0.855277 |
| QF_Bitvec | Bitwuzla-MachBV | 0.851208 |
| QF_Bitvec | Bitwuzla | 0.840518 |
| QF_Bitvec | bitwuzla-dandelion-base | 0.836527 |
| QF_Bitvec | Bitwuzla-SPFD-base | 0.835199 |
| QF_Bitvec | Bitwuzla-MachBV-base | 0.835199 |
| Bitvec | bitwuzla-dandelion | 0.830086 |
| QF_Bitvec | Yices2 | 0.829896 |
| QF_Bitvec | bitwuzla-dandelion | 0.82593 |
| Bitvec | z3-BooledASS-base | 0.825093 |
| Bitvec | z3-BooledASS | 0.820115 |
| QF_Bitvec | Bitwuzla-SPFD | 0.819341 |
| FPArith | Bitwuzla | 0.810066 |
| FPArith | cvc5-cvc5-xyz-base | 0.79939 |
| FPArith | cvc5-cvc5-xyz | 0.79939 |
| FPArith | cvc5 | 0.79939 |
| QF_Bitvec | bv_decide-nokernel | 0.790663 |
| QF_Bitvec | bv_decide | 0.788081 |
| Arith | cvc5-cvc5-xyz-base | 0.775896 |
| Arith | cvc5-cvc5-xyz | 0.775896 |
| Arith | cvc5 | 0.770962 |
| QF_FPArith | COLIBRI | 0.756192 |
| QF_Bitvec | NeuroSym | 0.754902 |
| QF_Bitvec | cvc5-cvc5-xyz-base | 0.744837 |
| QF_Bitvec | cvc5 | 0.744837 |
| QF_Bitvec | cvc5-cvc5-xyz | 0.744837 |
| QF_Bitvec | Z3-GEX | 0.728625 |
| QF_Datatypes | Z3-Z3++ | 0.724721 |
| QF_Datatypes | Z3-alpha2 | 0.699069 |
| FPArith | z3-BooledASS-base | 0.694042 |
| QF_Strings | Z3-Noodler | 0.690963 |
| Equality_MachineArith | z3-BooledASS-base | 0.690488 |
| QF_Datatypes | Z3-alpha2-debug | 0.688938 |
| QF_Datatypes | z3-BooledASS | 0.6839 |
| Arith | YicesQS | 0.680203 |
| QF_Datatypes | z3-BooledASS-base | 0.67888 |
| QF_Datatypes | Z3-alpha2-base | 0.67888 |
| QF_Datatypes | cvc5-cvc5-xyz | 0.673879 |
| QF_NonLinearRealArith | Z3-GEX | 0.649712 |
| QF_NonLinearRealArith | Z3-GEX-base | 0.646973 |
| QF_NonLinearRealArith | Z3-alpha2-debug | 0.646973 |
| QF_NonLinearRealArith | Z3-alpha2 | 0.646973 |
| QF_Strings | OSTRICH | 0.645804 |
| QF_NonLinearRealArith | cvc5 | 0.644241 |
| QF_NonLinearRealArith | Z3-siri | 0.644241 |
| QF_NonLinearRealArith | Z3-siri-base | 0.644241 |
| QF_Equality | plat-smt | 0.643814 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz | 0.636077 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz-base | 0.636077 |
| QF_FPArith | colibri2 | 0.614594 |
| QF_NonLinearRealArith | Z3-alpha2-base | 0.598669 |
| FPArith | z3-BooledASS | 0.598434 |
| QF_Equality_LinearArith | z3-BooledASS-base | 0.594935 |
| QF_Equality_LinearArith | z3-BooledASS | 0.594935 |
| QF_NonLinearRealArith | Yices2 | 0.593418 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq-base | 0.580137 |
| QF_Equality_LinearArith | OpenSMT | 0.580137 |
| QF_Equality_LinearArith | Yices2 | 0.571347 |
| QF_Equality_LinearArith | cvc5 | 0.549666 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz-base | 0.548235 |
| QF_NonLinearRealArith | z3-BooledASS | 0.534689 |
| QF_NonLinearRealArith | z3-BooledASS-base | 0.534689 |
| QF_Bitvec | Z3-alpha2-debug | 0.530922 |
| QF_Bitvec | Z3-alpha2 | 0.530922 |
| QF_NonLinearRealArith | SMT-RAT | 0.527254 |
| QF_Equality_LinearArith | SMTInterpol | 0.527002 |
| QF_LinearRealArith | cvc5 | 0.516015 |
| QF_LinearRealArith | Yices2 | 0.516015 |
| Arith | UltimateEliminator+MathSAT | 0.513719 |
| QF_Bitvec | z3-BooledASS-base | 0.510997 |
| QF_Bitvec | Z3-GEX-base | 0.509959 |
| QF_Bitvec | Z3-alpha2-base | 0.509959 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz | 0.504815 |
| QF_LinearRealArith | OpenSMT | 0.500211 |
| QF_LinearRealArith | Z3-GEX | 0.49708 |
| QF_LinearRealArith | z3-BooledASS | 0.49708 |
| QF_LinearRealArith | z3-BooledASS-base | 0.49708 |
| QF_LinearRealArith | Z3-GEX-base | 0.49708 |
| QF_LinearRealArith | OpenSMT-SMTS-seq-base | 0.49708 |
| QF_LinearRealArith | cvc5-cvc5-xyz-base | 0.493959 |
| QF_LinearRealArith | cvc5-cvc5-xyz | 0.493959 |
| QF_LinearRealArith | OpenSMT-SMTS-seq | 0.493959 |
| QF_Datatypes | cvc5-cvc5-xyz-base | 0.427299 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 0.42331 |
| QF_Equality_Bitvec | bitwuzla-dandelion-base | 0.417813 |
| QF_Equality_Bitvec | Bitwuzla | 0.4169 |
| QF_Datatypes | cvc5 | 0.392274 |
| QF_LinearIntArith | QiuQi | 0.381739 |
| QF_Bitvec | SMTInterpol | 0.380403 |
| QF_Equality_Bitvec | Yices2 | 0.377727 |
| FPArith | bitwuzla-dandelion-base | 0.366605 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz-base | 0.366523 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz | 0.366523 |
| QF_Equality_Bitvec | cvc5 | 0.366523 |
| QF_LinearIntArith | cvc5 | 0.35815 |
| QF_LinearIntArith | Yices2 | 0.347181 |
| QF_LinearIntArith | OpenSMT-SMTS-seq | 0.342841 |
| QF_LinearIntArith | OpenSMT-SMTS-seq-base | 0.342841 |
| QF_LinearIntArith | OpenSMT | 0.342841 |
| QF_Datatypes | Z3-Z3++-base | 0.337226 |
| QF_Equality_Bitvec | z3-BooledASS-base | 0.331478 |
| QF_LinearIntArith | Z3-alpha2-debug | 0.321552 |
| QF_LinearIntArith | Z3-alpha2 | 0.321552 |
| Equality_NonLinearArith | SMTInterpol | 0.319606 |
| QF_LinearRealArith | SMTInterpol | 0.312157 |
| QF_LinearIntArith | Z3-GEX | 0.310134 |
| QF_LinearIntArith | Z3-alpha2-base | 0.303993 |
| QF_LinearIntArith | z3-BooledASS-base | 0.303993 |
| FPArith | bitwuzla-dandelion | 0.302979 |
| QF_LinearIntArith | Z3-GEX-base | 0.296906 |
| QF_LinearIntArith | cvc5-cvc5-xyz | 0.293894 |
| QF_LinearIntArith | cvc5-cvc5-xyz-base | 0.293894 |
| QF_NonLinearIntArith | Z3-alpha2 | 0.292378 |
| QF_NonLinearIntArith | Z3-alpha2-debug | 0.29027 |
| QF_Equality_Bitvec | SMTInterpol | 0.288248 |
| QF_LinearIntArith | SMTInterpol | 0.285938 |
| Equality_MachineArith | SMTInterpol | 0.283569 |
| QF_NonLinearIntArith | z3-BooledASS-base | 0.275733 |
| QF_LinearIntArith | z3-BooledASS | 0.270353 |
| QF_NonLinearIntArith | Z3-GEX-base | 0.270293 |
| QF_NonLinearIntArith | Z3-siri-base | 0.269617 |
| QF_NonLinearIntArith | Z3-GEX | 0.266249 |
| QF_NonLinearIntArith | Z3-Z3++ | 0.256272 |
| QF_NonLinearIntArith | Z3-alpha2-base | 0.256272 |
| Equality | cvc5-cvc5-xyz-base | 0.249183 |
| Equality | cvc5 | 0.249183 |
| Equality | cvc5-cvc5-xyz | 0.249183 |
| QF_Strings | cvc5-cvc5-xyz | 0.242097 |
| QF_Strings | cvc5-cvc5-xyz-base | 0.239563 |
| QF_Strings | cvc5 | 0.239563 |
| QF_FPArith | bitwuzla-dandelion | 0.229267 |
| QF_Strings | Z3-GEX | 0.226111 |
| QF_Strings | Z3-GEX-base | 0.223663 |
| QF_Strings | Z3-Noodler-base | 0.223419 |
| QF_Strings | z3-BooledASS | 0.223419 |
| QF_Strings | z3-BooledASS-base | 0.223419 |
| Bitvec | UltimateEliminator+MathSAT | 0.222794 |
| QF_Equality_Bitvec | z3-BooledASS | 0.218043 |
| QF_NonLinearIntArith | Z3-siri | 0.217661 |
| QF_NonLinearRealArith | Xolver | 0.213945 |
| QF_Datatypes | SMTInterpol | 0.202478 |
| QF_NonLinearIntArith | Z3-Z3++-base | 0.200993 |
| Bitvec | SMTInterpol | 0.200089 |
| QF_NonLinearIntArith | Yices2 | 0.19348 |
| QF_Bitvec | z3-BooledASS | 0.170265 |
| QF_NonLinearIntArith | cvc5 | 0.152929 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz-base | 0.149891 |
| QF_Equality_Bitvec | NeuroSym | 0.149865 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz | 0.149388 |
| QF_LinearIntArith | NeuroSym | 0.115507 |
| Arith | Amaya | 0.111439 |
| QF_Equality_NonLinearArith | Z3-alpha2-debug | 0.109881 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 0.109881 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 0.106393 |
| QF_LinearRealArith | Samet | 0.10622 |
| QF_Equality_NonLinearArith | Z3-alpha2-base | 0.10467 |
| QF_Equality_NonLinearArith | z3-BooledASS | 0.10467 |
| QF_Bitvec | Roole | 0.099405 |
| QF_NonLinearRealArith | SMTInterpol | 0.084558 |
| Arith | SMTInterpol | 0.083487 |
| QF_NonLinearIntArith | z3-BooledASS | 0.081969 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz | 0.076062 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz-base | 0.074607 |
| QF_Equality_NonLinearArith | cvc5 | 0.074607 |
| Equality | z3-BooledASS | 0.063903 |
| Equality | z3-BooledASS-base | 0.063365 |
| QF_Equality_NonLinearArith | Yices2 | 0.055704 |
| FPArith | colibri2 | 0.051808 |
| Equality_MachineArith | z3-BooledASS | 0.04038 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.032518 |
| Equality_MachineArith | Bitwuzla-fixed | 0.023849 |
| Equality_MachineArith | Bitwuzla | 0.023734 |
| Equality_MachineArith | bitwuzla-dandelion-base | 0.01906 |
| Arith | SMT-RAT | 0.016652 |
| Equality_MachineArith | bitwuzla-dandelion | 0.015727 |
| FPArith | UltimateEliminator+MathSAT | 0.014881 |
| Equality | Yices2 | 0.01207 |
| Equality | SMTInterpol | 0.008611 |
| QF_FPArith | z3-BooledASS | 0.003933 |
| QF_Equality_NonLinearArith | Xolver | 0.003404 |
| FPArith | Bitwuzla-fixed | 0.00303 |
| QF_NonLinearIntArith | Xolver | 0.001376 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.000612 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.00019 |
| QF_NonLinearIntArith | SMTInterpol | 0.000169 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.000154 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq | -6.545539 |
| Division | Solver | Contribution |
|---|---|---|
| QF_Strings | Z3-Noodler | 3.455639 |
| QF_Equality | Yices2 | 3.147367 |
| QF_Equality | z3-BooledASS-base | 3.12499 |
| QF_Equality | z3-BooledASS | 3.12499 |
| QF_Equality | OpenSMT-SMTS-seq-base | 3.116061 |
| QF_Equality | OpenSMT | 3.116061 |
| QF_Equality | OpenSMT-SMTS-seq | 3.111602 |
| QF_Equality | cvc5-cvc5-xyz | 3.111602 |
| QF_Equality | cvc5-cvc5-xyz-base | 3.111602 |
| QF_Equality | cvc5 | 3.107146 |
| QF_Bitvec | Bitwuzla-MachBV | 3.042375 |
| QF_Bitvec | Bitwuzla | 3.001962 |
| QF_Equality | SMTInterpol | 2.979302 |
| QF_Bitvec | bitwuzla-dandelion-base | 2.974335 |
| QF_Bitvec | Bitwuzla-SPFD-base | 2.96182 |
| QF_Bitvec | Bitwuzla-MachBV-base | 2.95932 |
| QF_Bitvec | NeuroSym | 2.919464 |
| QF_Strings | OSTRICH | 2.732183 |
| QF_Equality_LinearArith | z3-BooledASS-base | 2.674257 |
| QF_Equality_LinearArith | z3-BooledASS | 2.674257 |
| QF_FPArith | bitwuzla-dandelion-base | 2.662913 |
| QF_FPArith | Bitwuzla | 2.655046 |
| QF_Equality_Bitvec | bitwuzla-dandelion-base | 2.635359 |
| QF_Equality_Bitvec | bitwuzla-dandelion | 2.610189 |
| QF_Equality_Bitvec | Bitwuzla | 2.610189 |
| QF_Equality_LinearArith | SMTInterpol | 2.574176 |
| QF_Equality_Bitvec | Yices2 | 2.551178 |
| QF_Equality_LinearArith | Yices2 | 2.524852 |
| FPArith | Bitwuzla | 2.519641 |
| QF_Bitvec | Bitwuzla-SPFD | 2.405605 |
| FPArith | cvc5 | 2.384539 |
| FPArith | cvc5-cvc5-xyz-base | 2.379947 |
| FPArith | cvc5-cvc5-xyz | 2.379947 |
| QF_Equality_LinearArith | cvc5 | 2.376764 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz-base | 2.370815 |
| QF_Equality_LinearArith | OpenSMT | 2.364873 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq-base | 2.358938 |
| QF_NonLinearRealArith | Z3-GEX | 2.311209 |
| QF_Equality_LinearArith | cvc5-cvc5-xyz | 2.297077 |
| QF_Equality_Bitvec | z3-BooledASS-base | 2.281156 |
| Bitvec | Bitwuzla-fixed | 2.220479 |
| Bitvec | Bitwuzla | 2.196011 |
| QF_NonLinearRealArith | Z3-alpha2 | 2.183754 |
| QF_NonLinearRealArith | Yices2 | 2.178731 |
| QF_NonLinearRealArith | Z3-alpha2-debug | 2.173714 |
| QF_LinearIntArith | Yices2 | 2.140054 |
| QF_Bitvec | cvc5 | 2.104673 |
| QF_Bitvec | cvc5-cvc5-xyz | 2.100459 |
| QF_FPArith | cvc5-cvc5-xyz-base | 2.098202 |
| QF_FPArith | cvc5-cvc5-xyz | 2.098202 |
| QF_Bitvec | cvc5-cvc5-xyz-base | 2.09625 |
| QF_FPArith | cvc5 | 2.09471 |
| Arith | Z3-GEX | 2.079076 |
| Equality_LinearArith | z3-BooledASS-base | 2.077694 |
| Arith | Z3-alpha2-debug | 2.066959 |
| Arith | Z3-alpha2 | 2.066959 |
| QF_Bitvec | Z3-GEX | 2.031545 |
| QF_Bitvec | bitwuzla-dandelion | 2.025337 |
| Arith | z3-BooledASS-base | 2.002933 |
| Arith | z3-BooledASS | 1.998965 |
| Equality_LinearArith | cvc5-cvc5-xyz-base | 1.998931 |
| Equality_LinearArith | cvc5-cvc5-xyz | 1.998931 |
| Equality_LinearArith | cvc5 | 1.998931 |
| Equality_LinearArith | z3-BooledASS | 1.992935 |
| Arith | Z3-alpha2-base | 1.979183 |
| QF_NonLinearRealArith | cvc5 | 1.972987 |
| Arith | Z3-GEX-base | 1.971298 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz-base | 1.949173 |
| QF_NonLinearRealArith | cvc5-cvc5-xyz | 1.944428 |
| Arith | YicesQS | 1.943824 |
| QF_NonLinearIntArith | Z3-GEX | 1.940776 |
| QF_Equality | plat-smt | 1.910943 |
| QF_NonLinearIntArith | Z3-alpha2 | 1.867156 |
| QF_LinearIntArith | Z3-GEX | 1.865739 |
| Bitvec | YicesQS | 1.852723 |
| QF_NonLinearIntArith | Z3-alpha2-debug | 1.83176 |
| QF_LinearRealArith | Yices2 | 1.81113 |
| QF_Equality_Bitvec | cvc5 | 1.784525 |
| QF_NonLinearRealArith | Z3-GEX-base | 1.781983 |
| QF_NonLinearRealArith | Z3-siri-base | 1.777445 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz-base | 1.776984 |
| QF_Equality_Bitvec | cvc5-cvc5-xyz | 1.776984 |
| QF_NonLinearRealArith | Z3-siri | 1.772914 |
| QF_NonLinearIntArith | z3-BooledASS-base | 1.763713 |
| QF_NonLinearRealArith | z3-BooledASS | 1.745847 |
| QF_NonLinearRealArith | Z3-alpha2-base | 1.741356 |
| QF_NonLinearRealArith | z3-BooledASS-base | 1.741356 |
| QF_Equality_Bitvec | NeuroSym | 1.739516 |
| QF_NonLinearIntArith | Yices2 | 1.736169 |
| QF_NonLinearIntArith | Z3-siri-base | 1.696954 |
| QF_NonLinearIntArith | Z3-GEX-base | 1.696954 |
| FPArith | z3-BooledASS-base | 1.667436 |
| QF_NonLinearRealArith | SMT-RAT | 1.661508 |
| QF_LinearIntArith | QiuQi | 1.659827 |
| QF_LinearRealArith | OpenSMT-SMTS-seq | 1.653591 |
| QF_LinearRealArith | OpenSMT-SMTS-seq-base | 1.647894 |
| QF_LinearRealArith | OpenSMT | 1.647894 |
| QF_NonLinearIntArith | Z3-alpha2-base | 1.631483 |
| QF_LinearIntArith | z3-BooledASS-base | 1.631394 |
| QF_LinearIntArith | Z3-alpha2-base | 1.624324 |
| QF_Strings | Z3-GEX | 1.622337 |
| QF_LinearIntArith | Z3-alpha2 | 1.603206 |
| QF_LinearIntArith | Z3-GEX-base | 1.593865 |
| FPArith | bitwuzla-dandelion-base | 1.576503 |
| Bitvec | bitwuzla-dandelion-base | 1.572821 |
| QF_LinearIntArith | Z3-alpha2-debug | 1.570631 |
| QF_FPArith | colibri2 | 1.564296 |
| QF_Strings | cvc5 | 1.557242 |
| QF_Strings | cvc5-cvc5-xyz | 1.554666 |
| QF_Strings | cvc5-cvc5-xyz-base | 1.553379 |
| QF_Strings | Z3-GEX-base | 1.531577 |
| QF_Bitvec | Z3-alpha2 | 1.521612 |
| QF_LinearIntArith | z3-BooledASS | 1.520117 |
| QF_Bitvec | Z3-alpha2-debug | 1.514451 |
| Bitvec | bitwuzla-dandelion | 1.498017 |
| QF_Bitvec | z3-BooledASS-base | 1.493071 |
| QF_Bitvec | Z3-GEX-base | 1.489522 |
| QF_Bitvec | Z3-alpha2-base | 1.48775 |
| QF_Strings | z3-BooledASS | 1.484659 |
| QF_Strings | z3-BooledASS-base | 1.484659 |
| QF_Bitvec | bv_decide-nokernel | 1.463043 |
| Equality_NonLinearArith | z3-BooledASS | 1.459503 |
| Equality_NonLinearArith | z3-BooledASS-base | 1.458396 |
| QF_Strings | Z3-Noodler-base | 1.453371 |
| QF_NonLinearIntArith | Z3-Z3++ | 1.439673 |
| Arith | cvc5-cvc5-xyz | 1.43147 |
| Arith | cvc5-cvc5-xyz-base | 1.43147 |
| Arith | cvc5 | 1.428116 |
| QF_NonLinearIntArith | Z3-siri | 1.414798 |
| Bitvec | z3-BooledASS-base | 1.334785 |
| QF_LinearRealArith | cvc5 | 1.334282 |
| Bitvec | z3-BooledASS | 1.328451 |
| Equality_NonLinearArith | cvc5 | 1.318096 |
| Equality_NonLinearArith | cvc5-cvc5-xyz-base | 1.313891 |
| Equality_NonLinearArith | cvc5-cvc5-xyz | 1.312841 |
| QF_FPArith | z3-BooledASS-base | 1.31283 |
| QF_LinearIntArith | OpenSMT-SMTS-seq-base | 1.309354 |
| QF_LinearIntArith | OpenSMT | 1.30513 |
| QF_LinearRealArith | Z3-GEX | 1.298669 |
| QF_LinearRealArith | Z3-GEX-base | 1.283553 |
| QF_LinearRealArith | z3-BooledASS | 1.278535 |
| QF_Bitvec | bv_decide | 1.274473 |
| QF_LinearRealArith | z3-BooledASS-base | 1.273526 |
| QF_LinearIntArith | OpenSMT-SMTS-seq | 1.271586 |
| QF_Equality_NonLinearArith | Z3-alpha2 | 1.240516 |
| QF_Equality_NonLinearArith | Z3-alpha2-debug | 1.234616 |
| QF_LinearIntArith | cvc5 | 1.228222 |
| Bitvec | cvc5 | 1.223086 |
| Bitvec | cvc5-cvc5-xyz-base | 1.217024 |
| Bitvec | cvc5-cvc5-xyz | 1.217024 |
| QF_NonLinearIntArith | Z3-Z3++-base | 1.190716 |
| Arith | UltimateEliminator+MathSAT | 1.175556 |
| QF_Equality_NonLinearArith | Z3-alpha2-base | 1.159193 |
| QF_Equality_NonLinearArith | z3-BooledASS | 1.15349 |
| QF_Equality_NonLinearArith | z3-BooledASS-base | 1.142126 |
| QF_Equality_Bitvec | z3-BooledASS | 1.133356 |
| QF_Equality_NonLinearArith | Yices2 | 1.130818 |
| QF_Equality_Bitvec | SMTInterpol | 1.03482 |
| QF_LinearIntArith | cvc5-cvc5-xyz-base | 1.000395 |
| QF_LinearRealArith | cvc5-cvc5-xyz-base | 0.999828 |
| QF_LinearIntArith | cvc5-cvc5-xyz | 0.998548 |
| Equality_LinearArith | SMTInterpol | 0.995865 |
| QF_LinearRealArith | cvc5-cvc5-xyz | 0.995399 |
| Equality_MachineArith | z3-BooledASS-base | 0.947664 |
| QF_LinearIntArith | SMTInterpol | 0.936779 |
| Equality_MachineArith | cvc5 | 0.908234 |
| Equality_MachineArith | cvc5-cvc5-xyz-base | 0.903276 |
| Equality_MachineArith | cvc5-cvc5-xyz | 0.894808 |
| QF_Datatypes | Z3-Z3++ | 0.865561 |
| QF_Equality_NonLinearArith | cvc5 | 0.851652 |
| QF_LinearIntArith | NeuroSym | 0.835959 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz | 0.832187 |
| QF_Equality_NonLinearArith | cvc5-cvc5-xyz-base | 0.817735 |
| QF_LinearRealArith | SMTInterpol | 0.814256 |
| QF_FPArith | bitwuzla-dandelion | 0.792272 |
| QF_NonLinearRealArith | Xolver | 0.671828 |
| QF_NonLinearIntArith | z3-BooledASS | 0.633279 |
| QF_NonLinearIntArith | cvc5 | 0.569715 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz-base | 0.542544 |
| QF_NonLinearIntArith | cvc5-cvc5-xyz | 0.539672 |
| QF_LinearRealArith | Samet | 0.538553 |
| FPArith | Bitwuzla-fixed | 0.486805 |
| FPArith | z3-BooledASS | 0.456165 |
| QF_Equality_NonLinearArith | SMTInterpol | 0.381782 |
| QF_NonLinearIntArith | Xolver | 0.331611 |
| Equality_NonLinearArith | SMTInterpol | 0.31599 |
| Arith | Amaya | 0.296174 |
| FPArith | bitwuzla-dandelion | 0.291624 |
| Bitvec | UltimateEliminator+MathSAT | 0.254966 |
| Equality_MachineArith | SMTInterpol | 0.247908 |
| Bitvec | SMTInterpol | 0.202551 |
| QF_Equality_NonLinearArith | Xolver | 0.177786 |
| QF_Bitvec | z3-BooledASS | 0.169666 |
| Equality_MachineArith | Bitwuzla | 0.166038 |
| Equality_MachineArith | Bitwuzla-fixed | 0.166038 |
| Equality | cvc5-cvc5-xyz | 0.165149 |
| Equality | cvc5-cvc5-xyz-base | 0.162559 |
| Equality | cvc5 | 0.162559 |
| QF_Datatypes | cvc5-cvc5-xyz | 0.158634 |
| FPArith | colibri2 | 0.13943 |
| QF_Datatypes | SMTInterpol | 0.130903 |
| QF_Bitvec | SMTInterpol | 0.118073 |
| QF_Bitvec | Roole | 0.11658 |
| QF_Datatypes | Z3-alpha2-debug | 0.109827 |
| QF_Datatypes | Z3-alpha2 | 0.109827 |
| Arith | SMTInterpol | 0.096959 |
| QF_Datatypes | cvc5-cvc5-xyz-base | 0.085192 |
| QF_NonLinearRealArith | SMTInterpol | 0.084558 |
| QF_Datatypes | cvc5 | 0.083426 |
| QF_Datatypes | z3-BooledASS-base | 0.083426 |
| QF_Datatypes | z3-BooledASS | 0.083426 |
| QF_Datatypes | Z3-alpha2-base | 0.081679 |
| QF_Datatypes | Z3-Z3++-base | 0.074875 |
| Equality_MachineArith | z3-BooledASS | 0.074402 |
| Equality | z3-BooledASS-base | 0.071106 |
| Equality | z3-BooledASS | 0.070538 |
| Equality_MachineArith | bitwuzla-dandelion-base | 0.049024 |
| FPArith | UltimateEliminator+MathSAT | 0.042147 |
| Equality_MachineArith | bitwuzla-dandelion | 0.035455 |
| Arith | SMT-RAT | 0.018131 |
| Equality | Yices2 | 0.010053 |
| Equality_NonLinearArith | UltimateEliminator+MathSAT | 0.007183 |
| Equality | SMTInterpol | 0.005261 |
| QF_FPArith | z3-BooledASS | 0.004086 |
| Equality_MachineArith | UltimateEliminator+MathSAT | 0.003199 |
| Equality_LinearArith | UltimateEliminator+MathSAT | 0.001033 |
| QF_NonLinearIntArith | SMTInterpol | 0.000224 |
| Equality | UltimateEliminator+MathSAT | 0 |
| QF_FPArith | COLIBRI | -6.338173 |
| QF_Equality_LinearArith | OpenSMT-SMTS-seq | -6.545539 |
| QF_Bitvec | Yices2 | -6.809667 |