\[10^{-150} < \left|x\right| \land \left|x\right| < 10^{+150}\]

\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]

\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}

(FPCore (p x)
 :precision binary64
 (sqrt (* 0.5 (+ 1.0 (/ x (sqrt (+ (* (* 4.0 p) p) (* x x))))))))

double code(double p, double x) {
	return sqrt(0.5 * (1.0 + (x / sqrt(((4.0 * p) * p) + (x * x)))));
}

Reproduce

Please include this information when filing a bug report:

herbie shell --seed 2021060 
(FPCore (p x)
  :name "Given's Rotation SVD example"
  :precision binary64
  :pre (< 1e-150 (fabs x) 1e+150)

  :herbie-target
  (sqrt (+ 0.5 (/ (copysign 0.5 x) (hypot 1.0 (/ (* 2.0 p) x)))))

  (sqrt (* 0.5 (+ 1.0 (/ x (sqrt (+ (* (* 4.0 p) p) (* x x))))))))

Backtrace

Failed to produce proof for (/.f64 (.f64 x x) 1) to (.f64 x x)		L	C
for-loop	/data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt	167	8
(unnamed)	/data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt	149	6
egraph-add-exprs	/data/pavpan/nightlies/herbie/egg-generate-proof/egg-herbie/main.rkt	154	0
with-egraph	/data/pavpan/nightlies/herbie/egg-generate-proof/egg-herbie/main.rkt	74	0
(unnamed)	/data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt	79	0
simplify!	/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt	236	0
run-iter!	/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt	360	0
for-loop	/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt	391	2
run-improve	/data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt	377	0
(unnamed)	/data/pavpan/nightlies/herbie/egg-generate-proof/src/sandbox.rkt	54	6
run	/opt/racket-7.9/share/pkgs/profile-lib/main.rkt	39	2
profile-thunk	/opt/racket-7.9/share/pkgs/profile-lib/main.rkt	9	0
(unnamed)	/opt/racket-7.9/collects/racket/engine.rkt	42	24