Average Error: 10.6 → 0.6
Time: 13.5s
Precision: 64
\[x + \frac{\left(y - z\right) \cdot t}{a - z}\]
\[\begin{array}{l} \mathbf{if}\;x + \frac{\left(y - z\right) \cdot t}{a - z} = -\infty \lor \neg \left(x + \frac{\left(y - z\right) \cdot t}{a - z} \le 3.29088473563426511 \cdot 10^{180}\right):\\ \;\;\;\;x + \frac{y - z}{\frac{a - z}{t}}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\left(y - z\right) \cdot t}{a - z}\\ \end{array}\]
x + \frac{\left(y - z\right) \cdot t}{a - z}
\begin{array}{l}
\mathbf{if}\;x + \frac{\left(y - z\right) \cdot t}{a - z} = -\infty \lor \neg \left(x + \frac{\left(y - z\right) \cdot t}{a - z} \le 3.29088473563426511 \cdot 10^{180}\right):\\
\;\;\;\;x + \frac{y - z}{\frac{a - z}{t}}\\

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

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r740703 = x;
        double r740704 = y;
        double r740705 = z;
        double r740706 = r740704 - r740705;
        double r740707 = t;
        double r740708 = r740706 * r740707;
        double r740709 = a;
        double r740710 = r740709 - r740705;
        double r740711 = r740708 / r740710;
        double r740712 = r740703 + r740711;
        return r740712;
}

double f(double x, double y, double z, double t, double a) {
        double r740713 = x;
        double r740714 = y;
        double r740715 = z;
        double r740716 = r740714 - r740715;
        double r740717 = t;
        double r740718 = r740716 * r740717;
        double r740719 = a;
        double r740720 = r740719 - r740715;
        double r740721 = r740718 / r740720;
        double r740722 = r740713 + r740721;
        double r740723 = -inf.0;
        bool r740724 = r740722 <= r740723;
        double r740725 = 3.290884735634265e+180;
        bool r740726 = r740722 <= r740725;
        double r740727 = !r740726;
        bool r740728 = r740724 || r740727;
        double r740729 = r740720 / r740717;
        double r740730 = r740716 / r740729;
        double r740731 = r740713 + r740730;
        double r740732 = r740728 ? r740731 : r740722;
        return r740732;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original10.6
Target0.5
Herbie0.6
\[\begin{array}{l} \mathbf{if}\;t \lt -1.0682974490174067 \cdot 10^{-39}:\\ \;\;\;\;x + \frac{y - z}{a - z} \cdot t\\ \mathbf{elif}\;t \lt 3.9110949887586375 \cdot 10^{-141}:\\ \;\;\;\;x + \frac{\left(y - z\right) \cdot t}{a - z}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y - z}{a - z} \cdot t\\ \end{array}\]

Derivation

  1. Split input into 2 regimes
  2. if (+ x (/ (* (- y z) t) (- a z))) < -inf.0 or 3.290884735634265e+180 < (+ x (/ (* (- y z) t) (- a z)))

    1. Initial program 37.4

      \[x + \frac{\left(y - z\right) \cdot t}{a - z}\]
    2. Using strategy rm
    3. Applied associate-/l*1.5

      \[\leadsto x + \color{blue}{\frac{y - z}{\frac{a - z}{t}}}\]

    if -inf.0 < (+ x (/ (* (- y z) t) (- a z))) < 3.290884735634265e+180

    1. Initial program 0.2

      \[x + \frac{\left(y - z\right) \cdot t}{a - z}\]
    2. Using strategy rm
    3. Applied pow10.2

      \[\leadsto \color{blue}{{\left(x + \frac{\left(y - z\right) \cdot t}{a - z}\right)}^{1}}\]
  3. Recombined 2 regimes into one program.
  4. Final simplification0.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;x + \frac{\left(y - z\right) \cdot t}{a - z} = -\infty \lor \neg \left(x + \frac{\left(y - z\right) \cdot t}{a - z} \le 3.29088473563426511 \cdot 10^{180}\right):\\ \;\;\;\;x + \frac{y - z}{\frac{a - z}{t}}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\left(y - z\right) \cdot t}{a - z}\\ \end{array}\]

Reproduce

herbie shell --seed 2020046 
(FPCore (x y z t a)
  :name "Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisTick from plot-0.2.3.4, A"
  :precision binary64

  :herbie-target
  (if (< t -1.0682974490174067e-39) (+ x (* (/ (- y z) (- a z)) t)) (if (< t 3.9110949887586375e-141) (+ x (/ (* (- y z) t) (- a z))) (+ x (* (/ (- y z) (- a z)) t))))

  (+ x (/ (* (- y z) t) (- a z))))