\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\left(\left(-t1\right) \cdot \frac{1}{t1 + u}\right) \cdot \frac{v}{t1 + u}double f(double u, double v, double t1) {
double r29896 = t1;
double r29897 = -r29896;
double r29898 = v;
double r29899 = r29897 * r29898;
double r29900 = u;
double r29901 = r29896 + r29900;
double r29902 = r29901 * r29901;
double r29903 = r29899 / r29902;
return r29903;
}
double f(double u, double v, double t1) {
double r29904 = t1;
double r29905 = -r29904;
double r29906 = 1.0;
double r29907 = u;
double r29908 = r29904 + r29907;
double r29909 = r29906 / r29908;
double r29910 = r29905 * r29909;
double r29911 = v;
double r29912 = r29911 / r29908;
double r29913 = r29910 * r29912;
return r29913;
}



Bits error versus u



Bits error versus v



Bits error versus t1
Results
Initial program 18.2
rmApplied times-frac1.2
rmApplied div-inv1.3
Final simplification1.3
herbie shell --seed 2019350 +o rules:numerics
(FPCore (u v t1)
:name "Rosa's DopplerBench"
:precision binary64
(/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))