\[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]

↓

\[\begin{array}{l} \mathbf{if}\;\left(y \cdot 9\right) \cdot z \le -2.616507040877682570245126886877728515495 \cdot 10^{173} \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 6.743032447782565923529056966013493692094 \cdot 10^{232}\right):\\ \;\;\;\;\mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;27 \cdot \left(a \cdot b\right) + \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)\\ \end{array}\]

\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b

↓

\begin{array}{l}
\mathbf{if}\;\left(y \cdot 9\right) \cdot z \le -2.616507040877682570245126886877728515495 \cdot 10^{173} \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 6.743032447782565923529056966013493692094 \cdot 10^{232}\right):\\
\;\;\;\;\mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;27 \cdot \left(a \cdot b\right) + \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)\\

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r450522 = x;
        double r450523 = 2.0;
        double r450524 = r450522 * r450523;
        double r450525 = y;
        double r450526 = 9.0;
        double r450527 = r450525 * r450526;
        double r450528 = z;
        double r450529 = r450527 * r450528;
        double r450530 = t;
        double r450531 = r450529 * r450530;
        double r450532 = r450524 - r450531;
        double r450533 = a;
        double r450534 = 27.0;
        double r450535 = r450533 * r450534;
        double r450536 = b;
        double r450537 = r450535 * r450536;
        double r450538 = r450532 + r450537;
        return r450538;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r450539 = y;
        double r450540 = 9.0;
        double r450541 = r450539 * r450540;
        double r450542 = z;
        double r450543 = r450541 * r450542;
        double r450544 = -2.6165070408776826e+173;
        bool r450545 = r450543 <= r450544;
        double r450546 = 6.743032447782566e+232;
        bool r450547 = r450543 <= r450546;
        double r450548 = !r450547;
        bool r450549 = r450545 || r450548;
        double r450550 = a;
        double r450551 = 27.0;
        double r450552 = r450550 * r450551;
        double r450553 = b;
        double r450554 = x;
        double r450555 = 2.0;
        double r450556 = r450554 * r450555;
        double r450557 = t;
        double r450558 = r450542 * r450557;
        double r450559 = r450540 * r450558;
        double r450560 = r450539 * r450559;
        double r450561 = r450556 - r450560;
        double r450562 = fma(r450552, r450553, r450561);
        double r450563 = r450550 * r450553;
        double r450564 = r450551 * r450563;
        double r450565 = r450543 * r450557;
        double r450566 = r450556 - r450565;
        double r450567 = r450564 + r450566;
        double r450568 = r450549 ? r450562 : r450567;
        return r450568;
}

Original	3.7
Target	2.7
Herbie	0.4

Derivation

Split input into 2 regimes
if (* (* y 9.0) z) < -2.6165070408776826e+173 or 6.743032447782566e+232 < (* (* y 9.0) z)
1. Initial program 27.4
  \[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]
2. Simplified27.4
  \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)}\]
3. Using strategy rm
4. Applied associate-*l*1.4
  \[\leadsto \mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right)\]
5. Using strategy rm
6. Applied associate-*l*0.8
  \[\leadsto \mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - \color{blue}{y \cdot \left(9 \cdot \left(z \cdot t\right)\right)}\right)\]
if -2.6165070408776826e+173 < (* (* y 9.0) z) < 6.743032447782566e+232
1. Initial program 0.4
  \[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]
2. Simplified0.4
  \[\leadsto \color{blue}{\mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)}\]
3. Using strategy rm
4. Applied fma-udef0.4
  \[\leadsto \color{blue}{\left(a \cdot 27\right) \cdot b + \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)}\]
5. Simplified0.3
  \[\leadsto \color{blue}{27 \cdot \left(a \cdot b\right)} + \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)\]
Recombined 2 regimes into one program.
Final simplification0.4
\[\leadsto \begin{array}{l} \mathbf{if}\;\left(y \cdot 9\right) \cdot z \le -2.616507040877682570245126886877728515495 \cdot 10^{173} \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 6.743032447782565923529056966013493692094 \cdot 10^{232}\right):\\ \;\;\;\;\mathsf{fma}\left(a \cdot 27, b, x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;27 \cdot \left(a \cdot b\right) + \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)\\ \end{array}\]

Error

Target

Derivation

`if (* (* y 9.0) z) < -2.6165070408776826e+173 or 6.743032447782566e+232 < (* (* y 9.0) z)`

`if -2.6165070408776826e+173 < (* (* y 9.0) z) < 6.743032447782566e+232`

Reproduce