[sledge] Make Sh.and_cong robust wrt conjoining to an unsat formula

Reviewed By: jvillard Differential Revision: D20303063 fbshipit-source-id: f49f227f2
5 years ago · f80e0977cd
parent 37ddf95a49
commit f80e0977cd
1 changed files with 3 additions and 1 deletions
--- 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]