From 0f060b17799a332aa6f14f500f9b637852f56b2f Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 6 Nov 2020 06:15:28 -0800
Subject: [PATCH] [sledge] Fix Sh.star when formulas can be false without unsat
 context

Summary:
Since Context treats only equality directly, formulas involving other
literals can normalize to false when the context is not unsat. This
diff changes Sh.star to check this case, and return the canonical
false symbolic heap.

Reviewed By: da319

Differential Revision: D24746227

fbshipit-source-id: 50a51b8a6
---
 sledge/src/sh.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 6543f5181..1b07d3262 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -467,13 +467,15 @@ let star q1 q2 =
       let xs, ctx =
         Context.union (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
       in
-      if Context.is_unsat ctx then false_ us
+      let pure = Formula.and_ p1 p2 in
+      if Formula.equal Formula.ff pure || Context.is_unsat ctx then
+        false_ us
       else
         exists_fresh xs
           { us
           ; xs= Var.Set.union xs1 xs2
           ; ctx
-          ; pure= Formula.and_ p1 p2
+          ; pure
           ; heap= List.append h1 h2
           ; djns= List.append d1 d2 } )
   |>