From 1881e990da37b724489e19ad9041acfbb060b34e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sat, 15 Aug 2020 02:18:59 -0700
Subject: [PATCH] [sledge] Change: Strengthen Sh.pure_approx with segment loc
 non-null

Reviewed By: jvillard

Differential Revision: D22571149

fbshipit-source-id: fca90beb9
---
 sledge/src/sh.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 9ed676237..4b18e279b 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -595,9 +595,13 @@ let rec is_empty q =
 
 let rec pure_approx q =
   Formula.andN
-    ( q.pure
-    :: List.map q.djns ~f:(fun djn ->
-           Formula.orN (List.map djn ~f:pure_approx) ) )
+    ( [q.pure]
+    |> fun init ->
+    List.fold ~init q.heap ~f:(fun p seg ->
+        Formula.dq Term.zero seg.loc :: p )
+    |> fun init ->
+    List.fold ~init q.djns ~f:(fun p djn ->
+        Formula.orN (List.map djn ~f:pure_approx) :: p ) )
 
 let pure_approx q =
   [%Trace.call fun {pf} -> pf "%a" pp q]