From ae8cd953f819a585e29d662ca619fea2920ddc51 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 2 Mar 2020 08:43:22 -0800 Subject: [PATCH] [sledge] Fix potential unsyncing of var contexts in solver Summary: Handle the case the universal context of a goal does not stay in sync with that of the minuend. The need for this indicates that there is some problematic redundancy in the representation of solver goals. Reviewed By: ngorogiannis Differential Revision: D20120268 fbshipit-source-id: 44a4d6260 --- sledge/src/symbheap/solver.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 40984a749..b33a5d083 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -560,11 +560,12 @@ let excise_heap ({min; sub} as goal) = | Some goal -> Some {goal with pgs= true} | None -> Some goal -let rec excise ({min; xs; sub; zs; pgs} as goal) = +let rec excise ({us; min; xs; sub; zs; pgs} as goal) = [%Trace.info "@[<2>excise@ %a@]" pp goal] ; if Sh.is_false min then Some (Sh.false_ (Set.diff (Set.union min.us xs) zs)) - else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min)) + else if Sh.is_emp sub then + Some (Sh.exists zs (Sh.extend_us (Set.union us xs) min)) else if Sh.is_false sub then None else if pgs then {goal with pgs= false} |> excise_exists |> excise_pure >>= excise_heap