diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 2cee99739..f4318abcd 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -123,7 +123,7 @@ module PulseTransferFunctions = struct
         astate
 
 
-  let dispatch_call ({tenv; InterproceduralAnalysis.proc_desc} as analysis_data) ret call_exp
+  let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc} as analysis_data) ret call_exp
       actuals call_loc flags astate =
     (* evaluate all actuals *)
     let<*> astate, rev_func_args =
@@ -196,7 +196,7 @@ module PulseTransferFunctions = struct
           | Error _ as err ->
               Some err
           | Ok exec_state ->
-              ExecutionDomain.force_exit_program tenv proc_desc exec_state
+              PulseSummary.force_exit_program tenv proc_desc exec_state
               |> Option.map ~f:(fun exec_state -> Ok exec_state) )
     else exec_states_res
 
@@ -225,7 +225,8 @@ module PulseTransferFunctions = struct
      add and execute calls to dealloc. The main advantage of adding this calls
      is that some memory could be freed in dealloc, and we would be reporting a leak on it if we
      didn't call it. *)
-  let execute_injected_dealloc_calls analysis_data vars astate location =
+  let execute_injected_dealloc_calls
+      ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) vars astate location =
     let used_ids = Stack.keys astate |> List.filter_map ~f:(fun var -> Var.get_ident var) in
     Ident.update_name_generator used_ids ;
     let call_dealloc (astate_list : Domain.t list) (ret_id, id, typ, dealloc) =
@@ -243,7 +244,7 @@ module PulseTransferFunctions = struct
               [astate]
           | ContinueProgram astate ->
               dispatch_call analysis_data ret call_exp actuals location call_flags astate
-              |> PulseReport.report_exec_results analysis_data )
+              |> PulseReport.report_exec_results tenv proc_desc err_log )
     in
     let dynamic_types_unreachable =
       PulseOperations.get_dynamic_type_unreachable_values vars astate
@@ -258,8 +259,8 @@ module PulseTransferFunctions = struct
 
 
   let exec_instr_aux (astate : Domain.t)
-      ({tenv; InterproceduralAnalysis.proc_desc} as analysis_data) _cfg_node (instr : Sil.instr) :
-      Domain.t list =
+      ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node
+      (instr : Sil.instr) : Domain.t list =
     match astate with
     | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ ->
         (* We can also continue the analysis with the error state here
@@ -282,7 +283,7 @@ module PulseTransferFunctions = struct
               [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
                  PulseOperations.write_id lhs_id rhs_addr_hist astate) ]
           in
-          PulseReport.report_results analysis_data result
+          PulseReport.report_results tenv proc_desc err_log result
       | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
           (* [*lhs_exp := rhs_exp] *)
           let event = ValueHistory.Assignment loc in
@@ -326,7 +327,7 @@ module PulseTransferFunctions = struct
             | _ ->
                 astates
           in
-          PulseReport.report_results analysis_data result
+          PulseReport.report_results tenv proc_desc err_log result
       | Prune (condition, loc, _is_then_branch, _if_kind) ->
           (let<*> astate = PulseOperations.prune loc ~condition astate in
            if PulseArithmetic.is_unsat_cheap astate then
@@ -335,10 +336,10 @@ module PulseTransferFunctions = struct
            else
              (* [condition] is true or unknown value: go into the branch *)
              [Ok (ContinueProgram astate)])
-          |> PulseReport.report_exec_results analysis_data
+          |> PulseReport.report_exec_results tenv proc_desc err_log
       | Call (ret, call_exp, actuals, loc, call_flags) ->
           dispatch_call analysis_data ret call_exp actuals loc call_flags astate
-          |> PulseReport.report_exec_results analysis_data
+          |> PulseReport.report_exec_results tenv proc_desc err_log
       | Metadata (ExitScope (vars, location)) ->
           let remove_vars vars astates =
             List.concat_map astates ~f:(fun (astate : Domain.t) ->
@@ -347,7 +348,7 @@ module PulseTransferFunctions = struct
                     [astate]
                 | ContinueProgram astate ->
                     PulseOperations.remove_vars tenv vars location astate
-                    |> PulseReport.report_result analysis_data )
+                    |> PulseReport.report_result tenv proc_desc err_log )
           in
           if Procname.is_java (Procdesc.get_proc_name proc_desc) then
             remove_vars vars [ContinueProgram astate]
@@ -404,7 +405,7 @@ let with_debug_exit_node proc_desc ~f =
     ~f
 
 
-let checker ({tenv; InterproceduralAnalysis.proc_desc; err_log} as analysis_data) =
+let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) =
   AbstractValue.State.reset () ;
   let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
   let initial = [initial_astate] in
diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml
index 41f82d3aa..c5c804eb1 100644
--- a/infer/src/pulse/PulseAccessResult.ml
+++ b/infer/src/pulse/PulseAccessResult.ml
@@ -16,13 +16,3 @@ type 'astate error =
 type ('a, 'astate) base_t = ('a, 'astate error) result
 
 type 'a t = ('a, AbductiveDomain.t) base_t
-
-let to_summary tenv proc_desc error =
-  let open SatUnsat.Import in
-  match error with
-  | ReportableError {astate; diagnostic} ->
-      let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in
-      ReportableError {astate; diagnostic}
-  | ISLError astate ->
-      let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in
-      ISLError astate
diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli
deleted file mode 100644
index 0719d34e6..000000000
--- a/infer/src/pulse/PulseAccessResult.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(*
- * 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.
- *)
-
-open! IStd
-open PulseBasicInterface
-module AbductiveDomain = PulseAbductiveDomain
-
-type 'astate error =
-  | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
-  | ISLError of 'astate
-
-type ('a, 'astate) base_t = ('a, 'astate error) result
-
-type 'a t = ('a, AbductiveDomain.t) base_t
-
-val to_summary :
-  Tenv.t -> Procdesc.t -> AbductiveDomain.t error -> AbductiveDomain.summary error SatUnsat.t
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index 86810e033..02ca1349e 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -7,7 +7,6 @@
 
 open! IStd
 module F = Format
-module L = Logging
 open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 module LatentIssue = PulseLatentIssue
@@ -81,31 +80,3 @@ let get_astate : t -> AbductiveDomain.t = function
 let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition
 
 type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
-
-let summary_of_post_common tenv ~continue_program proc_desc = function
-  | ContinueProgram astate -> (
-    match AbductiveDomain.summary_of_post tenv proc_desc astate with
-    | Unsat ->
-        None
-    | Sat astate ->
-        Some (continue_program astate) )
-  (* already a summary but need to reconstruct the variants to make the type system happy *)
-  | AbortProgram astate ->
-      Some (AbortProgram astate)
-  | ExitProgram astate ->
-      Some (ExitProgram astate)
-  | LatentAbortProgram {astate; latent_issue} ->
-      Some (LatentAbortProgram {astate; latent_issue})
-  | ISLLatentMemoryError astate ->
-      Some (ISLLatentMemoryError astate)
-
-
-let summary_of_posts tenv proc_desc posts =
-  List.filter_mapi posts ~f:(fun i exec_state ->
-      L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
-      summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate ->
-          ContinueProgram astate ) )
-
-
-let force_exit_program tenv proc_desc post =
-  summary_of_post_common tenv proc_desc post ~continue_program:(fun astate -> ExitProgram astate)
diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli
index 8a642a794..e6fb02394 100644
--- a/infer/src/pulse/PulseExecutionDomain.mli
+++ b/infer/src/pulse/PulseExecutionDomain.mli
@@ -33,7 +33,3 @@ val is_unsat_cheap : t -> bool
 (** see {!PulsePathCondition.is_unsat_cheap} *)
 
 type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
-
-val summary_of_posts : Tenv.t -> Procdesc.t -> t list -> summary list
-
-val force_exit_program : Tenv.t -> Procdesc.t -> t -> t option
diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml
index 04d3014ef..a12379cf6 100644
--- a/infer/src/pulse/PulseLatentIssue.ml
+++ b/infer/src/pulse/PulseLatentIssue.ml
@@ -35,19 +35,13 @@ let is_manifest (astate : AbductiveDomain.summary) =
 
 (* require a summary because we don't want to stop reporting because some non-abducible condition is
    not true as calling context cannot possibly influence such conditions *)
-let should_report (access_error : AbductiveDomain.summary PulseAccessResult.error) =
-  match access_error with
-  | ReportableError {astate; diagnostic} -> (
-    match diagnostic with
-    | MemoryLeak _ | StackVariableAddressEscape _ ->
-        (* these issues are reported regardless of the calling context, not sure if that's the right
-           decision yet *)
-        `ReportNow (astate, diagnostic)
-    | AccessToInvalidAddress latent ->
-        if is_manifest astate then `ReportNow (astate, diagnostic)
-        else `DelayReport (astate, AccessToInvalidAddress latent)
-    | ReadUninitializedValue latent ->
-        if is_manifest astate then `ReportNow (astate, diagnostic)
-        else `DelayReport (astate, ReadUninitializedValue latent) )
-  | ISLError astate ->
-      `ISLDelay astate
+let should_report (astate : AbductiveDomain.summary) (diagnostic : Diagnostic.t) =
+  match diagnostic with
+  | MemoryLeak _ | StackVariableAddressEscape _ ->
+      (* these issues are reported regardless of the calling context, not sure if that's the right
+         decision yet *)
+      `ReportNow
+  | AccessToInvalidAddress latent ->
+      if is_manifest astate then `ReportNow else `DelayReport (AccessToInvalidAddress latent)
+  | ReadUninitializedValue latent ->
+      if is_manifest astate then `ReportNow else `DelayReport (ReadUninitializedValue latent)
diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli
index f76a086b8..99e4a95a6 100644
--- a/infer/src/pulse/PulseLatentIssue.mli
+++ b/infer/src/pulse/PulseLatentIssue.mli
@@ -20,10 +20,6 @@ type t =
 
 val to_diagnostic : t -> Diagnostic.t
 
-val should_report :
-     AbductiveDomain.summary PulseAccessResult.error
-  -> [> `DelayReport of AbductiveDomain.summary * t
-     | `ReportNow of AbductiveDomain.summary * Diagnostic.t
-     | `ISLDelay of AbductiveDomain.summary ]
+val should_report : AbductiveDomain.summary -> Diagnostic.t -> [> `DelayReport of t | `ReportNow]
 
 val add_call : CallEvent.t * Location.t -> t -> t
diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml
index 0a50993a1..eab331f3e 100644
--- a/infer/src/pulse/PulseObjectiveCSummary.ml
+++ b/infer/src/pulse/PulseObjectiveCSummary.ml
@@ -25,7 +25,7 @@ let mk_objc_method_nil_summary_aux proc_desc astate =
   PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate
 
 
-let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_data) initial =
+let mk_objc_method_nil_summary {InterproceduralAnalysis.tenv; proc_desc; err_log} initial =
   let proc_name = Procdesc.get_proc_name proc_desc in
   match (initial, proc_name) with
   | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
@@ -36,7 +36,7 @@ let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_
          However, there is an exception in the case where the return type is non-POD.
          In that case it's UB and we want to report an error. *)
       let result = mk_objc_method_nil_summary_aux proc_desc astate in
-      Some (PulseReport.report_result analysis_data result)
+      Some (PulseReport.report_result tenv proc_desc err_log result)
   | ContinueProgram _, _
   | ExitProgram _, _
   | AbortProgram _, _
@@ -45,7 +45,7 @@ let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_
       None
 
 
-let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_data) astate =
+let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} astate =
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
   match astate with
@@ -54,7 +54,7 @@ let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_d
         let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in
         PulseArithmetic.prune_positive (fst value) astate
       in
-      PulseReport.report_result analysis_data result
+      PulseReport.report_result tenv proc_desc err_log result
   | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ ->
       [astate]
 
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 60d67871d..8d32252dd 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -643,7 +643,9 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
       map_call_result ~is_isl_error_prepost:false
         (astate :> AbductiveDomain.t)
         ~f:(fun astate ->
-          let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in
+          let+ (astate_summary : AbductiveDomain.summary) =
+            AbductiveDomain.summary_of_post tenv caller_proc_desc astate
+          in
           match callee_exec_state with
           | ContinueProgram _ | ISLLatentMemoryError _ ->
               assert false
@@ -655,17 +657,14 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
               let latent_issue =
                 LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
               in
-              let error =
-                ReportableError
-                  {diagnostic= LatentIssue.to_diagnostic latent_issue; astate= astate_summary}
-              in
-              match LatentIssue.should_report error with
-              | `DelayReport (astate, latent_issue) ->
-                  Ok (LatentAbortProgram {astate; latent_issue})
-              | `ReportNow (astate, diagnostic) ->
-                  Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)})
-              | `ISLDelay astate ->
-                  Error (ISLError (astate :> AbductiveDomain.t)) ) )
+              let diagnostic = LatentIssue.to_diagnostic latent_issue in
+              match LatentIssue.should_report astate_summary diagnostic with
+              | `DelayReport latent_issue ->
+                  Ok (LatentAbortProgram {astate= astate_summary; latent_issue})
+              | `ReportNow ->
+                  Error
+                    (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)}) )
+          )
   | ISLLatentMemoryError astate ->
       map_call_result ~is_isl_error_prepost:true
         (astate :> AbductiveDomain.t)
diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml
index 60d2997f9..bb5157902 100644
--- a/infer/src/pulse/PulseReport.ml
+++ b/infer/src/pulse/PulseReport.ml
@@ -8,7 +8,6 @@
 open! IStd
 open PulseBasicInterface
 open PulseDomainInterface
-open PulseOperations.Import
 
 let report ?(extra_trace = []) proc_desc err_log diagnostic =
   let open Diagnostic in
@@ -45,37 +44,65 @@ let is_suppressed tenv proc_desc diagnostic astate =
       false
 
 
-let report_error tenv proc_desc err_log access_error =
-  match LatentIssue.should_report access_error with
-  | `ReportNow (astate_summary, diagnostic) ->
-      if not (is_suppressed tenv proc_desc diagnostic astate_summary) then
-        report proc_desc err_log diagnostic ;
-      AbortProgram astate_summary
-  | `DelayReport (astate, latent_issue) ->
-      if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ;
-      LatentAbortProgram {astate; latent_issue}
-  | `ISLDelay astate ->
+let summary_of_error_post tenv proc_desc mk_error astate =
+  match AbductiveDomain.summary_of_post tenv proc_desc astate with
+  | Sat astate ->
+      Sat (mk_error astate)
+  | Unsat ->
+      Unsat
+
+
+let summary_error_of_error tenv proc_desc (error : AbductiveDomain.t AccessResult.error) :
+    AbductiveDomain.summary AccessResult.error SatUnsat.t =
+  match error with
+  | ReportableError {astate; diagnostic} ->
+      summary_of_error_post tenv proc_desc
+        (fun astate -> AccessResult.ReportableError {astate; diagnostic})
+        astate
+  | ISLError astate ->
+      summary_of_error_post tenv proc_desc (fun astate -> AccessResult.ISLError astate) astate
+
+
+let report_summary_error tenv proc_desc err_log
+    (access_error : AbductiveDomain.summary AccessResult.error) : _ ExecutionDomain.base_t =
+  match access_error with
+  | ISLError astate ->
       ISLLatentMemoryError astate
+  | ReportableError {astate; diagnostic} -> (
+    match LatentIssue.should_report astate diagnostic with
+    | `ReportNow ->
+        if not (is_suppressed tenv proc_desc diagnostic astate) then
+          report proc_desc err_log diagnostic ;
+        AbortProgram astate
+    | `DelayReport latent_issue ->
+        if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ;
+        LatentAbortProgram {astate; latent_issue} )
+
+
+let report_error tenv proc_desc err_log (access_error : AbductiveDomain.t AccessResult.error) =
+  let open SatUnsat.Import in
+  summary_error_of_error tenv proc_desc access_error >>| report_summary_error tenv proc_desc err_log
 
 
-let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results =
+let report_exec_results tenv proc_desc err_log results =
   List.filter_map results ~f:(fun exec_result ->
       match exec_result with
       | Ok post ->
           Some post
       | Error error -> (
-        match AccessResult.to_summary tenv proc_desc error with
+        match report_error tenv proc_desc err_log error with
         | Unsat ->
             None
-        | Sat error ->
-            Some (report_error tenv proc_desc err_log error) ) )
+        | Sat exec_state ->
+            Some exec_state ) )
 
 
-let report_results analysis_data results =
+let report_results tenv proc_desc err_log results =
+  let open IResult.Let_syntax in
   List.map results ~f:(fun result ->
       let+ astate = result in
-      ContinueProgram astate )
-  |> report_exec_results analysis_data
+      ExecutionDomain.ContinueProgram astate )
+  |> report_exec_results tenv proc_desc err_log
 
 
-let report_result analysis_data result = report_results analysis_data [result]
+let report_result tenv proc_desc err_log result = report_results tenv proc_desc err_log [result]
diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli
index bb0416a26..65fedb6ed 100644
--- a/infer/src/pulse/PulseReport.mli
+++ b/infer/src/pulse/PulseReport.mli
@@ -9,16 +9,18 @@ open! IStd
 open PulseDomainInterface
 
 val report_result :
-     PulseSummary.t InterproceduralAnalysis.t
-  -> AbductiveDomain.t AccessResult.t
-  -> ExecutionDomain.t list
+  Tenv.t -> Procdesc.t -> Errlog.t -> AbductiveDomain.t AccessResult.t -> ExecutionDomain.t list
 
 val report_results :
-     PulseSummary.t InterproceduralAnalysis.t
+     Tenv.t
+  -> Procdesc.t
+  -> Errlog.t
   -> AbductiveDomain.t AccessResult.t list
   -> ExecutionDomain.t list
 
 val report_exec_results :
-     PulseSummary.t InterproceduralAnalysis.t
+     Tenv.t
+  -> Procdesc.t
+  -> Errlog.t
   -> ExecutionDomain.t AccessResult.t list
   -> ExecutionDomain.t list
diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml
index 65deaf692..bd3bbb863 100644
--- a/infer/src/pulse/PulseSummary.ml
+++ b/infer/src/pulse/PulseSummary.ml
@@ -7,6 +7,8 @@
 
 open! IStd
 module F = Format
+module L = Logging
+open PulseBasicInterface
 open PulseDomainInterface
 
 type t = ExecutionDomain.summary list [@@deriving yojson_of]
@@ -19,4 +21,33 @@ let pp fmt summary =
   F.close_box ()
 
 
-let of_posts tenv pdesc posts = ExecutionDomain.summary_of_posts tenv pdesc posts
+let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate : ExecutionDomain.t) :
+    _ ExecutionDomain.base_t option =
+  match exec_astate with
+  | ContinueProgram astate -> (
+    match AbductiveDomain.summary_of_post tenv proc_desc astate with
+    | Unsat ->
+        None
+    | Sat astate ->
+        Some (continue_program astate) )
+  (* already a summary but need to reconstruct the variants to make the type system happy :( *)
+  | AbortProgram astate ->
+      Some (AbortProgram astate)
+  | ExitProgram astate ->
+      Some (ExitProgram astate)
+  | LatentAbortProgram {astate; latent_issue} ->
+      Some (LatentAbortProgram {astate; latent_issue})
+  | ISLLatentMemoryError astate ->
+      Some (ISLLatentMemoryError astate)
+
+
+let force_exit_program tenv proc_desc post =
+  exec_summary_of_post_common tenv proc_desc post ~continue_program:(fun astate ->
+      ExitProgram astate )
+
+
+let of_posts tenv proc_desc posts =
+  List.filter_mapi posts ~f:(fun i exec_state ->
+      L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ;
+      exec_summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate ->
+          ContinueProgram astate ) )
diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli
index 00733f818..de7fdcf6c 100644
--- a/infer/src/pulse/PulseSummary.mli
+++ b/infer/src/pulse/PulseSummary.mli
@@ -12,4 +12,7 @@ type t = ExecutionDomain.summary list [@@deriving yojson_of]
 
 val of_posts : Tenv.t -> Procdesc.t -> ExecutionDomain.t list -> t
 
+val force_exit_program :
+  Tenv.t -> Procdesc.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option
+
 val pp : Format.formatter -> t -> unit