Error

Derivation

1. Initial program 0.4

   \[\frac{x \cdot y - 1}{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - 1}\]
2. Using strategy rm

3. Applied square-unmult 0.4

   \[\leadsto \frac{x \cdot y - 1}{\color{blue}{{\left(x \cdot y\right)}^2} - 1}\]

4. Applied difference-of-sqr-1 0.4

   \[\leadsto \frac{x \cdot y - 1}{\color{blue}{\left(x \cdot y + 1\right) \cdot \left(x \cdot y - 1\right)}}\]

5. Applied *-un-lft-identity 0.4

   \[\leadsto \frac{\color{blue}{1 \cdot \left(x \cdot y - 1\right)}}{\left(x \cdot y + 1\right) \cdot \left(x \cdot y - 1\right)}\]

6. Applied times-frac 0.3

   \[\leadsto \color{blue}{\frac{1}{x \cdot y + 1} \cdot \frac{x \cdot y - 1}{x \cdot y - 1}}\]

7. Applied simplify 0.3

   \[\leadsto \frac{1}{x \cdot y + 1} \cdot \color{blue}{1}\]
8. Removed slow pow expressions

Runtime

Time bar (total: 17.4s) Debug log

Please include this information when filing a bug report:

herbie shell --seed '#(3052192724 3812927732 3686175817 630908657 2373248591 511094450)'
(FPCore (x y)
  :name "sec4-example"
  :pre (and (<= 1.001 x 2) (<= 1.001 y 2))
  (/ (- (* x y) 1) (- (* (* x y) (* x y)) 1)))