\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\cos^{-1} \left(\frac{\log \left(e^{1 - 5 \cdot \left(v \cdot v\right)}\right)}{v \cdot v - 1}\right)double f(double v) {
double r301919 = 1.0;
double r301920 = 5.0;
double r301921 = v;
double r301922 = r301921 * r301921;
double r301923 = r301920 * r301922;
double r301924 = r301919 - r301923;
double r301925 = r301922 - r301919;
double r301926 = r301924 / r301925;
double r301927 = acos(r301926);
return r301927;
}
double f(double v) {
double r301928 = 1.0;
double r301929 = 5.0;
double r301930 = v;
double r301931 = r301930 * r301930;
double r301932 = r301929 * r301931;
double r301933 = r301928 - r301932;
double r301934 = exp(r301933);
double r301935 = log(r301934);
double r301936 = r301931 - r301928;
double r301937 = r301935 / r301936;
double r301938 = acos(r301937);
return r301938;
}



Bits error versus v
Results
Initial program 0.6
rmApplied add-log-exp0.6
Applied add-log-exp0.6
Applied diff-log0.6
Simplified0.6
Final simplification0.6
herbie shell --seed 2020027 +o rules:numerics
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))