From a6f948c2c34d16c893f8cc5eba2eb41650fe236d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 2 Mar 2020 08:43:45 -0800
Subject: [PATCH] [sledge] Strengthen handling of existential segments

Summary:
Due to strengthened existential witnessing, the incomplete ad hoc
witness guessing is no longer needed.

Reviewed By: ngorogiannis

Differential Revision: D20120277

fbshipit-source-id: 8ee1656dd
---
 sledge/src/symbheap/solver.ml      | 6 ++----
 sledge/src/symbheap/solver_test.ml | 9 ++++++---
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index ba4486a8f..9a307a44c 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -498,9 +498,7 @@ let excise_seg ({sub} as goal) msg ssg =
         )
     (* k-l = 0 so k = l *)
     | Zero -> (
-      match Equality.difference sub.cong o n with
-      | None -> Some {goal with sub= Sh.and_ (Term.eq o n) goal.sub}
-      | Some o_n -> (
+        let* o_n = Equality.difference sub.cong o n in
         match Int.sign (Z.sign o_n) with
         (* o-n < 0      [k; o)
          * so o < n   ⊢ [l;   n) *)
@@ -510,7 +508,7 @@ let excise_seg ({sub} as goal) msg ssg =
         | Zero -> Some (excise_seg_same goal msg ssg)
         (* o-n > 0      [k;   o)
          * so o > n   ⊢ [l; n) *)
-        | Pos -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
+        | Pos -> Some (excise_seg_sub_prefix goal msg ssg o_n) )
     (* k-l > 0 so k > l *)
     | Pos -> (
         let ko = Term.add k o in
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index b84585040..b4e85b70f 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -194,8 +194,6 @@ let%test_module _ =
           ∧ 16 = %m_8 = %n_9
           ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
-    (* Incompleteness: changing the order of the subtrahend leads to
-       different existential instantiation, which fails *)
     let%expect_test _ =
       infer_frame
         (Sh.star
@@ -211,7 +209,12 @@ let%test_module _ =
             %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩
           \- ∃ %a_2, %m_8, %n_9 .
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
-        ) infer_frame: |}]
+        ) infer_frame:
+          ∃ %a0_10, %a1_11 .
+            %a_2 = %a0_10
+          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ 16 = %m_8 = %n_9
+          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star