Unfold with undecided guards in PLE when new equalities are discovered

src/Language/Fixpoint/Solver/PLE.hs

@@ -942,15 +942,18 @@ evalApp γ ctx e0 es et
                     then elaborateExpr "EvalApp unfold full: " newE 
                     else pure newE
 
-         (e', fe) <- evalIte γ ctx et newE'        -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
+         (newEqs1, (e', fe)) <- collectNewEqualities $ evalIte γ ctx et newE' -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
+
          let e2' = stripPLEUnfold e'
          let e3' = simplify γ ctx (eApps e2' es2)  -- reduces a bit the equations
-
-         if hasUndecidedGuard e' then do
-           -- Don't unfold the expression if there is an if-then-else
-           -- guarding it, just to preserve the size of further
-           -- rewrites.
-           modify $ \st -> st 
+             noNewEqualities = S.null newEqs1
+
+         if hasUndecidedGuard e' && noNewEqualities then do
+           -- Don't unfold the expression if there is an if-then-else guarding
+           -- it, just to preserve the size of further rewrites.
+           -- If there are new equalities, after evaluating however, we do
+           -- unfold in order to allow analisis of the resulting expression.
+           modify $ \st -> st
              { evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)
              }
            return (Nothing, noExpand)
@@ -978,6 +981,14 @@ evalApp γ ctx e0 es et
     hasUndecidedGuard EIte{} = True
     hasUndecidedGuard _ = False
 
+    collectNewEqualities :: EvalST a -> EvalST (EvEqualities, a)
+    collectNewEqualities m = do
+      newEqs0 <- state $ \st -> (evNewEqualities st, st { evNewEqualities = S.empty })
+      r <- m
+      newEqs1 <- state $ \st ->
+        (evNewEqualities st, st { evNewEqualities = S.union (evNewEqualities st) newEqs0 })
+      return (newEqs1, r)
+
 evalApp γ ctx e0 args@(e:es) _
   | EVar f <- dropECst e0
   , (d, as) <- splitEAppThroughECst e

tests/proof/ple_guards.fq

@@ -0,0 +1,22 @@
+// minimal reproduction of LH #1409. UNSAFE with --rewrite; SAFE with --rewrite --noincrple 
+fixpoint "--rewrite"
+fixpoint "--save"
+
+expand [1: True]
+
+constant add1 : (func(0 , [int; int]))
+constant add2 : (func(0 , [int; int]))
+constant sel : (func(0 , [int; int]))
+
+define add1 (x : int) : int = { x + 1 }
+define add2 (x : int) : int = { add1 (add1 x) }
+define sel (x : int) : int = { if ((add2 x) = (x + 2)) then 0 else 1 }
+
+bind 0 t : {v: int   |   true  }
+bind 1 t2 : {v: int   |  true }
+
+constraint:
+  env [0;1]
+  lhs {v : int | true }
+  rhs {v : int | sel 1 = 0 }
+  id 1 tag []