From 270b6003deeb8471212f4787d479fbb9835f1a6b Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 25 Feb 2019 07:07:54 -0800
Subject: [PATCH] [sledge] Revise excision of segments to witness existential
 size

Reviewed By: jvillard

Differential Revision: D14075517

fbshipit-source-id: a3d2e7fcf
---
 sledge/src/symbheap/solver.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index 3f2d82534..98e96e042 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -504,7 +504,7 @@ let excise_seg ({sub} as goal) msg ssg =
   (* k-l = 0 so k = l *)
   | 0 -> (
     match Congruence.difference sub.cong o n with
-    | None -> Some (excise_seg_same goal msg ssg)
+    | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
     | Some o_n -> (
       match[@warning "-p"] Z.sign o_n with
       (* o-n < 0      [k; o)