Exception for Migdal et al, Equation (64)

Math

\[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]

FPCore

(FPCore (a1 a2 th)
 :precision binary64
 (+
  (* (/ (cos th) (sqrt 2.0)) (* a1 a1))
  (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))

C

double code(double a1, double a2, double th) {
	return ((cos(th) / sqrt(2.0)) * (a1 * a1)) + ((cos(th) / sqrt(2.0)) * (a2 * a2));
}

Reproduce

Please include this information when filing a bug report:

herbie shell --seed 2021060 
(FPCore (a1 a2 th)
  :name "Migdal et al, Equation (64)"
  :precision binary64
  (+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))

Backtrace

Failed to produce proof for (/.f64 (/.f64 (*.f64 (cbrt.f64 (+.f64 (*.f64 a2 a2) (*.f64 a1 a1))) (cbrt.f64 (+.f64 (*.f64 a2 a2) (*.f64 a1 a1)))) (*.f64 (cbrt.f64 (sqrt.f64 (sqrt.f64 2))) (cbrt.f64 (sqrt.f64 (sqrt.f64 2))))) (*.f64 (cbrt.f64 (sqrt.f64 (sqrt.f64 2))) (cbrt.f64 (sqrt.f64 (sqrt.f64 2))))) to (/.f64 (*.f64 (cbrt.f64 (+.f64 (*.f64 a1 a1) (*.f64 a2 a2))) (cbrt.f64 (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))) (*.f64 (sqrt.f64 (sqrt.f64 2)) (cbrt.f64 (sqrt.f64 (sqrt.f64 2)))))		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
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