unfold on undecied if guard

ucsd-progsys · Sep 25, 2024 · d521162 · d521162
1 parent 61150bb
commit d521162
Showing 1 changed file with 4 additions and 7 deletions.
diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs
@@ -829,13 +829,10 @@ evalApp γ ctx e0 es et
                 if undecidedGuards
                   then do
                     modify $ \st ->
-                      st {
-                        evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)
-                      }
-                    -- Don't unfold the expression if there is an if-then-else
-                    -- guarding it, just to preserve the size of further
-                    -- rewrites.
-                    return (Nothing, noExpand)
+                      st { evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)
+                         , evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)
+                         }
+                    return (Just $ eApps e2' es2, fe)
                   else do
                     useFuel f
                     modify $ \st ->