[sledge] [solver] Strengthen handling of existential subtrahends

Summary:
A frame inference query `Minuend ⊢ ∃xs. Subtrahend` returns a
`∃zs. Remainder` formula such that `Minuend ⊢ ∃xs. Subtrahend *
∃zs. Remainder` when successful. Currently if the subtrahend is itself
existentially quantified, its existentials are treated trivially: they
must witness themselves. This diff allows the solver to find witnesses
as the `xs`. They are still existentially quantified in the remainder,
so clients that need to constrain them should still name them before
calling the solver.

Reviewed By: kren1

Differential Revision: D16269630

fbshipit-source-id: 65136edd1

sledge/src/symbheap/solver.ml

@@ -605,9 +605,9 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
           [%Trace.info "@[<2>subtrahend@ %a@]" Sh.pp sub] ;
           let sub = Sh.extend_us us sub in
           let ws, sub = Sh.bind_exists sub ~wrt:xs in
+          let xs = Set.union xs ws in
           let sub = Sh.and_cong min.cong sub in
           let zs = Var.Set.empty in
-          let min = Sh.extend_us ws min in
           excise {us; com; min; xs; sub; zs; pgs= true}
           >>| fun remainder -> Sh.exists (Set.union ys ws) remainder )
       >>| fun remainder -> Sh.or_ remainders remainder )