From f80e0977cd59b160dee2d019ef88b8207cf8cfe0 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 10 Mar 2020 02:21:02 -0700
Subject: [PATCH] [sledge] Make Sh.and_cong robust wrt conjoining to an unsat
 formula

Reviewed By: jvillard

Differential Revision: D20303063

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

diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index d3125dfde..5f339b70b 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -422,7 +422,9 @@ let and_cong_ cong q =
 let and_cong cong q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Equality.pp cong pp q]
   ;
-  and_cong_ cong (extend_us (Equality.fv cong) q)
+  ( match q.djns with
+  | [[]] -> q
+  | _ -> and_cong_ cong (extend_us (Equality.fv cong) q) )
   |>
   [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]