\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 r32085 = t1;
double r32086 = -r32085;
double r32087 = v;
double r32088 = r32086 * r32087;
double r32089 = u;
double r32090 = r32085 + r32089;
double r32091 = r32090 * r32090;
double r32092 = r32088 / r32091;
return r32092;
}
double f(double u, double v, double t1) {
double r32093 = t1;
double r32094 = -r32093;
double r32095 = 1.0;
double r32096 = u;
double r32097 = r32093 + r32096;
double r32098 = r32095 / r32097;
double r32099 = r32094 * r32098;
double r32100 = v;
double r32101 = r32100 / r32097;
double r32102 = r32099 * r32101;
return r32102;
}



Bits error versus u



Bits error versus v



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