Check the tree-like invariant in PLE.

ucsd-progsys · Oct 23, 2021 · a0f2dc9 · a0f2dc9
1 parent 8b1b48b
commit a0f2dc9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs
@@ -327,7 +327,7 @@ updCtxRes res iMb ctx = (ctx, res')
 
 
 updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
-updRes res (Just i) e = M.insert i e res 
+updRes res (Just i) e = M.insertWith (error "tree-like invariant broken in ple. See https://github.com/ucsd-progsys/liquid-fixpoint/issues/496") i e res
 updRes res  Nothing _ = res 
 
 ----------------------------------------------------------------------------------------------