\[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]

↓

\[\begin{array}{l} \mathbf{if}\;t \le -6.383228782902789 \cdot 10^{-256}:\\ \;\;\;\;\frac{x}{x + e^{\left(\frac{\sqrt{t + a} \cdot z}{t} - \left(\left(\frac{5.0}{6.0} + a\right) - \left(\left(\frac{2.0}{t \cdot 3.0}\right)\right)\right) \cdot \left(b - c\right)\right) \cdot 2.0} \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{\sqrt{t + a} \cdot z}{t} - \left(b - c\right) \cdot \left(\left(\frac{5.0}{6.0} + a\right) - \sqrt[3]{\left(\frac{2.0}{t \cdot 3.0} \cdot \frac{2.0}{t \cdot 3.0}\right) \cdot \frac{2.0}{t \cdot 3.0}}\right)\right)}}\\ \end{array}\]

\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}

↓

\begin{array}{l}
\mathbf{if}\;t \le -6.383228782902789 \cdot 10^{-256}:\\
\;\;\;\;\frac{x}{x + e^{\left(\frac{\sqrt{t + a} \cdot z}{t} - \left(\left(\frac{5.0}{6.0} + a\right) - \left(\left(\frac{2.0}{t \cdot 3.0}\right)\right)\right) \cdot \left(b - c\right)\right) \cdot 2.0} \cdot y}\\

\mathbf{else}:\\
\;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{\sqrt{t + a} \cdot z}{t} - \left(b - c\right) \cdot \left(\left(\frac{5.0}{6.0} + a\right) - \sqrt[3]{\left(\frac{2.0}{t \cdot 3.0} \cdot \frac{2.0}{t \cdot 3.0}\right) \cdot \frac{2.0}{t \cdot 3.0}}\right)\right)}}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r20143282 = x;
        double r20143283 = y;
        double r20143284 = 2.0;
        double r20143285 = z;
        double r20143286 = t;
        double r20143287 = a;
        double r20143288 = r20143286 + r20143287;
        double r20143289 = sqrt(r20143288);
        double r20143290 = r20143285 * r20143289;
        double r20143291 = r20143290 / r20143286;
        double r20143292 = b;
        double r20143293 = c;
        double r20143294 = r20143292 - r20143293;
        double r20143295 = 5.0;
        double r20143296 = 6.0;
        double r20143297 = r20143295 / r20143296;
        double r20143298 = r20143287 + r20143297;
        double r20143299 = 3.0;
        double r20143300 = r20143286 * r20143299;
        double r20143301 = r20143284 / r20143300;
        double r20143302 = r20143298 - r20143301;
        double r20143303 = r20143294 * r20143302;
        double r20143304 = r20143291 - r20143303;
        double r20143305 = r20143284 * r20143304;
        double r20143306 = exp(r20143305);
        double r20143307 = r20143283 * r20143306;
        double r20143308 = r20143282 + r20143307;
        double r20143309 = r20143282 / r20143308;
        return r20143309;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r20143310 = t;
        double r20143311 = -6.383228782902789e-256;
        bool r20143312 = r20143310 <= r20143311;
        double r20143313 = x;
        double r20143314 = a;
        double r20143315 = r20143310 + r20143314;
        double r20143316 = sqrt(r20143315);
        double r20143317 = z;
        double r20143318 = r20143316 * r20143317;
        double r20143319 = r20143318 / r20143310;
        double r20143320 = 5.0;
        double r20143321 = 6.0;
        double r20143322 = r20143320 / r20143321;
        double r20143323 = r20143322 + r20143314;
        double r20143324 = 2.0;
        double r20143325 = 3.0;
        double r20143326 = r20143310 * r20143325;
        double r20143327 = r20143324 / r20143326;
        double r20143328 = /* ERROR: no posit support in C */;
        double r20143329 = /* ERROR: no posit support in C */;
        double r20143330 = r20143323 - r20143329;
        double r20143331 = b;
        double r20143332 = c;
        double r20143333 = r20143331 - r20143332;
        double r20143334 = r20143330 * r20143333;
        double r20143335 = r20143319 - r20143334;
        double r20143336 = r20143335 * r20143324;
        double r20143337 = exp(r20143336);
        double r20143338 = y;
        double r20143339 = r20143337 * r20143338;
        double r20143340 = r20143313 + r20143339;
        double r20143341 = r20143313 / r20143340;
        double r20143342 = r20143327 * r20143327;
        double r20143343 = r20143342 * r20143327;
        double r20143344 = cbrt(r20143343);
        double r20143345 = r20143323 - r20143344;
        double r20143346 = r20143333 * r20143345;
        double r20143347 = r20143319 - r20143346;
        double r20143348 = r20143324 * r20143347;
        double r20143349 = exp(r20143348);
        double r20143350 = r20143338 * r20143349;
        double r20143351 = r20143313 + r20143350;
        double r20143352 = r20143313 / r20143351;
        double r20143353 = r20143312 ? r20143341 : r20143352;
        return r20143353;
}

Target

Original	4.0
Target	3.2
Herbie	6.9

\[\begin{array}{l} \mathbf{if}\;t \lt -2.118326644891581 \cdot 10^{-50}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\left(a \cdot c + 0.8333333333333334 \cdot c\right) - a \cdot b\right)}}\\ \mathbf{elif}\;t \lt 5.196588770651547 \cdot 10^{-123}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \frac{\left(z \cdot \sqrt{t + a}\right) \cdot \left(\left(3.0 \cdot t\right) \cdot \left(a - \frac{5.0}{6.0}\right)\right) - \left(\left(\frac{5.0}{6.0} + a\right) \cdot \left(3.0 \cdot t\right) - 2.0\right) \cdot \left(\left(a - \frac{5.0}{6.0}\right) \cdot \left(\left(b - c\right) \cdot t\right)\right)}{\left(\left(t \cdot t\right) \cdot 3.0\right) \cdot \left(a - \frac{5.0}{6.0}\right)}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\\ \end{array}\]

Derivation

Split input into 2 regimes
if t < -6.383228782902789e-256
1. Initial program 5.0
  \[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]
2. Using strategy rm
3. Applied insert-posit166.8
  \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \color{blue}{\left(\left(\frac{2.0}{t \cdot 3.0}\right)\right)}\right)\right)}}\]
if -6.383228782902789e-256 < t
1. Initial program 3.7
  \[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]
2. Using strategy rm
3. Applied add-cbrt-cube6.9
  \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \color{blue}{\sqrt[3]{\left(\frac{2.0}{t \cdot 3.0} \cdot \frac{2.0}{t \cdot 3.0}\right) \cdot \frac{2.0}{t \cdot 3.0}}}\right)\right)}}\]
Recombined 2 regimes into one program.
Final simplification6.9
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -6.383228782902789 \cdot 10^{-256}:\\ \;\;\;\;\frac{x}{x + e^{\left(\frac{\sqrt{t + a} \cdot z}{t} - \left(\left(\frac{5.0}{6.0} + a\right) - \left(\left(\frac{2.0}{t \cdot 3.0}\right)\right)\right) \cdot \left(b - c\right)\right) \cdot 2.0} \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{\sqrt{t + a} \cdot z}{t} - \left(b - c\right) \cdot \left(\left(\frac{5.0}{6.0} + a\right) - \sqrt[3]{\left(\frac{2.0}{t \cdot 3.0} \cdot \frac{2.0}{t \cdot 3.0}\right) \cdot \frac{2.0}{t \cdot 3.0}}\right)\right)}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019168 
(FPCore (x y z t a b c)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, I"

  :herbie-target
  (if (< t -2.118326644891581e-50) (/ x (+ x (* y (exp (* 2.0 (- (+ (* a c) (* 0.8333333333333334 c)) (* a b))))))) (if (< t 5.196588770651547e-123) (/ x (+ x (* y (exp (* 2.0 (/ (- (* (* z (sqrt (+ t a))) (* (* 3.0 t) (- a (/ 5.0 6.0)))) (* (- (* (+ (/ 5.0 6.0) a) (* 3.0 t)) 2.0) (* (- a (/ 5.0 6.0)) (* (- b c) t)))) (* (* (* t t) 3.0) (- a (/ 5.0 6.0))))))))) (/ x (+ x (* y (exp (* 2.0 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5.0 6.0)) (/ 2.0 (* t 3.0))))))))))))

  (/ x (+ x (* y (exp (* 2.0 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5.0 6.0)) (/ 2.0 (* t 3.0)))))))))))

Error

Target

Derivation

`if t < -6.383228782902789e-256`

`if -6.383228782902789e-256 < t`

Reproduce