Example 2 from Robby

Specification

?
\[\begin{array}{l} t_1 := \tan^{-1} \left(\frac{\left(-eh\right) \cdot \tan t}{ew}\right)\\ \left|\left(ew \cdot \cos t\right) \cdot \cos t\_1 - \left(eh \cdot \sin t\right) \cdot \sin t\_1\right| \end{array} \]
(FPCore (eh ew t)
  :precision binary64
  :pre TRUE
  (let* ((t_1 (atan (/ (* (- eh) (tan t)) ew))))
  (fabs
   (- (* (* ew (cos t)) (cos t_1)) (* (* eh (sin t)) (sin t_1))))))
double code(double eh, double ew, double t) {
	double t_1 = atan(((-eh * tan(t)) / ew));
	return fabs((((ew * cos(t)) * cos(t_1)) - ((eh * sin(t)) * sin(t_1))));
}
real(8) function code(eh, ew, t)
use fmin_fmax_functions
    real(8), intent (in) :: eh
    real(8), intent (in) :: ew
    real(8), intent (in) :: t
    real(8) :: t_1
    t_1 = atan(((-eh * tan(t)) / ew))
    code = abs((((ew * cos(t)) * cos(t_1)) - ((eh * sin(t)) * sin(t_1))))
end function
public static double code(double eh, double ew, double t) {
	double t_1 = Math.atan(((-eh * Math.tan(t)) / ew));
	return Math.abs((((ew * Math.cos(t)) * Math.cos(t_1)) - ((eh * Math.sin(t)) * Math.sin(t_1))));
}
def code(eh, ew, t):
	t_1 = math.atan(((-eh * math.tan(t)) / ew))
	return math.fabs((((ew * math.cos(t)) * math.cos(t_1)) - ((eh * math.sin(t)) * math.sin(t_1))))
function code(eh, ew, t)
	t_1 = atan(Float64(Float64(Float64(-eh) * tan(t)) / ew))
	return abs(Float64(Float64(Float64(ew * cos(t)) * cos(t_1)) - Float64(Float64(eh * sin(t)) * sin(t_1))))
end
function tmp = code(eh, ew, t)
	t_1 = atan(((-eh * tan(t)) / ew));
	tmp = abs((((ew * cos(t)) * cos(t_1)) - ((eh * sin(t)) * sin(t_1))));
end
code[eh_, ew_, t_] := Block[{t$95$1 = N[ArcTan[N[(N[((-eh) * N[Tan[t], $MachinePrecision]), $MachinePrecision] / ew), $MachinePrecision]], $MachinePrecision]}, N[Abs[N[(N[(N[(ew * N[Cos[t], $MachinePrecision]), $MachinePrecision] * N[Cos[t$95$1], $MachinePrecision]), $MachinePrecision] - N[(N[(eh * N[Sin[t], $MachinePrecision]), $MachinePrecision] * N[Sin[t$95$1], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]
f(eh, ew, t):
	eh in [-inf, +inf],
	ew in [-inf, +inf],
	t in [-inf, +inf]
code: THEORY
BEGIN
f(eh, ew, t: real): real =
	LET t_1 = (atan((((- eh) * (tan(t))) / ew))) IN
	abs((((ew * (cos(t))) * (cos(t_1))) - ((eh * (sin(t))) * (sin(t_1)))))
END code
\begin{array}{l}
t_1 := \tan^{-1} \left(\frac{\left(-eh\right) \cdot \tan t}{ew}\right)\\
\left|\left(ew \cdot \cos t\right) \cdot \cos t\_1 - \left(eh \cdot \sin t\right) \cdot \sin t\_1\right|
\end{array}

Timeout after 2.5min

Use the --timeout flag to change the timeout.