diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index bd6961623..a428af6de 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -246,7 +246,8 @@ module Make (Dom : Domain_sig.Dom) = struct
     let Llair.{callee; args; areturn; return; recursive} = call in
     let Llair.{name; params; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var]
+      pf "%a from %a with state %a" Var.pp name.var Var.pp
+        return.dst.parent.name.var Dom.pp state]
     ;
     let dnf_states =
       if opts.function_summaries then Dom.dnf state else [state]
@@ -278,7 +279,10 @@ module Make (Dom : Domain_sig.Dom) = struct
                 with
               | Some stk ->
                   Work.add stk ~prev:block ~retreating:recursive state entry
-              | None -> Work.skip )
+              | None -> (
+                match Dom.recursion_beyond_bound with
+                | `skip -> Work.seq acc (exec_jump stk state block return)
+                | `prune -> Work.skip ) )
         | Some post -> Work.seq acc (exec_jump stk post block return) )
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
@@ -293,7 +297,8 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp globals =
     let Llair.{name; params; freturn; locals} = block.parent in
-    [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var]
+    [%Trace.call fun {pf} ->
+      pf "from %a with pre_state %a" Var.pp name.var Dom.pp pre_state]
     ;
     ( match Stack.pop_return stk with
     | Some (from_call, retn_site, stk) ->
diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml
index a645dcdde..90894d8bf 100644
--- a/sledge/src/domain/domain_sig.ml
+++ b/sledge/src/domain/domain_sig.ml
@@ -39,6 +39,7 @@ module type Dom = sig
     -> t
     -> t * from_call
 
+  val recursion_beyond_bound : [`skip | `prune]
   val post : Var.Set.t -> from_call -> t -> t
   val retn : Var.t list -> Var.t option -> from_call -> t -> t
   val dnf : t -> t list
diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml
index 2834c38a4..6e7d68485 100644
--- a/sledge/src/domain/relation.ml
+++ b/sledge/src/domain/relation.ml
@@ -67,6 +67,8 @@ module Make (State_domain : State_domain_sig) = struct
     {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
   [@@deriving sexp_of]
 
+  let recursion_beyond_bound = State_domain.recursion_beyond_bound
+
   let call ~summaries actuals areturn formals locals globals_vec
       (entry, current) =
     let globals =
diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml
index 660c1fe21..990932a8b 100644
--- a/sledge/src/domain/unit.ml
+++ b/sledge/src/domain/unit.ml
@@ -23,6 +23,7 @@ let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None
 type from_call = unit [@@deriving compare, equal, sexp]
 
 let call ~summaries:_ _ _ _ _ _ _ = ((), ())
+let recursion_beyond_bound = `skip
 let post _ _ () = ()
 let retn _ _ _ _ = ()
 let dnf () = [()]
diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml
index 68e7f3966..c2fb0413a 100644
--- a/sledge/src/domain/used_globals.ml
+++ b/sledge/src/domain/used_globals.ml
@@ -19,6 +19,7 @@ let init globals =
   empty
 
 let join = Set.union
+let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
 let retn _ _ from_call post = Set.union from_call post
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index 5024c005a..7749970c4 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -125,6 +125,8 @@ let call ~summaries actuals areturn formals locals globals_vec q =
     pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
       q']
 
+let recursion_beyond_bound = `prune
+
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals _ q =
   [%Trace.call fun {pf} ->
diff --git a/sledge/test/exec/nonreducible_call_graph.c b/sledge/test/exec/nonreducible_call_graph.c
new file mode 100644
index 000000000..b64dbf504
--- /dev/null
+++ b/sledge/test/exec/nonreducible_call_graph.c
@@ -0,0 +1,36 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdio.h>
+
+char* a = "I'm a string";
+char* b = "I'm a different string";
+char* c = "foo bar";
+char* d = "hello world";
+FILE* file;
+
+void f();
+void g();
+
+int main() {        // accesses: a,b,c,d
+  if (getc(file)) { // nondeterministic
+    f();
+  } else {
+    g();
+  }
+  char* s = a;
+  return 0;
+}
+
+void f() { // accesses: b, c, d
+  char* s1 = b;
+  g();
+  char* s2 = c;
+}
+void g() { // accesses: b, c, d
+  char* s = d;
+  f();
+}