diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index f328d9fd1..ea16f52ad 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -255,7 +255,7 @@ module PulseTransferFunctions = struct
     (astates, ret_vars)
 
 
-  let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
+  let exec_instr_aux (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
       _cfg_node (instr : Sil.instr) : Domain.t list =
     match astate with
     | AbortProgram _ | LatentAbortProgram _ ->
@@ -345,6 +345,13 @@ module PulseTransferFunctions = struct
           [Domain.ContinueProgram astate] )
 
 
+  let exec_instr astate analysis_data cfg_node instr =
+    (* Sometimes instead of stopping on contradictions a false path condition is recorded
+       instead. Prune these early here so they don't spuriously count towards the disjunct limit. *)
+    exec_instr_aux astate analysis_data cfg_node instr
+    |> List.filter ~f:(fun exec_state -> not (Domain.is_unsat_cheap exec_state))
+
+
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
 end
 
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index 8b21d4ce6..f00de15a2 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -59,6 +59,17 @@ let pp fmt = function
         (astate :> AbductiveDomain.t)
 
 
+(* do not export this function as there lies wickedness: clients should generally care about what
+   kind of state they are manipulating so let's not encourage them not to *)
+let get_astate : t -> AbductiveDomain.t = function
+  | ContinueProgram astate ->
+      astate
+  | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} ->
+      (astate :> AbductiveDomain.t)
+
+
+let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition
+
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
 let summary_of_posts pdesc posts =
diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli
index df2a4c30b..cbf7e9978 100644
--- a/infer/src/pulse/PulseExecutionDomain.mli
+++ b/infer/src/pulse/PulseExecutionDomain.mli
@@ -26,6 +26,9 @@ val continue : AbductiveDomain.t -> t
 
 val mk_initial : Procdesc.t -> t
 
+val is_unsat_cheap : t -> bool
+(** see {!PulsePathCondition.is_unsat_cheap} *)
+
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
 val summary_of_posts : Procdesc.t -> t list -> summary list