[sledge] Fix solver crash

Summary:
Fix a crash that occurs when subtrahend has an existential variable that
was renamed as in the test.

The crash is due to an assertion in `Sh.exists` that says only variables
in the vocabulary can be existentialy quantifed out.

The problem was `Sh.exists` call in Solver.ml:611. Where `ws`
(existentials of the subthrehend) are not present in the vocabulary of
the remainder. This is because remainder "inheirts" the vocabulary of
the minued.

This fix simply extends the vocabulary of minued with `ws`, which
means the remaainder has the correct vocabulary. This should have no
externally visible effect as `ws` are then existentialed out.

Another option would be to try to change all the `excise_seg` functions,
to keep the vocabulary, but that looked annoying to implement.

Reviewed By: jvillard

Differential Revision: D16201423

fbshipit-source-id: b88c3abc4

sledge/src/symbheap/solver.ml

@@ -606,6 +606,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
           let ws, sub = Sh.bind_exists sub ~wrt:xs 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 )

sledge/src/symbheap/solver_test.ml

@@ -88,6 +88,25 @@ let%test_module _ =
           \-   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
         ) infer_frame:   emp |}]
 
+    let%expect_test _ =
+      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; arr= a2} in
+      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in
+      let minued = Sh.star common seg1 in
+      let subtrahend =
+        Sh.and_ (Exp.eq m n)
+          (Sh.exists
+             (Var.Set.of_list [m_])
+             (Sh.extend_us (Var.Set.of_list [m_]) common))
+      in
+      infer_frame minued [n_; m_] subtrahend ;
+      [%expect
+        {|
+        ( infer_frame:
+            %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
+          \- ∃ %m_8, %n_9 .
+            ∃ %m_10 .   %m_8 = %n_9 ∧ %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
+        ) infer_frame: ∃ %m_10 .   %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ |}]
+
     let%expect_test _ =
       check_frame
         (Sh.star