Timeout in 2.5m

Use the --timeout flag to change the timeout.

\[gz \ge 0.0 \cdot gz \land 0.0 \cdot gz \le 1 \cdot vz \land 1 \cdot vz \ge \left(-1\right) \cdot vz \land \left(-1\right) \cdot vz \le 1 \cdot vx \land 1 \cdot vx \ge \left(-1\right) \cdot vx \land \left(-1\right) \cdot vx \le 1\]
\[\frac{\left(-\left(\left(az - dz\right) - \frac{vz}{vx} \cdot \left(ax - dx\right)\right)\right) - \left(\left(bz - az\right) - \frac{vz}{vx} \cdot \left(bx - ax\right)\right) \cdot gz}{\left(\left(\left(dz - cz\right) - \left(bz - az\right)\right) - \frac{vz}{vx} \cdot \left(\left(dx - cx\right) - \left(bx - ax\right)\right)\right) \cdot gz + \left(\left(cz - az\right) - \frac{vz}{vx} \cdot \left(cx - ax\right)\right)}\]
\frac{\left(-\left(\left(az - dz\right) - \frac{vz}{vx} \cdot \left(ax - dx\right)\right)\right) - \left(\left(bz - az\right) - \frac{vz}{vx} \cdot \left(bx - ax\right)\right) \cdot gz}{\left(\left(\left(dz - cz\right) - \left(bz - az\right)\right) - \frac{vz}{vx} \cdot \left(\left(dx - cx\right) - \left(bx - ax\right)\right)\right) \cdot gz + \left(\left(cz - az\right) - \frac{vz}{vx} \cdot \left(cx - ax\right)\right)}
double f(double az, double dz, double vz, double vx, double ax, double dx, double bz, double bx, double gz, double cz, double cx) {
        double r3369339 = az;
        double r3369340 = dz;
        double r3369341 = r3369339 - r3369340;
        double r3369342 = vz;
        double r3369343 = vx;
        double r3369344 = r3369342 / r3369343;
        double r3369345 = ax;
        double r3369346 = dx;
        double r3369347 = r3369345 - r3369346;
        double r3369348 = r3369344 * r3369347;
        double r3369349 = r3369341 - r3369348;
        double r3369350 = -r3369349;
        double r3369351 = bz;
        double r3369352 = r3369351 - r3369339;
        double r3369353 = bx;
        double r3369354 = r3369353 - r3369345;
        double r3369355 = r3369344 * r3369354;
        double r3369356 = r3369352 - r3369355;
        double r3369357 = gz;
        double r3369358 = r3369356 * r3369357;
        double r3369359 = r3369350 - r3369358;
        double r3369360 = cz;
        double r3369361 = r3369340 - r3369360;
        double r3369362 = r3369361 - r3369352;
        double r3369363 = cx;
        double r3369364 = r3369346 - r3369363;
        double r3369365 = r3369364 - r3369354;
        double r3369366 = r3369344 * r3369365;
        double r3369367 = r3369362 - r3369366;
        double r3369368 = r3369367 * r3369357;
        double r3369369 = r3369360 - r3369339;
        double r3369370 = r3369363 - r3369345;
        double r3369371 = r3369344 * r3369370;
        double r3369372 = r3369369 - r3369371;
        double r3369373 = r3369368 + r3369372;
        double r3369374 = r3369359 / r3369373;
        return r3369374;
}

Reproduce

herbie shell --seed 1 
(FPCore (az dz vz vx ax dx bz bx gz cz cx)
  :name "(-((az - dz) - (vz/vx) * (ax - dx)) - ((bz - az) - ((vz/vx) * (bx - ax)))*gz) / ((((dz - cz) - (bz - az)) - (vz/vx) * ((dx - cx) - (bx - ax)))*gz + ((cz - az) - (vz/vx) * (cx - ax)))"
  :precision binary64
  :pre (and (>= gz (* 0.0 gz)) (<= (* 0.0 gz) (* 1 vz)) (>= (* 1 vz) (* (- 1) vz)) (<= (* (- 1) vz) (* 1 vx)) (>= (* 1 vx) (* (- 1) vx)) (<= (* (- 1) vx) 1))
  (/ (- (- (- (- az dz) (* (/ vz vx) (- ax dx)))) (* (- (- bz az) (* (/ vz vx) (- bx ax))) gz)) (+ (* (- (- (- dz cz) (- bz az)) (* (/ vz vx) (- (- dx cx) (- bx ax)))) gz) (- (- cz az) (* (/ vz vx) (- cx ax))))))