diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 96d579f7b..d0475ea1b 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -407,6 +407,7 @@ let exec_term :
             | Some (Error ()) ->
                 Report.invalid_access_term (Domain.project state) block.term ;
                 Work.skip
+            | Some (Ok state) when Domain.is_false state -> Work.skip
             | Some (Ok state) -> exec_goto stk state block return
             | None when Llair.Func.is_undefined callee ->
                 exec_skip_func stk state block return
diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml
index 364e09205..f0bb550bd 100644
--- a/sledge/src/symbheap/domain.ml
+++ b/sledge/src/symbheap/domain.ml
@@ -22,6 +22,8 @@ let join (entry_a, current_a) (entry_b, current_b) =
   assert (State_domain.equal entry_b entry_a) ;
   (entry_a, State_domain.join current_a current_b)
 
+let is_false (_, curr) = State_domain.is_false curr
+
 let exec_assume (entry, current) cnd =
   match State_domain.exec_assume current cnd with
   | Some current -> Some (entry, current)
diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli
index 346cbd824..9fc792548 100644
--- a/sledge/src/symbheap/domain.mli
+++ b/sledge/src/symbheap/domain.mli
@@ -13,6 +13,7 @@ val project : t -> State_domain.t
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
+val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
 val exec_return : t -> Var.t -> Exp.t -> t
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index 9fdc5e93a..3738686e8 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -25,6 +25,7 @@ let init globals =
     | _ -> q )
 
 let join = Sh.or_
+let is_false = Sh.is_false
 let exec_assume = Exec.assume
 let exec_return = Exec.return
 let exec_inst = Exec.inst
diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli
index b283530e7..9517221e7 100644
--- a/sledge/src/symbheap/state_domain.mli
+++ b/sledge/src/symbheap/state_domain.mli
@@ -12,6 +12,7 @@ type t [@@deriving equal, sexp_of]
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
+val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
 val exec_return : t -> Var.t -> Exp.t -> t