Average Error: 0.0 → 0.0
Time: 13.2s
Precision: 64
\[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
↓
\[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y
↓
\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y
double f(double x, double y) {
        double r408599 = x;
        double r408600 = r408599 * r408599;
        double r408601 = 2.0;
        double r408602 = r408599 * r408601;
        double r408603 = y;
        double r408604 = r408602 * r408603;
        double r408605 = r408600 + r408604;
        double r408606 = r408603 * r408603;
        double r408607 = r408605 + r408606;
        return r408607;
}
↓
double f(double x, double y) {
        double r408608 = x;
        double r408609 = r408608 * r408608;
        double r408610 = 2.0;
        double r408611 = r408608 * r408610;
        double r408612 = y;
        double r408613 = r408611 * r408612;
        double r408614 = r408609 + r408613;
        double r408615 = r408612 * r408612;
        double r408616 = r408614 + r408615;
        return r408616;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original0.0
Target0.0
Herbie0.0
\[x \cdot x + \left(y \cdot y + \left(x \cdot y\right) \cdot 2\right)\]

Derivation

  1. Initial program 0.0

    \[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]

  2. Final simplification0.0

    \[\leadsto \left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]

Reproduce

herbie shell --seed 2019323 
(FPCore (x y)
  :name "Examples.Basics.ProofTests:f4 from sbv-4.4"
  :precision binary64

  :herbie-target
  (+ (* x x) (+ (* y y) (* (* x y) 2)))

  (+ (+ (* x x) (* (* x 2) y)) (* y y)))