\[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\]

↓

\[\begin{array}{l} \mathbf{if}\;b \le -9.238052366259206 \cdot 10^{-38}:\\ \;\;\;\;-\frac{c}{b}\\ \mathbf{elif}\;b \le 2.7654658503846575 \cdot 10^{+109}:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(\sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*} + b\right)\\ \mathbf{else}:\\ \;\;\;\;-\frac{b}{a}\\ \end{array}\]

double f(double a, double b, double c) {
        double r12254868 = b;
        double r12254869 = -r12254868;
        double r12254870 = r12254868 * r12254868;
        double r12254871 = 4.0;
        double r12254872 = a;
        double r12254873 = c;
        double r12254874 = r12254872 * r12254873;
        double r12254875 = r12254871 * r12254874;
        double r12254876 = r12254870 - r12254875;
        double r12254877 = sqrt(r12254876);
        double r12254878 = r12254869 - r12254877;
        double r12254879 = 2.0;
        double r12254880 = r12254879 * r12254872;
        double r12254881 = r12254878 / r12254880;
        return r12254881;
}

↓

double f(double a, double b, double c) {
        double r12254882 = b;
        double r12254883 = -9.238052366259206e-38;
        bool r12254884 = r12254882 <= r12254883;
        double r12254885 = c;
        double r12254886 = r12254885 / r12254882;
        double r12254887 = -r12254886;
        double r12254888 = 2.7654658503846575e+109;
        bool r12254889 = r12254882 <= r12254888;
        double r12254890 = -0.5;
        double r12254891 = a;
        double r12254892 = r12254890 / r12254891;
        double r12254893 = -4.0;
        double r12254894 = r12254885 * r12254893;
        double r12254895 = r12254882 * r12254882;
        double r12254896 = fma(r12254891, r12254894, r12254895);
        double r12254897 = sqrt(r12254896);
        double r12254898 = r12254897 + r12254882;
        double r12254899 = r12254892 * r12254898;
        double r12254900 = r12254882 / r12254891;
        double r12254901 = -r12254900;
        double r12254902 = r12254889 ? r12254899 : r12254901;
        double r12254903 = r12254884 ? r12254887 : r12254902;
        return r12254903;
}

\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}

↓

\begin{array}{l}
\mathbf{if}\;b \le -9.238052366259206 \cdot 10^{-38}:\\
\;\;\;\;-\frac{c}{b}\\

\mathbf{elif}\;b \le 2.7654658503846575 \cdot 10^{+109}:\\
\;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(\sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*} + b\right)\\

\mathbf{else}:\\
\;\;\;\;-\frac{b}{a}\\

\end{array}

Original	33.5
Target	20.8
Herbie	10.3

Derivation

Split input into 3 regimes
if b < -9.238052366259206e-38
1. Initial program 53.5
  \[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\]
2. Simplified53.5
  \[\leadsto \color{blue}{\frac{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}{a}}\]
3. Using strategy rm
4. Applied *-un-lft-identity53.5
  \[\leadsto \frac{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}{\color{blue}{1 \cdot a}}\]
5. Applied div-inv53.5
  \[\leadsto \frac{\color{blue}{\left(\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}\right) \cdot \frac{1}{2}}}{1 \cdot a}\]
6. Applied times-frac53.5
  \[\leadsto \color{blue}{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{1} \cdot \frac{\frac{1}{2}}{a}}\]
7. Simplified53.5
  \[\leadsto \color{blue}{\left(-\left(b + \sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*}\right)\right)} \cdot \frac{\frac{1}{2}}{a}\]
8. Simplified53.5
  \[\leadsto \left(-\left(b + \sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*}\right)\right) \cdot \color{blue}{\frac{\frac{1}{2}}{a}}\]
9. Taylor expanded around -inf 7.8
  \[\leadsto \color{blue}{-1 \cdot \frac{c}{b}}\]
10. Simplified7.8
  \[\leadsto \color{blue}{-\frac{c}{b}}\]
if -9.238052366259206e-38 < b < 2.7654658503846575e+109
1. Initial program 14.2
  \[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\]
2. Simplified14.2
  \[\leadsto \color{blue}{\frac{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}{a}}\]
3. Using strategy rm
4. Applied *-un-lft-identity14.2
  \[\leadsto \frac{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}{\color{blue}{1 \cdot a}}\]
5. Applied div-inv14.2
  \[\leadsto \frac{\color{blue}{\left(\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}\right) \cdot \frac{1}{2}}}{1 \cdot a}\]
6. Applied times-frac14.3
  \[\leadsto \color{blue}{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{1} \cdot \frac{\frac{1}{2}}{a}}\]
7. Simplified14.4
  \[\leadsto \color{blue}{\left(-\left(b + \sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*}\right)\right)} \cdot \frac{\frac{1}{2}}{a}\]
8. Simplified14.4
  \[\leadsto \left(-\left(b + \sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*}\right)\right) \cdot \color{blue}{\frac{\frac{1}{2}}{a}}\]
if 2.7654658503846575e+109 < b
1. Initial program 47.4
  \[\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\]
2. Simplified47.4
  \[\leadsto \color{blue}{\frac{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}{a}}\]
3. Using strategy rm
4. Applied *-un-lft-identity47.4
  \[\leadsto \frac{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{\color{blue}{1 \cdot 2}}}{a}\]
5. Applied *-un-lft-identity47.4
  \[\leadsto \frac{\frac{\left(-b\right) - \color{blue}{1 \cdot \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}}{1 \cdot 2}}{a}\]
6. Applied *-un-lft-identity47.4
  \[\leadsto \frac{\frac{\left(-\color{blue}{1 \cdot b}\right) - 1 \cdot \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{1 \cdot 2}}{a}\]
7. Applied distribute-rgt-neg-in47.4
  \[\leadsto \frac{\frac{\color{blue}{1 \cdot \left(-b\right)} - 1 \cdot \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{1 \cdot 2}}{a}\]
8. Applied distribute-lft-out--47.4
  \[\leadsto \frac{\frac{\color{blue}{1 \cdot \left(\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}\right)}}{1 \cdot 2}}{a}\]
9. Applied times-frac47.4
  \[\leadsto \frac{\color{blue}{\frac{1}{1} \cdot \frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}}{a}\]
10. Applied associate-/l*47.5
  \[\leadsto \color{blue}{\frac{\frac{1}{1}}{\frac{a}{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}}}\]
11. Simplified47.5
  \[\leadsto \frac{\color{blue}{1}}{\frac{a}{\frac{\left(-b\right) - \sqrt{(\left(a \cdot c\right) \cdot -4 + \left(b \cdot b\right))_*}}{2}}}\]
12. Taylor expanded around 0 3.4
  \[\leadsto \color{blue}{-1 \cdot \frac{b}{a}}\]
13. Simplified3.4
  \[\leadsto \color{blue}{-\frac{b}{a}}\]
Recombined 3 regimes into one program.
Final simplification10.3
\[\leadsto \begin{array}{l} \mathbf{if}\;b \le -9.238052366259206 \cdot 10^{-38}:\\ \;\;\;\;-\frac{c}{b}\\ \mathbf{elif}\;b \le 2.7654658503846575 \cdot 10^{+109}:\\ \;\;\;\;\frac{\frac{-1}{2}}{a} \cdot \left(\sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*} + b\right)\\ \mathbf{else}:\\ \;\;\;\;-\frac{b}{a}\\ \end{array}\]

Error

Target

Derivation

`if b < -9.238052366259206e-38`

`if -9.238052366259206e-38 < b < 2.7654658503846575e+109`

`if 2.7654658503846575e+109 < b`

Reproduce