Average Error: 0.2 → 0.2
Time: 56.3s
Precision: 64
\[\left(0\right) \lt a \land \left(0\right) \lt b \land \left(0\right) \lt c\]
\[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
↓
\[\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + c}}\]
\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}
↓
\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + c}}
double f(double a, double b, double c) {
        double r5338427 = a;
        double r5338428 = b;
        double r5338429 = r5338427 + r5338428;
        double r5338430 = c;
        double r5338431 = r5338429 + r5338430;
        double r5338432 = 2.0;
        double r5338433 = /* ERROR: no posit support in C */;
        double r5338434 = r5338431 / r5338433;
        double r5338435 = r5338434 - r5338427;
        double r5338436 = r5338434 * r5338435;
        double r5338437 = r5338434 - r5338428;
        double r5338438 = r5338436 * r5338437;
        double r5338439 = r5338434 - r5338430;
        double r5338440 = r5338438 * r5338439;
        double r5338441 = sqrt(r5338440);
        return r5338441;
}
↓
double f(double a, double b, double c) {
        double r5338442 = a;
        double r5338443 = b;
        double r5338444 = r5338442 + r5338443;
        double r5338445 = c;
        double r5338446 = r5338444 + r5338445;
        double r5338447 = 2.0;
        double r5338448 = r5338446 / r5338447;
        double r5338449 = r5338448 - r5338442;
        double r5338450 = r5338448 * r5338449;
        double r5338451 = r5338448 - r5338443;
        double r5338452 = r5338450 * r5338451;
        double r5338453 = r5338448 * r5338448;
        double r5338454 = r5338445 * r5338445;
        double r5338455 = r5338453 - r5338454;
        double r5338456 = r5338448 + r5338445;
        double r5338457 = r5338455 / r5338456;
        double r5338458 = r5338452 * r5338457;
        double r5338459 = sqrt(r5338458);
        return r5338459;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 0.2

    \[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  2. Using strategy rm

  3. Applied p16-flip--0.2

    \[\leadsto \sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) - \left(c \cdot c\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{c}\right)}\right)}\right)}\]

  4. Final simplification0.2

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

Reproduce

herbie shell --seed 2019134 
(FPCore (a b c)
  :name "Area of a triangle"
  :pre (and (<.p16 (real->posit16 0) a) (<.p16 (real->posit16 0) b) (<.p16 (real->posit16 0) c))
  (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))