Average Error: 52.4 → 1.5
Time: 13.6s
Precision: binary64
\[\left(\left(4.930380657631324 \cdot 10^{-32} < a \land a < 2.028240960365167 \cdot 10^{+31}\right) \land \left(4.930380657631324 \cdot 10^{-32} < b \land b < 2.028240960365167 \cdot 10^{+31}\right)\right) \land \left(4.930380657631324 \cdot 10^{-32} < c \land c < 2.028240960365167 \cdot 10^{+31}\right)\]
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a} \]
↓
\[\left(\frac{{c}^{3}}{{b}^{5}} \cdot \left(a \cdot a\right)\right) \cdot -2 - \mathsf{fma}\left(5, \frac{{c}^{4}}{\frac{{b}^{7}}{{a}^{3}}}, \frac{c}{b} + a \cdot \frac{c \cdot c}{{b}^{3}}\right) \]
\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
↓
\left(\frac{{c}^{3}}{{b}^{5}} \cdot \left(a \cdot a\right)\right) \cdot -2 - \mathsf{fma}\left(5, \frac{{c}^{4}}{\frac{{b}^{7}}{{a}^{3}}}, \frac{c}{b} + a \cdot \frac{c \cdot c}{{b}^{3}}\right)

(FPCore (a b c)
 :precision binary64
 (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))
↓
(FPCore (a b c)
 :precision binary64
 (-
  (* (* (/ (pow c 3.0) (pow b 5.0)) (* a a)) -2.0)
  (fma
   5.0
   (/ (pow c 4.0) (/ (pow b 7.0) (pow a 3.0)))
   (+ (/ c b) (* a (/ (* c c) (pow b 3.0)))))))
double code(double a, double b, double c) {
	return (-b + sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
↓
double code(double a, double b, double c) {
	return (((pow(c, 3.0) / pow(b, 5.0)) * (a * a)) * -2.0) - fma(5.0, (pow(c, 4.0) / (pow(b, 7.0) / pow(a, 3.0))), ((c / b) + (a * ((c * c) / pow(b, 3.0)))));
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 52.4

    \[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a} \]

  2. Simplified52.4

    \[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -4\right)\right)} - b\right) \cdot \frac{0.5}{a}} \]
    Proof
    (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite=> sub0-neg_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)): 0 points increase in error, 0 points decrease in error
    (Rewrite=> associate-/l*_binary64 (/.f64 -1 (/.f64 (*.f64 2 a) (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 6 points increase in error, 6 points decrease in error
    (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 -1 (*.f64 2 a)) (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))): 12 points increase in error, 10 points decrease in error
    (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b)) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) b) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) b))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (neg.f64 b)))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (Rewrite=> sub0-neg_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 0 (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) -1))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 0 (*.f64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) -1))) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 0 (*.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) -1)) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 0 (*.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) -1)) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 0 (*.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) -1)) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> +-lft-identity_binary64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) -1)) (/.f64 -1 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> associate-*l*_binary64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> sub0-neg_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (neg.f64 (Rewrite=> sub-neg_binary64 (+.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (neg.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (neg.f64 (+.f64 (neg.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0))) b)) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (neg.f64 (+.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (neg.f64 0))) b)) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (neg.f64 (+.f64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite=> metadata-eval 0)) b)) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (neg.f64 (Rewrite=> associate-+l+_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (+.f64 0 b)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (neg.f64 (+.f64 0 b)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite=> remove-double-neg_binary64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (neg.f64 (neg.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0)))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (neg.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (neg.f64 0)))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (neg.f64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite=> metadata-eval 0))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (neg.f64 0))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (+.f64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (Rewrite=> metadata-eval 0)) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (+.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) 0) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite=> fma-def_binary64 (fma.f64 -1 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) 0)) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (fma.f64 -1 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= metadata-eval (neg.f64 0))) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 -1 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) 0)) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) 0) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (Rewrite=> remove-double-neg_binary64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) 0) (neg.f64 (+.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (neg.f64 (Rewrite=> +-lft-identity_binary64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (neg.f64 (Rewrite<= --rgt-identity_binary64 (-.f64 b 0)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b 0)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) 0))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) 0)) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (Rewrite<= +-commutative_binary64 (+.f64 0 (neg.f64 b)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (Rewrite<= sub-neg_binary64 (-.f64 0 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (+.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) 0) (Rewrite<= neg-sub0_binary64 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite=> associate-+l-_binary64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (-.f64 0 (neg.f64 b)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 b b) (neg.f64 (*.f64 (*.f64 4 a) c))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 (*.f64 4 a) c)) (*.f64 b b)))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 (*.f64 4 a) c))) (*.f64 b b))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (*.f64 (*.f64 4 a) c) (*.f64 b b))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (-.f64 0 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 (*.f64 4 a) c) (neg.f64 (*.f64 b b)))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (-.f64 0 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 b b)) (*.f64 (*.f64 4 a) c))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (Rewrite=> associate--r+_binary64 (-.f64 (-.f64 0 (neg.f64 (*.f64 b b))) (*.f64 (*.f64 4 a) c)))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (-.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (neg.f64 (*.f64 b b)))) (*.f64 (*.f64 4 a) c))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (-.f64 (neg.f64 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 b (neg.f64 b)))) (*.f64 (*.f64 4 a) c))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (-.f64 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 b (neg.f64 (neg.f64 b)))) (*.f64 (*.f64 4 a) c))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (Rewrite=> fma-neg_binary64 (fma.f64 b (neg.f64 (neg.f64 b)) (neg.f64 (*.f64 (*.f64 4 a) c))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 6 points increase in error, 9 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b (neg.f64 (neg.f64 b)) (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (*.f64 4 a)) c)))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b (Rewrite=> remove-double-neg_binary64 b) (*.f64 (neg.f64 (*.f64 4 a)) c))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (*.f64 4 a) c))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 (*.f64 4 a) c))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (*.f64 4 a) c) -1)))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (Rewrite=> associate-*l*_binary64 (*.f64 4 (*.f64 a c))) -1))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 a c) 4)) -1))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (Rewrite=> associate-*l*_binary64 (*.f64 a (*.f64 c 4))) -1))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite=> associate-*l*_binary64 (*.f64 a (*.f64 (*.f64 c 4) -1))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (Rewrite<= *-commutative_binary64 (*.f64 -1 (*.f64 c 4)))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 c 4)))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 c (neg.f64 4)))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c (Rewrite=> metadata-eval -4))))) (-.f64 0 (neg.f64 b))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) (Rewrite<= neg-sub0_binary64 (neg.f64 (neg.f64 b)))) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) (Rewrite=> remove-double-neg_binary64 b)) (*.f64 -1 (/.f64 -1 (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 -1 (*.f64 2 a))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (neg.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 -1 2) a)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (Rewrite=> distribute-neg-frac_binary64 (/.f64 (neg.f64 (/.f64 -1 2)) a))): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (/.f64 (neg.f64 (Rewrite=> metadata-eval -1/2)) a)): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (/.f64 (Rewrite=> metadata-eval 1/2) a)): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) a)): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (/.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) 2) a)): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (/.f64 (/.f64 (Rewrite=> metadata-eval 1) 2) a)): 0 points increase in error, 0 points decrease in error
    (*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -4)))) b) (/.f64 (Rewrite=> metadata-eval 1/2) a)): 0 points increase in error, 0 points decrease in error

  3. Taylor expanded in b around inf 1.8

    \[\leadsto \color{blue}{\left(-\left(2 \cdot \frac{c \cdot a}{b} + \left(2 \cdot \frac{{c}^{2} \cdot {a}^{2}}{{b}^{3}} + \left(10 \cdot \frac{{c}^{4} \cdot {a}^{4}}{{b}^{7}} + 4 \cdot \frac{{c}^{3} \cdot {a}^{3}}{{b}^{5}}\right)\right)\right)\right)} \cdot \frac{0.5}{a} \]

  4. Taylor expanded in c around 0 1.5

    \[\leadsto \color{blue}{-\left(2 \cdot \frac{{c}^{3} \cdot {a}^{2}}{{b}^{5}} + \left(5 \cdot \frac{{c}^{4} \cdot {a}^{3}}{{b}^{7}} + \left(\frac{{c}^{2} \cdot a}{{b}^{3}} + \frac{c}{b}\right)\right)\right)} \]

  5. Simplified1.5

    \[\leadsto \color{blue}{\left(\frac{{c}^{3}}{{b}^{5}} \cdot \left(a \cdot a\right)\right) \cdot -2 - \mathsf{fma}\left(5, \frac{{c}^{4}}{\frac{{b}^{7}}{{a}^{3}}}, \frac{c}{b} + \frac{c \cdot c}{{b}^{3}} \cdot a\right)} \]
    Proof
    (neg.f64 (+.f64 (*.f64 2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b))))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (neg.f64 (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> unsub-neg_binary64 (-.f64 (neg.f64 (*.f64 2 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) 2))) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (neg.f64 2))) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (Rewrite=> associate-/l*_binary64 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (pow.f64 a 2)))) (neg.f64 2)) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (pow.f64 a 2))) (neg.f64 2)) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (Rewrite=> unpow2_binary64 (*.f64 a a))) (neg.f64 2)) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) (Rewrite=> metadata-eval -2)) (+.f64 (*.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) -2) (Rewrite=> fma-def_binary64 (fma.f64 5 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 3)) (pow.f64 b 7)) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) -2) (fma.f64 5 (Rewrite=> associate-/l*_binary64 (/.f64 (pow.f64 c 4) (/.f64 (pow.f64 b 7) (pow.f64 a 3)))) (+.f64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (/.f64 c b)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) -2) (fma.f64 5 (/.f64 (pow.f64 c 4) (/.f64 (pow.f64 b 7) (pow.f64 a 3))) (Rewrite=> +-commutative_binary64 (+.f64 (/.f64 c b) (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) -2) (fma.f64 5 (/.f64 (pow.f64 c 4) (/.f64 (pow.f64 b 7) (pow.f64 a 3))) (+.f64 (/.f64 c b) (Rewrite=> associate-/l*_binary64 (/.f64 (pow.f64 c 2) (/.f64 (pow.f64 b 3) a)))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) -2) (fma.f64 5 (/.f64 (pow.f64 c 4) (/.f64 (pow.f64 b 7) (pow.f64 a 3))) (+.f64 (/.f64 c b) (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 b 3)) a))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (*.f64 (/.f64 (pow.f64 c 3) (pow.f64 b 5)) (*.f64 a a)) -2) (fma.f64 5 (/.f64 (pow.f64 c 4) (/.f64 (pow.f64 b 7) (pow.f64 a 3))) (+.f64 (/.f64 c b) (*.f64 (/.f64 (Rewrite=> unpow2_binary64 (*.f64 c c)) (pow.f64 b 3)) a)))): 0 points increase in error, 0 points decrease in error

  6. Final simplification1.5

    \[\leadsto \left(\frac{{c}^{3}}{{b}^{5}} \cdot \left(a \cdot a\right)\right) \cdot -2 - \mathsf{fma}\left(5, \frac{{c}^{4}}{\frac{{b}^{7}}{{a}^{3}}}, \frac{c}{b} + a \cdot \frac{c \cdot c}{{b}^{3}}\right) \]

Reproduce

herbie shell --seed 2022160 
(FPCore (a b c)
  :name "Quadratic roots, wide range"
  :precision binary64
  :pre (and (and (and (< 4.930380657631324e-32 a) (< a 2.028240960365167e+31)) (and (< 4.930380657631324e-32 b) (< b 2.028240960365167e+31))) (and (< 4.930380657631324e-32 c) (< c 2.028240960365167e+31)))
  (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))