\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 r317138 = 1.0;
double r317139 = 5.0;
double r317140 = v;
double r317141 = r317140 * r317140;
double r317142 = r317139 * r317141;
double r317143 = r317138 - r317142;
double r317144 = r317141 - r317138;
double r317145 = r317143 / r317144;
double r317146 = acos(r317145);
return r317146;
}
double f(double v) {
double r317147 = 1.0;
double r317148 = 5.0;
double r317149 = v;
double r317150 = r317149 * r317149;
double r317151 = r317148 * r317150;
double r317152 = r317147 - r317151;
double r317153 = exp(r317152);
double r317154 = log(r317153);
double r317155 = r317150 - r317147;
double r317156 = r317154 / r317155;
double r317157 = acos(r317156);
return r317157;
}



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
(FPCore (v)
:name "Falkner and Boettcher, Appendix B, 1"
:precision binary64
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1))))