From 77c630b7f4c55396f56ab00489b80c400b703daa Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 2 Dec 2020 13:49:48 -0800
Subject: [PATCH] [sledge] Normalize pure constraints when conjoining to a
 symbolic heap

Reviewed By: jvillard

Differential Revision: D25196729

fbshipit-source-id: fc289d811
---
 sledge/src/sh.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 78556f5ab..d6bb98f19 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -531,7 +531,8 @@ let pure (p : Formula.t) =
     pf "%a" pp q ;
     invariant q]
 
-let and_ e q = star (pure e) q
+let and_ b q =
+  star (pure (Formula.map_terms ~f:(Context.normalize q.ctx) b)) q
 
 let and_subst subst q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Context.Subst.pp subst pp q]