[sledge] Work harder to detect infeasible paths when executing assume

Summary:
Switch to a stronger but more expensive operation to check if a
symbolic heap is unsatisfiable.

Reviewed By: ngorogiannis

Differential Revision: D27564872

fbshipit-source-id: c8e306408

sledge/src/domain_sh.ml

@@ -46,7 +46,7 @@ let dnf = Sh.dnf
 let exec_assume q b =
   Exec.assume q (X.formula b)
   |> simplify
-  |> fun q -> if Sh.is_unsat q then None else Some q
+  |> fun q -> if Sh.is_unsat_dnf q then None else Some q
 
 let exec_kill r q = Exec.kill q (X.reg r) |> simplify
 

sledge/src/sh.mli

@@ -117,6 +117,10 @@ val is_unsat : t -> bool
 (** Holds only of inconsistent formulas, does not hold of all inconsistent
     formulas. *)
 
+val is_unsat_dnf : t -> bool
+(** Holds only of inconsistent formulas, does not hold of all inconsistent
+    formulas. Like [is_unsat] but more complete and expensive. *)
+
 val is_empty : t -> bool
 (** Holds only if all satisfying states have empty heap. *)