From f8f47c07551e0643a27bafac9b08006ec97ef5f5 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 6 Mar 2020 02:19:57 -0800
Subject: [PATCH] [sledge] Fix a few existential context fumbles

Summary:
In a few places, implicitly witnessed existential variables could
remain in the existential context. This led to weakness in the solver,
where occurrences bound by the existential context would be not known
to be constrained by their witnesses.

Reviewed By: jvillard

Differential Revision: D20248542

fbshipit-source-id: 44f62839c
---
 sledge/src/symbheap/solver.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index d56cfc422..208240656 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -199,6 +199,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   let o_n = Term.integer o_n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
+  let xs = Set.diff xs (Term.fv n) in
   let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
   let min =
     Sh.and_
@@ -212,7 +213,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
       (Sh.and_ (Term.eq m m')
          (Sh.and_ (Term.eq a0 a') (Sh.rem_seg ssg sub)))
   in
-  goal |> with_ ~us ~com ~min ~sub ~zs
+  goal |> with_ ~us ~com ~min ~xs ~sub ~zs
 
 (*   [k; o)
  * ⊢ [l;   n)
@@ -274,6 +275,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let l_k = Term.integer l_k in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
+  let xs = Set.diff xs (Term.fv n) in
   let com =
     Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
   in
@@ -289,7 +291,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       (Sh.and_ (Term.eq m m')
          (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub)))
   in
-  goal |> with_ ~us ~com ~min ~sub ~zs
+  goal |> with_ ~us ~com ~min ~xs ~sub ~zs
 
 (*   [k;      o)
  * ⊢    [l; n)
@@ -318,6 +320,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
+  let xs = Set.diff xs (Set.union (Term.fv l) (Term.fv n)) in
   let com =
     Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
   in
@@ -335,7 +338,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       (Sh.and_ (Term.eq m m')
          (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub)))
   in
-  goal |> with_ ~us ~com ~min ~sub ~zs
+  goal |> with_ ~us ~com ~min ~xs ~sub ~zs
 
 (*   [k;   o)
  * ⊢    [l;  n)
@@ -365,6 +368,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
+  let xs = Set.diff xs (Term.fv l) in
   let com =
     Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; arr= a1}) com
   in