\[\frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{t}}\]

↓

\[\begin{array}{l} \mathbf{if}\;t \le -1.4387487013439223 \cdot 10^{28} \lor \neg \left(t \le 1.17534675755780474 \cdot 10^{-10}\right):\\ \;\;\;\;\frac{1 \cdot \mathsf{fma}\left(\frac{y}{t}, z, x\right)}{\left(a + 1\right) + y \cdot \frac{b}{t}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \left(y \cdot z\right) \cdot \frac{1}{t}}{\left(a + 1\right) + \left(y \cdot b\right) \cdot \frac{1}{t}}\\ \end{array}\]

\frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{t}}

↓

\begin{array}{l}
\mathbf{if}\;t \le -1.4387487013439223 \cdot 10^{28} \lor \neg \left(t \le 1.17534675755780474 \cdot 10^{-10}\right):\\
\;\;\;\;\frac{1 \cdot \mathsf{fma}\left(\frac{y}{t}, z, x\right)}{\left(a + 1\right) + y \cdot \frac{b}{t}}\\

\mathbf{else}:\\
\;\;\;\;\frac{x + \left(y \cdot z\right) \cdot \frac{1}{t}}{\left(a + 1\right) + \left(y \cdot b\right) \cdot \frac{1}{t}}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r766450 = x;
        double r766451 = y;
        double r766452 = z;
        double r766453 = r766451 * r766452;
        double r766454 = t;
        double r766455 = r766453 / r766454;
        double r766456 = r766450 + r766455;
        double r766457 = a;
        double r766458 = 1.0;
        double r766459 = r766457 + r766458;
        double r766460 = b;
        double r766461 = r766451 * r766460;
        double r766462 = r766461 / r766454;
        double r766463 = r766459 + r766462;
        double r766464 = r766456 / r766463;
        return r766464;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r766465 = t;
        double r766466 = -1.4387487013439223e+28;
        bool r766467 = r766465 <= r766466;
        double r766468 = 1.1753467575578047e-10;
        bool r766469 = r766465 <= r766468;
        double r766470 = !r766469;
        bool r766471 = r766467 || r766470;
        double r766472 = 1.0;
        double r766473 = y;
        double r766474 = r766473 / r766465;
        double r766475 = z;
        double r766476 = x;
        double r766477 = fma(r766474, r766475, r766476);
        double r766478 = r766472 * r766477;
        double r766479 = a;
        double r766480 = 1.0;
        double r766481 = r766479 + r766480;
        double r766482 = b;
        double r766483 = r766482 / r766465;
        double r766484 = r766473 * r766483;
        double r766485 = r766481 + r766484;
        double r766486 = r766478 / r766485;
        double r766487 = r766473 * r766475;
        double r766488 = r766472 / r766465;
        double r766489 = r766487 * r766488;
        double r766490 = r766476 + r766489;
        double r766491 = r766473 * r766482;
        double r766492 = r766491 * r766488;
        double r766493 = r766481 + r766492;
        double r766494 = r766490 / r766493;
        double r766495 = r766471 ? r766486 : r766494;
        return r766495;
}

Original	16.9
Target	13.0
Herbie	12.8

Derivation

Split input into 2 regimes
if t < -1.4387487013439223e+28 or 1.1753467575578047e-10 < t
1. Initial program 12.2
  \[\frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{t}}\]
2. Using strategy rm
3. Applied *-un-lft-identity12.2
  \[\leadsto \frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{\color{blue}{1 \cdot t}}}\]
4. Applied times-frac8.9
  \[\leadsto \frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \color{blue}{\frac{y}{1} \cdot \frac{b}{t}}}\]
5. Simplified8.9
  \[\leadsto \frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \color{blue}{y} \cdot \frac{b}{t}}\]
6. Using strategy rm
7. Applied *-un-lft-identity8.9
  \[\leadsto \frac{x + \color{blue}{1 \cdot \frac{y \cdot z}{t}}}{\left(a + 1\right) + y \cdot \frac{b}{t}}\]
8. Applied *-un-lft-identity8.9
  \[\leadsto \frac{\color{blue}{1 \cdot x} + 1 \cdot \frac{y \cdot z}{t}}{\left(a + 1\right) + y \cdot \frac{b}{t}}\]
9. Applied distribute-lft-out8.9
  \[\leadsto \frac{\color{blue}{1 \cdot \left(x + \frac{y \cdot z}{t}\right)}}{\left(a + 1\right) + y \cdot \frac{b}{t}}\]
10. Simplified3.8
  \[\leadsto \frac{1 \cdot \color{blue}{\mathsf{fma}\left(\frac{y}{t}, z, x\right)}}{\left(a + 1\right) + y \cdot \frac{b}{t}}\]
if -1.4387487013439223e+28 < t < 1.1753467575578047e-10
1. Initial program 21.7
  \[\frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{t}}\]
2. Using strategy rm
3. Applied *-un-lft-identity21.7
  \[\leadsto \frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{\color{blue}{1 \cdot t}}}\]
4. Applied times-frac26.1
  \[\leadsto \frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \color{blue}{\frac{y}{1} \cdot \frac{b}{t}}}\]
5. Simplified26.1
  \[\leadsto \frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \color{blue}{y} \cdot \frac{b}{t}}\]
6. Using strategy rm
7. Applied div-inv26.1
  \[\leadsto \frac{x + \color{blue}{\left(y \cdot z\right) \cdot \frac{1}{t}}}{\left(a + 1\right) + y \cdot \frac{b}{t}}\]
8. Using strategy rm
9. Applied div-inv26.1
  \[\leadsto \frac{x + \left(y \cdot z\right) \cdot \frac{1}{t}}{\left(a + 1\right) + y \cdot \color{blue}{\left(b \cdot \frac{1}{t}\right)}}\]
10. Applied associate-*r*21.7
  \[\leadsto \frac{x + \left(y \cdot z\right) \cdot \frac{1}{t}}{\left(a + 1\right) + \color{blue}{\left(y \cdot b\right) \cdot \frac{1}{t}}}\]
Recombined 2 regimes into one program.
Final simplification12.8
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -1.4387487013439223 \cdot 10^{28} \lor \neg \left(t \le 1.17534675755780474 \cdot 10^{-10}\right):\\ \;\;\;\;\frac{1 \cdot \mathsf{fma}\left(\frac{y}{t}, z, x\right)}{\left(a + 1\right) + y \cdot \frac{b}{t}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \left(y \cdot z\right) \cdot \frac{1}{t}}{\left(a + 1\right) + \left(y \cdot b\right) \cdot \frac{1}{t}}\\ \end{array}\]

Error

Target

Derivation

`if t < -1.4387487013439223e+28 or 1.1753467575578047e-10 < t`

`if -1.4387487013439223e+28 < t < 1.1753467575578047e-10`

Reproduce