diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index de7e20f7d..0757dac31 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -1731,6 +1731,12 @@ INTERNAL OPTIONS
            Maximum number of array elements and structure fields to keep
            track of for a given array address.
 
+       --pulse-report-latent-issues
+           Activates: Only use for testing, there should be no need to turn
+           this on for regular code analysis. Report latent issues instead of
+           waiting for them to become concrete. (Conversely:
+           --no-pulse-report-latent-issues)
+
        --pulse-widen-threshold int
            Under-approximate after int loop iterations
 
diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml
index 6420009b9..6ab2a8e51 100644
--- a/infer/src/IR/IntLit.ml
+++ b/infer/src/IR/IntLit.ml
@@ -157,3 +157,5 @@ let min i1 i2 = if leq i1 i2 then i1 else i2
 let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i
 
 let to_string i = F.asprintf "%a" pp i
+
+let equal i1 i2 = eq i1 i2
diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli
index f5d277e0a..9468b4872 100644
--- a/infer/src/IR/IntLit.mli
+++ b/infer/src/IR/IntLit.mli
@@ -27,6 +27,9 @@ val div : t -> t -> t
 
 val eq : t -> t -> bool
 
+val equal : t -> t -> bool
+(** an alias for {!eq}, for convenience *)
+
 val of_int : int -> t
 
 val of_big_int : Z.t -> t [@@warning "-32"]
diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml
index 308097782..45d5913f5 100644
--- a/infer/src/IR/Pvar.ml
+++ b/infer/src/IR/Pvar.ml
@@ -332,6 +332,6 @@ module Set = PrettyPrintable.MakePPSet (struct
   let pp = pp Pp.text
 end)
 
-type capture_mode = ByReference | ByValue [@@deriving compare]
+type capture_mode = ByReference | ByValue [@@deriving compare, equal]
 
 let string_of_capture_mode = function ByReference -> "by ref" | ByValue -> "by value"
diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli
index a214483c8..11674f5b3 100644
--- a/infer/src/IR/Pvar.mli
+++ b/infer/src/IR/Pvar.mli
@@ -174,6 +174,6 @@ val rename : f:(string -> string) -> t -> t
 (** Sets of pvars. *)
 module Set : PrettyPrintable.PPSet with type elt = t
 
-type capture_mode = ByReference | ByValue [@@deriving compare]
+type capture_mode = ByReference | ByValue [@@deriving compare, equal]
 
 val string_of_capture_mode : capture_mode -> string
diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml
index f848a36ad..116fed58f 100644
--- a/infer/src/IR/Sil.ml
+++ b/infer/src/IR/Sil.ml
@@ -23,7 +23,7 @@ type if_kind =
   | Ik_land_lor  (** obtained from translation of && or || *)
   | Ik_while
   | Ik_switch
-[@@deriving compare]
+[@@deriving compare, equal]
 
 type instr_metadata =
   | Abstract of Location.t
diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli
index dcabb35b8..4221d5d27 100644
--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@@ -22,7 +22,7 @@ type if_kind =
   | Ik_land_lor  (** obtained from translation of && or || *)
   | Ik_while
   | Ik_switch
-[@@deriving compare]
+[@@deriving compare, equal]
 
 type instr_metadata =
   | Abstract of Location.t
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index efc6844a3..1764f8f79 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -1881,6 +1881,12 @@ and pulse_model_transfer_ownership =
      are method or namespace::method"
 
 
+and pulse_report_latent_issues =
+  CLOpt.mk_bool ~long:"pulse-report-latent-issues"
+    "Only use for testing, there should be no need to turn this on for regular code analysis. \
+     Report latent issues instead of waiting for them to become concrete."
+
+
 and pulse_widen_threshold =
   CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3
     "Under-approximate after $(i,int) loop iterations"
@@ -3025,6 +3031,8 @@ and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
   List.partition_map ~f:aux models
 
 
+and pulse_report_latent_issues = !pulse_report_latent_issues
+
 and pulse_widen_threshold = !pulse_widen_threshold
 
 and pure_by_default = !pure_by_default
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 4203bd309..6f83ab8f7 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -469,6 +469,8 @@ val pulse_model_transfer_ownership_namespace : (string * string) list
 
 val pulse_model_transfer_ownership : string list
 
+val pulse_report_latent_issues : bool
+
 val pulse_widen_threshold : int
 
 val pure_by_default : bool
diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml
index aa2cff7ac..ffc3acbf4 100644
--- a/infer/src/checkers/impurity.ml
+++ b/infer/src/checkers/impurity.ml
@@ -142,7 +142,7 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai
     match exec_state with
     | ExitProgram astate ->
         (astate, true)
-    | AbortProgram astate | ContinueProgram astate ->
+    | AbortProgram astate | ContinueProgram astate | LatentAbortProgram {astate} ->
         (astate, false)
   in
   let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 31b8f0ac4..be78f3962 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -12,21 +12,40 @@ open IResult.Let_syntax
 open PulseBasicInterface
 open PulseDomainInterface
 
-let report {InterproceduralAnalysis.proc_desc; err_log} diagnostic =
+let report ?(extra_trace = []) proc_desc err_log diagnostic =
   let open Diagnostic in
-  Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic)
+  Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic)
+    ~ltr:(extra_trace @ get_trace diagnostic)
     Pulse (get_issue_type diagnostic) (get_message diagnostic)
 
 
-let check_error_transform analysis_data ~f = function
+let check_error_transform {InterproceduralAnalysis.proc_desc; err_log} ~f = function
   | Ok astate ->
       f astate
-  | Error (diagnostic, astate) ->
+  | Error (diagnostic, astate) -> (
       let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
       if is_unsat then []
-      else (
-        report analysis_data diagnostic ;
-        [ExecutionDomain.AbortProgram astate] )
+      else
+        let astate = AbductiveDomain.of_post proc_desc astate in
+        if PulseArithmetic.is_unsat_cheap astate then []
+        else
+          match LatentIssue.should_report_diagnostic astate diagnostic with
+          | `ReportNow ->
+              report proc_desc err_log diagnostic ;
+              [ExecutionDomain.AbortProgram astate]
+          | `DelayReport latent_issue ->
+              ( if Config.pulse_report_latent_issues then
+                (* HACK: report latent issues with a prominent message to distinguish them from
+                   non-latent. Useful for infer's own tests. *)
+                let diagnostic = LatentIssue.to_diagnostic latent_issue in
+                let extra_trace =
+                  let depth = 0 in
+                  let tags = [] in
+                  let location = Diagnostic.get_location diagnostic in
+                  [Errlog.make_trace_element depth location "*** LATENT ***" tags]
+                in
+                report ~extra_trace proc_desc err_log diagnostic ) ;
+              [ExecutionDomain.LatentAbortProgram {astate; latent_issue}] )
 
 
 let check_error_continue analysis_data result =
@@ -83,14 +102,14 @@ module PulseTransferFunctions = struct
 
   (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *)
   let exec_object_out_of_scope call_loc (pvar, typ) exec_state =
-    match exec_state with
-    | ExecutionDomain.ContinueProgram astate ->
+    match (exec_state : ExecutionDomain.t) with
+    | ContinueProgram astate ->
         let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
         let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in
         (* invalidate [&x] *)
         PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
         >>| ExecutionDomain.continue
-    | ExecutionDomain.AbortProgram _ | ExecutionDomain.ExitProgram _ ->
+    | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
         Ok exec_state
 
 
@@ -183,7 +202,7 @@ module PulseTransferFunctions = struct
         ~f:(fun astates (astate : Domain.t) ->
           let astate =
             match astate with
-            | AbortProgram _ | ExitProgram _ ->
+            | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
                 [astate]
             | ContinueProgram astate ->
                 dispatch_call analysis_data ret call_exp actuals location call_flags astate
@@ -207,7 +226,7 @@ module PulseTransferFunctions = struct
   let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
       _cfg_node (instr : Sil.instr) : Domain.t list =
     match astate with
-    | AbortProgram _ ->
+    | AbortProgram _ | LatentAbortProgram _ ->
         (* We can also continue the analysis with the error state here
                  but there might be a risk we would get nonsense. *)
         [astate]
@@ -258,7 +277,7 @@ module PulseTransferFunctions = struct
             List.fold
               ~f:(fun astates (astate : Domain.t) ->
                 match astate with
-                | AbortProgram _ | ExitProgram _ ->
+                | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
                     [astate]
                 | ContinueProgram astate ->
                     let astate =
diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml
index 2f6dc24a3..105a622bc 100644
--- a/infer/src/pulse/PulseArithmetic.ml
+++ b/infer/src/pulse/PulseArithmetic.ml
@@ -52,3 +52,7 @@ let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.
 let is_unsat_expensive astate =
   let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in
   (AbductiveDomain.set_path_condition phi' astate, is_unsat)
+
+
+let has_no_assumptions astate =
+  PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition
diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli
index 0d5e440ac..1c986714f 100644
--- a/infer/src/pulse/PulseArithmetic.mli
+++ b/infer/src/pulse/PulseArithmetic.mli
@@ -35,3 +35,5 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
 val is_unsat_cheap : AbductiveDomain.t -> bool
 
 val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool
+
+val has_no_assumptions : AbductiveDomain.t -> bool
diff --git a/infer/src/pulse/PulseCallEvent.ml b/infer/src/pulse/PulseCallEvent.ml
index cf423a756..8aad844b3 100644
--- a/infer/src/pulse/PulseCallEvent.ml
+++ b/infer/src/pulse/PulseCallEvent.ml
@@ -12,7 +12,7 @@ type t =
   | Model of string
   | SkippedKnownCall of Procname.t
   | SkippedUnknownCall of Exp.t
-[@@deriving compare]
+[@@deriving compare, equal]
 
 let pp_config ~verbose fmt =
   let pp_proc_name = if verbose then Procname.pp else Procname.describe in
diff --git a/infer/src/pulse/PulseCallEvent.mli b/infer/src/pulse/PulseCallEvent.mli
index ad6b37ab3..a3fc36be9 100644
--- a/infer/src/pulse/PulseCallEvent.mli
+++ b/infer/src/pulse/PulseCallEvent.mli
@@ -13,7 +13,7 @@ type t =
   | Model of string  (** hardcoded model *)
   | SkippedKnownCall of Procname.t  (** known function without summary *)
   | SkippedUnknownCall of Exp.t  (** couldn't link the expression to a proc name *)
-[@@deriving compare]
+[@@deriving compare, equal]
 
 val pp : F.formatter -> t -> unit
 
diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml
index 538bd6181..05277d50e 100644
--- a/infer/src/pulse/PulseDiagnostic.ml
+++ b/infer/src/pulse/PulseDiagnostic.ml
@@ -12,21 +12,30 @@ module Invalidation = PulseInvalidation
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
 
+type access_to_invalid_address =
+  { calling_context: (CallEvent.t * Location.t) list
+  ; invalidation: Invalidation.t
+  ; invalidation_trace: Trace.t
+  ; access_trace: Trace.t }
+[@@deriving equal]
+
 type t =
-  | AccessToInvalidAddress of
-      {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
+  | AccessToInvalidAddress of access_to_invalid_address
   | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
+[@@deriving equal]
 
 let get_location = function
-  | AccessToInvalidAddress {access_trace} ->
+  | AccessToInvalidAddress {calling_context= []; access_trace} ->
       Trace.get_outer_location access_trace
+  | AccessToInvalidAddress {calling_context= (_, location) :: _} ->
+      (* report at the call site that triggers the bug *) location
   | MemoryLeak {location} | StackVariableAddressEscape {location} ->
       location
 
 
 let get_message = function
-  | AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} ->
+  | AccessToInvalidAddress {calling_context; invalidation; invalidation_trace; access_trace} ->
       (* The goal is to get one of the following messages depending on the scenario:
 
          42: delete x; return x->f
@@ -44,19 +53,27 @@ let get_message = function
          Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then
          "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
       *)
+      (* whether the [calling_context + trace] starts with a call or contains only an immediate event *)
+      let immediate_or_first_call calling_context (trace : Trace.t) =
+        match (calling_context, trace) with
+        | [], Immediate _ ->
+            `Immediate
+        | (f, _) :: _, _ | [], ViaCall {f; _} ->
+            `Call f
+      in
       let pp_access_trace fmt (trace : Trace.t) =
-        match trace with
-        | Immediate _ ->
+        match immediate_or_first_call calling_context trace with
+        | `Immediate ->
             F.fprintf fmt "accessing memory that "
-        | ViaCall {f; _} ->
+        | `Call f ->
             F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f
       in
       let pp_invalidation_trace line invalidation fmt (trace : Trace.t) =
         let pp_line fmt line = F.fprintf fmt " on line %d" line in
-        match trace with
-        | Immediate _ ->
+        match immediate_or_first_call calling_context trace with
+        | `Immediate ->
             F.fprintf fmt "%a%a" Invalidation.describe invalidation pp_line line
-        | ViaCall {f; _} ->
+        | `Call f ->
             F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalidation
               pp_line line CallEvent.describe f
       in
@@ -97,7 +114,21 @@ let add_errlog_header ~title location errlog =
 
 
 let get_trace = function
-  | AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} ->
+  | AccessToInvalidAddress {calling_context; invalidation; invalidation_trace; access_trace} ->
+      (fun errlog ->
+        match calling_context with
+        | [] ->
+            errlog
+        | (_, first_call_loc) :: _ ->
+            add_errlog_header ~title:"calling context starts here" first_call_loc
+            @@ ( List.fold calling_context ~init:(errlog, 0) ~f:(fun (errlog, depth) (call, loc) ->
+                     ( Errlog.make_trace_element depth loc
+                         (F.asprintf "in call to %a" CallEvent.pp call)
+                         []
+                       :: errlog
+                     , depth + 1 ) )
+               |> fst ) )
+      @@
       let start_location = Trace.get_start_location invalidation_trace in
       add_errlog_header ~title:"invalidation part of the trace starts here" start_location
       @@ Trace.add_to_errlog ~nesting:1
diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli
index ef5952e7d..eda012f90 100644
--- a/infer/src/pulse/PulseDiagnostic.mli
+++ b/infer/src/pulse/PulseDiagnostic.mli
@@ -6,16 +6,30 @@
  *)
 
 open! IStd
+module CallEvent = PulseCallEvent
 module Invalidation = PulseInvalidation
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
 
+type access_to_invalid_address =
+  { calling_context: (CallEvent.t * Location.t) list
+        (** the list of function calls leading to the issue being realised, which is an additional
+            common prefix to the traces in the record *)
+  ; invalidation: Invalidation.t
+  ; invalidation_trace: Trace.t
+        (** assuming we are in the calling context, the trace leads to [invalidation] without
+            further assumptions *)
+  ; access_trace: Trace.t
+        (** assuming we are in the calling context, the trace leads to an access to the value
+            invalidated in [invalidation_trace] without further assumptions *) }
+[@@deriving equal]
+
 (** an error to report to the user *)
 type t =
-  | AccessToInvalidAddress of
-      {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
+  | AccessToInvalidAddress of access_to_invalid_address
   | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
+[@@deriving equal]
 
 val get_message : t -> string
 
diff --git a/infer/src/pulse/PulseDomainInterface.ml b/infer/src/pulse/PulseDomainInterface.ml
index 97e5dde9f..d49e9c972 100644
--- a/infer/src/pulse/PulseDomainInterface.ml
+++ b/infer/src/pulse/PulseDomainInterface.ml
@@ -21,6 +21,7 @@ module BaseDomain = PulseBaseDomain
 module BaseStack = PulseBaseStack
 module BaseMemory = PulseBaseMemory
 module BaseAddressAttributes = PulseBaseAddressAttributes
+module LatentIssue = PulseLatentIssue
 
 (** {2 Enforce short form usage} *)
 
@@ -36,4 +37,5 @@ include struct
   [@@deprecated "use the short form BaseAddressAttributes instead"]
   module PulseExecutionDomain = PulseExecutionDomain
   [@@deprecated "use the short form ExecutionDomain instead"]
+  module PulseLatentIssue = PulseLatentIssue [@@deprecated "use the short form LatentIssue instead"]
 end
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index 2b8428d7d..b09e6eb09 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -8,12 +8,15 @@
 open! IStd
 module F = Format
 module L = Logging
+open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
+module LatentIssue = PulseLatentIssue
 
 type t =
   | AbortProgram of AbductiveDomain.t
   | ContinueProgram of AbductiveDomain.t
   | ExitProgram of AbductiveDomain.t
+  | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t}
 
 let continue astate = ContinueProgram astate
 
@@ -25,6 +28,9 @@ let leq ~lhs ~rhs =
   | ContinueProgram astate1, ContinueProgram astate2
   | ExitProgram astate1, ExitProgram astate2 ->
       AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
+  | ( LatentAbortProgram {astate= astate1; latent_issue= issue1}
+    , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
+      LatentIssue.equal issue1 issue2 && AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
   | _ ->
       false
 
@@ -36,6 +42,12 @@ let pp fmt = function
       F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate
   | AbortProgram astate ->
       F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp astate
+  | LatentAbortProgram {astate; latent_issue} ->
+      let diagnostic = LatentIssue.to_diagnostic latent_issue in
+      let message = Diagnostic.get_message diagnostic in
+      let location = Diagnostic.get_location diagnostic in
+      F.fprintf fmt "{LatentAbortProgram(%a: %s) %a}" Location.pp location message
+        AbductiveDomain.pp astate
 
 
 let map ~f exec_state =
@@ -46,11 +58,18 @@ let map ~f exec_state =
       ContinueProgram (f astate)
   | ExitProgram astate ->
       ExitProgram (f astate)
+  | LatentAbortProgram {astate; latent_issue} ->
+      LatentAbortProgram {astate= f astate; latent_issue}
 
 
 let of_posts pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
-      let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in
+      let ( AbortProgram astate
+          | ContinueProgram astate
+          | ExitProgram astate
+          | LatentAbortProgram {astate} ) =
+        exec_state
+      in
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
       let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
       if is_unsat then None
diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli
index 446a9210d..9d4791db8 100644
--- a/infer/src/pulse/PulseExecutionDomain.mli
+++ b/infer/src/pulse/PulseExecutionDomain.mli
@@ -4,18 +4,22 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  *)
+
 open! IStd
+module AbductiveDomain = PulseAbductiveDomain
+module LatentIssue = PulseLatentIssue
 
 type t =
-  | AbortProgram of PulseAbductiveDomain.t
+  | AbortProgram of AbductiveDomain.t
       (** represents the state at the program point that caused an error *)
-  | ContinueProgram of PulseAbductiveDomain.t  (** represents the state at the program point *)
-  | ExitProgram of PulseAbductiveDomain.t
-      (** represents the state originating at exit/divergence. *)
+  | ContinueProgram of AbductiveDomain.t  (** represents the state at the program point *)
+  | ExitProgram of AbductiveDomain.t  (** represents the state originating at exit/divergence. *)
+  | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t}
+      (** this path leads to an error but we don't have conclusive enough data to report it yet *)
 
 include AbstractDomain.NoJoin with type t := t
 
-val continue : PulseAbductiveDomain.t -> t
+val continue : AbductiveDomain.t -> t
 
 val of_posts : Procdesc.t -> t list -> t list
 
diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index b3525cffa..4bac45ca4 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -925,9 +925,19 @@ module Atom = struct
     Term.has_var_notin vars t1 || Term.has_var_notin vars t2
 
 
-  module Set = Caml.Set.Make (struct
-    type nonrec t = t [@@deriving compare]
-  end)
+  module Set = struct
+    include Caml.Set.Make (struct
+      type nonrec t = t [@@deriving compare]
+    end)
+
+    let pp_with_pp_var pp_var fmt atoms =
+      if is_empty atoms then F.pp_print_string fmt "true (no atoms)"
+      else
+        Pp.collection ~sep:"∧"
+          ~fold:(IContainer.fold_of_pervasives_set_fold fold)
+          ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (pp_with_pp_var pp_var) atom)
+          fmt atoms
+  end
 end
 
 module SatUnsatMonad = struct
@@ -957,267 +967,293 @@ module VarUF =
     end)
     (Var.Set)
 
-type t =
-  { var_eqs: VarUF.t  (** equality relation between variables *)
-  ; linear_eqs: LinArith.t Var.Map.t
-        (** equalities of the form [x = l] where [l] is from linear arithmetic *)
-  ; atoms: Atom.Set.t  (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) }
+module Formula = struct
+  type t =
+    { var_eqs: VarUF.t  (** equality relation between variables *)
+    ; linear_eqs: LinArith.t Var.Map.t
+          (** equalities of the form [x = l] where [l] is from linear arithmetic *)
+    ; atoms: Atom.Set.t  (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) }
 
-let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty}
+  let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty}
 
-let pp_with_pp_var pp_var fmt phi =
-  let pp_linear_eqs fmt m =
-    if Var.Map.is_empty m then F.pp_print_string fmt "true (no linear)"
-    else
-      Pp.collection ~sep:" ∧ "
-        ~fold:(IContainer.fold_of_pervasives_map_fold Var.Map.fold)
-        ~pp_item:(fun fmt (v, l) -> F.fprintf fmt "%a = %a" pp_var v (LinArith.pp pp_var) l)
-        fmt m
-  in
-  let pp_atoms fmt atoms =
-    if Atom.Set.is_empty atoms then F.pp_print_string fmt "true (no atoms)"
-    else
-      Pp.collection ~sep:"∧"
-        ~fold:(IContainer.fold_of_pervasives_set_fold Atom.Set.fold)
-        ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (Atom.pp_with_pp_var pp_var) atom)
-        fmt atoms
-  in
-  F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@]"
-    (VarUF.pp ~pp_empty:(fun fmt -> F.pp_print_string fmt "true (no var=var)") pp_var)
-    phi.var_eqs pp_linear_eqs phi.linear_eqs pp_atoms phi.atoms
+  let pp_with_pp_var pp_var fmt phi =
+    let pp_linear_eqs fmt m =
+      if Var.Map.is_empty m then F.pp_print_string fmt "true (no linear)"
+      else
+        Pp.collection ~sep:" ∧ "
+          ~fold:(IContainer.fold_of_pervasives_map_fold Var.Map.fold)
+          ~pp_item:(fun fmt (v, l) -> F.fprintf fmt "%a = %a" pp_var v (LinArith.pp pp_var) l)
+          fmt m
+    in
+    F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@]"
+      (VarUF.pp ~pp_empty:(fun fmt -> F.pp_print_string fmt "true (no var=var)") pp_var)
+      phi.var_eqs pp_linear_eqs phi.linear_eqs (Atom.Set.pp_with_pp_var pp_var) phi.atoms
 
 
-let pp = pp_with_pp_var Var.pp
+  (** module that breaks invariants more often that the rest, with an interface that is safer to use *)
+  module Normalizer : sig
+    val and_var_linarith : Var.t -> LinArith.t -> t -> t normalized
 
-(** module that breaks invariants more often that the rest, with an interface that is safer to use *)
-module Normalizer : sig
-  val and_var_linarith : Var.t -> LinArith.t -> t -> t normalized
+    val and_var_var : Var.t -> Var.t -> t -> t normalized
 
-  val and_var_var : Var.t -> Var.t -> t -> t normalized
+    val and_atom : Atom.t -> t -> t normalized
 
-  val and_atom : Atom.t -> t -> t normalized
+    val normalize_atom : t -> Atom.t -> Atom.t option normalized
 
-  val normalize : t -> t normalized
-end = struct
-  (* Use the monadic notations when normalizing formulas. *)
-  open SatUnsatMonad
-
-  (** OVERVIEW: the best way to think about this is as a half-assed Shostak technique.
-
-      The [var_eqs] and [linear_eqs] parts of a formula are kept in a normal form of sorts. We apply
-      some deduction every time a new equality is discovered. Where this is incomplete is that 1) we
-      don't insist on normalizing the linear part of the relation always, and 2) we stop discovering
-      new consequences of facts after some fixed number of steps (the [fuel] argument of some of the
-      functions of this module).
-
-      Normalizing more than 1) happens on [normalize], where we rebuild the linear equality relation
-      (the equalities between variables are always "normalized" thanks to the union-find data
-      structure).
-
-      For 2), there is no mitigation as saturating the consequences of what we know implies keeping
-      track of *all* the consequences (to avoid diverging by re-discovering the same facts over and
-      over), which would be expensive.
-
-      There is also an interaction between equality classes and linear equalities [x = l], as each
-      such key [x] in the [linear_eqs] map is (or was at some point) the representative of its
-      class. Unlike (non-diverging...) Shostak techniques, we do not try very hard to normalize the
-      [l] in the linear equalities.
-
-      Disclaimer: It could be that this half-assedness is premature optimisation and that we could
-      afford much more completeness. *)
-
-  (** the canonical representative of a given variable *)
-  let get_repr phi x = VarUF.find phi.var_eqs x
-
-  (** substitute vars in [l] *once* with their linear form to discover more simplification
-      opportunities *)
-  let apply phi l =
-    LinArith.subst_variables l ~f:(fun v ->
-        let repr = (get_repr phi v :> Var.t) in
-        match Var.Map.find_opt repr phi.linear_eqs with
-        | None ->
-            VarSubst repr
-        | Some l' ->
-            LinSubst l' )
+    val normalize : t -> t normalized
 
+    val implies_atom : t -> Atom.t -> bool
+  end = struct
+    (* Use the monadic notations when normalizing formulas. *)
+    open SatUnsatMonad
 
-  let rec solve_normalized_eq ~fuel l1 l2 phi =
-    LinArith.solve_eq l1 l2
-    >>= function
-    | None ->
-        Sat phi
-    | Some (v, l) -> (
-      match LinArith.get_as_var l with
-      | Some v' ->
-          merge_vars ~fuel (v :> Var.t) v' phi
-      | None -> (
-        match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
-        | None ->
-            (* this can break the (as a result non-)invariant that variables in the domain of
-               [linear_eqs] do not appear in the range of [linear_eqs] *)
-            Sat {phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}
-        | Some l' ->
-            (* This is the only step that consumes fuel: discovering an equality [l = l']: because we
-               do not record these anywhere (except when there consequence can be recorded as [y =
-               l''] or [y = y'], we could potentially discover the same equality over and over and
-               diverge otherwise. Or could we? *)
-            (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
-               normalize it *)
-            if fuel > 0 then (
-              L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ;
-              solve_normalized_eq ~fuel:(fuel - 1) l (apply phi l') phi )
-            else (
-              (* [fuel = 0]: give up simplifying further for fear of diverging *)
-              L.d_printfln "Ran out of fuel solving linear equality" ;
-              Sat phi ) ) )
-
-
-  and merge_vars ~fuel v1 v2 phi =
-    let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
-    let phi = {phi with var_eqs} in
-    match subst_opt with
-    | None ->
-        (* we already knew the equality *)
-        Sat phi
-    | Some (v_old, v_new) -> (
-        (* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new =
-           l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *)
-        (* NOTE: we try to maintain the invariant that for all [x=l] in [phi.linear_eqs], [x ∉
-           vars(l)]. We also try to stay as close as possible (without going back and re-normalizing
-           every linear equality every time we learn new equalities) to the invariant that the
-           domain and the range of [phi.linear_eqs] mention distinct variables. This is to speed up
-           normalization steps: when the stronger invariant holds we can normalize in one step (in
-           [normalize_linear_eqs]). *)
-        let v_new = (v_new :> Var.t) in
-        let phi, l_new =
-          match Var.Map.find_opt v_new phi.linear_eqs with
-          | None ->
-              (phi, None)
-          | Some l ->
-              if LinArith.has_var v_old l then
-                let l_new = LinArith.subst v_old v_new l in
-                let linear_eqs = Var.Map.add v_new l_new phi.linear_eqs in
-                ({phi with linear_eqs}, Some l_new)
-              else (phi, Some l)
-        in
-        let phi, l_old =
-          match Var.Map.find_opt v_old phi.linear_eqs with
-          | None ->
-              (phi, None)
-          | Some l_old ->
-              (* [l_old] has no [v_old] or [v_new] by invariant so no need to subst, unlike for
-                 [l_new] above: variables in [l_old] are strictly greater than [v_old], and [v_new]
-                 is smaller than [v_old] *)
-              ({phi with linear_eqs= Var.Map.remove v_old phi.linear_eqs}, Some l_old)
-        in
-        match (l_old, l_new) with
-        | None, None | None, Some _ ->
-            Sat phi
-        | Some l, None ->
-            Sat {phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}
-        | Some l1, Some l2 ->
-            (* no need to consume fuel here as we can only go through this branch finitely many
-               times because there are finitely many variables in a given formula *)
-            (* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *)
-            solve_normalized_eq ~fuel l1 l2 phi )
+    (** OVERVIEW: the best way to think about this is as a half-assed Shostak technique.
 
+        The [var_eqs] and [linear_eqs] parts of a formula are kept in a normal form of sorts. We
+        apply some deduction every time a new equality is discovered. Where this is incomplete is
+        that 1) we don't insist on normalizing the linear part of the relation always, and 2) we
+        stop discovering new consequences of facts after some fixed number of steps (the [fuel]
+        argument of some of the functions of this module).
 
-  (** an arbitrary value *)
-  let base_fuel = 5
+        Normalizing more than 1) happens on [normalize], where we rebuild the linear equality
+        relation (the equalities between variables are always "normalized" thanks to the union-find
+        data structure).
 
-  let solve_eq t1 t2 phi = solve_normalized_eq ~fuel:base_fuel (apply phi t1) (apply phi t2) phi
+        For 2), there is no mitigation as saturating the consequences of what we know implies
+        keeping track of *all* the consequences (to avoid diverging by re-discovering the same facts
+        over and over), which would be expensive.
 
-  let and_var_linarith v l phi = solve_eq l (LinArith.of_var v) phi
+        There is also an interaction between equality classes and linear equalities [x = l], as each
+        such key [x] in the [linear_eqs] map is (or was at some point) the representative of its
+        class. Unlike (non-diverging...) Shostak techniques, we do not try very hard to normalize
+        the [l] in the linear equalities.
 
-  let and_var_var v1 v2 phi = merge_vars ~fuel:base_fuel v1 v2 phi
+        Disclaimer: It could be that this half-assedness is premature optimisation and that we could
+        afford much more completeness. *)
 
-  let rec normalize_linear_eqs ~fuel phi0 =
-    let* changed, phi' =
-      (* reconstruct the relation from scratch *)
-      Var.Map.fold
-        (fun v l acc ->
-          let* changed, phi = acc in
-          let l' = apply phi0 l in
-          let+ phi' = and_var_linarith v l' phi in
-          (changed || not (phys_equal l l'), phi') )
-        phi0.linear_eqs
-        (Sat (false, {phi0 with linear_eqs= Var.Map.empty}))
-    in
-    if changed then
-      if fuel > 0 then (
-        (* do another pass if we can afford it *)
-        L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ;
-        normalize_linear_eqs ~fuel:(fuel - 1) phi' )
-      else (
-        L.d_printfln "ran out of fuel normalizing linear equalities" ;
-        Sat phi' )
-    else Sat phi0
-
-
-  let normalize_atom phi (atom : Atom.t) =
-    let normalize_term phi t =
-      Term.subst_variables t ~f:(fun v ->
-          let v_canon = (VarUF.find phi.var_eqs v :> Var.t) in
-          match Var.Map.find_opt v_canon phi.linear_eqs with
+    (** the canonical representative of a given variable *)
+    let get_repr phi x = VarUF.find phi.var_eqs x
+
+    (** substitute vars in [l] *once* with their linear form to discover more simplification
+        opportunities *)
+    let apply phi l =
+      LinArith.subst_variables l ~f:(fun v ->
+          let repr = (get_repr phi v :> Var.t) in
+          match Var.Map.find_opt repr phi.linear_eqs with
           | None ->
-              VarSubst v_canon
-          | Some l -> (
-            match LinArith.get_as_const l with None -> LinSubst l | Some q -> QSubst q ) )
-    in
-    let atom' = Atom.map_terms atom ~f:(fun t -> normalize_term phi t) in
-    Atom.eval atom' |> sat_of_eval_result
+              VarSubst repr
+          | Some l' ->
+              LinSubst l' )
 
 
-  (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if
-      [phi.linear_eqs] was changed as a result *)
-  let and_atom atom phi =
-    normalize_atom phi atom
-    >>= function
-    | None ->
-        Sat (false, phi)
-    | Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) ->
-        (* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so
-           they end up only on one side, hence only this match case is needed to detect linear
-           equalities *)
-        let+ phi' = solve_eq l (LinArith.of_q c) phi in
-        (true, phi')
-    | Some atom' ->
-        Sat (false, {phi with atoms= Atom.Set.add atom' phi.atoms})
-
-
-  let normalize_atoms phi =
-    let atoms0 = phi.atoms in
-    let init = Sat (false, {phi with atoms= Atom.Set.empty}) in
-    IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom ->
-        let* changed, phi = acc in
-        let+ changed', phi = and_atom atom phi in
-        (changed || changed', phi) )
-
-
-  let normalize phi =
-    (* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by
-       [normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining
-       fuel). That's ok because there's not much fuel to begin with, and as long as we're making
-       progress it's probably worth it anyway. *)
-    let rec normalize_with_fuel ~fuel phi =
-      if fuel <= 0 then (
-        L.d_printfln "ran out of fuel when normalizing" ;
-        Sat phi )
-      else
-        let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in
-        if new_linear_eqs then (
-          L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
-          normalize_with_fuel ~fuel:(fuel - 1) phi )
-        else Sat phi
-    in
-    normalize_with_fuel ~fuel:base_fuel phi
+    let rec solve_normalized_eq ~fuel l1 l2 phi =
+      LinArith.solve_eq l1 l2
+      >>= function
+      | None ->
+          Sat phi
+      | Some (v, l) -> (
+        match LinArith.get_as_var l with
+        | Some v' ->
+            merge_vars ~fuel (v :> Var.t) v' phi
+        | None -> (
+          match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
+          | None ->
+              (* this can break the (as a result non-)invariant that variables in the domain of
+                 [linear_eqs] do not appear in the range of [linear_eqs] *)
+              Sat {phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}
+          | Some l' ->
+              (* This is the only step that consumes fuel: discovering an equality [l = l']: because we
+                 do not record these anywhere (except when there consequence can be recorded as [y =
+                 l''] or [y = y'], we could potentially discover the same equality over and over and
+                 diverge otherwise. Or could we? *)
+              (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
+                 normalize it *)
+              if fuel > 0 then (
+                L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ;
+                solve_normalized_eq ~fuel:(fuel - 1) l (apply phi l') phi )
+              else (
+                (* [fuel = 0]: give up simplifying further for fear of diverging *)
+                L.d_printfln "Ran out of fuel solving linear equality" ;
+                Sat phi ) ) )
+
+
+    and merge_vars ~fuel v1 v2 phi =
+      let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
+      let phi = {phi with var_eqs} in
+      match subst_opt with
+      | None ->
+          (* we already knew the equality *)
+          Sat phi
+      | Some (v_old, v_new) -> (
+          (* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new =
+             l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *)
+          (* NOTE: we try to maintain the invariant that for all [x=l] in [phi.linear_eqs], [x ∉
+             vars(l)]. We also try to stay as close as possible (without going back and re-normalizing
+             every linear equality every time we learn new equalities) to the invariant that the
+             domain and the range of [phi.linear_eqs] mention distinct variables. This is to speed up
+             normalization steps: when the stronger invariant holds we can normalize in one step (in
+             [normalize_linear_eqs]). *)
+          let v_new = (v_new :> Var.t) in
+          let phi, l_new =
+            match Var.Map.find_opt v_new phi.linear_eqs with
+            | None ->
+                (phi, None)
+            | Some l ->
+                if LinArith.has_var v_old l then
+                  let l_new = LinArith.subst v_old v_new l in
+                  let linear_eqs = Var.Map.add v_new l_new phi.linear_eqs in
+                  ({phi with linear_eqs}, Some l_new)
+                else (phi, Some l)
+          in
+          let phi, l_old =
+            match Var.Map.find_opt v_old phi.linear_eqs with
+            | None ->
+                (phi, None)
+            | Some l_old ->
+                (* [l_old] has no [v_old] or [v_new] by invariant so no need to subst, unlike for
+                   [l_new] above: variables in [l_old] are strictly greater than [v_old], and [v_new]
+                   is smaller than [v_old] *)
+                ({phi with linear_eqs= Var.Map.remove v_old phi.linear_eqs}, Some l_old)
+          in
+          match (l_old, l_new) with
+          | None, None | None, Some _ ->
+              Sat phi
+          | Some l, None ->
+              Sat {phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}
+          | Some l1, Some l2 ->
+              (* no need to consume fuel here as we can only go through this branch finitely many
+                 times because there are finitely many variables in a given formula *)
+              (* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *)
+              solve_normalized_eq ~fuel l1 l2 phi )
+
+
+    (** an arbitrary value *)
+    let base_fuel = 5
+
+    let solve_eq t1 t2 phi = solve_normalized_eq ~fuel:base_fuel (apply phi t1) (apply phi t2) phi
+
+    let and_var_linarith v l phi = solve_eq l (LinArith.of_var v) phi
+
+    let and_var_var v1 v2 phi = merge_vars ~fuel:base_fuel v1 v2 phi
+
+    let rec normalize_linear_eqs ~fuel phi0 =
+      let* changed, phi' =
+        (* reconstruct the relation from scratch *)
+        Var.Map.fold
+          (fun v l acc ->
+            let* changed, phi = acc in
+            let l' = apply phi0 l in
+            let+ phi' = and_var_linarith v l' phi in
+            (changed || not (phys_equal l l'), phi') )
+          phi0.linear_eqs
+          (Sat (false, {phi0 with linear_eqs= Var.Map.empty}))
+      in
+      if changed then
+        if fuel > 0 then (
+          (* do another pass if we can afford it *)
+          L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ;
+          normalize_linear_eqs ~fuel:(fuel - 1) phi' )
+        else (
+          L.d_printfln "ran out of fuel normalizing linear equalities" ;
+          Sat phi' )
+      else Sat phi0
+
+
+    let normalize_atom phi (atom : Atom.t) =
+      let normalize_term phi t =
+        Term.subst_variables t ~f:(fun v ->
+            let v_canon = (VarUF.find phi.var_eqs v :> Var.t) in
+            match Var.Map.find_opt v_canon phi.linear_eqs with
+            | None ->
+                VarSubst v_canon
+            | Some l -> (
+              match LinArith.get_as_const l with None -> LinSubst l | Some q -> QSubst q ) )
+      in
+      let atom' = Atom.map_terms atom ~f:(fun t -> normalize_term phi t) in
+      Atom.eval atom' |> sat_of_eval_result
 
 
-  let and_atom atom phi = and_atom atom phi >>| snd
+    (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if
+        [phi.linear_eqs] was changed as a result *)
+    let and_atom atom phi =
+      normalize_atom phi atom
+      >>= function
+      | None ->
+          Sat (false, phi)
+      | Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) ->
+          (* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so
+             they end up only on one side, hence only this match case is needed to detect linear
+             equalities *)
+          let+ phi' = solve_eq l (LinArith.of_q c) phi in
+          (true, phi')
+      | Some atom' ->
+          Sat (false, {phi with atoms= Atom.Set.add atom' phi.atoms})
+
+
+    let normalize_atoms phi =
+      let atoms0 = phi.atoms in
+      let init = Sat (false, {phi with atoms= Atom.Set.empty}) in
+      IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom ->
+          let* changed, phi = acc in
+          let+ changed', phi = and_atom atom phi in
+          (changed || changed', phi) )
+
+
+    let normalize phi =
+      (* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by
+         [normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining
+         fuel). That's ok because there's not much fuel to begin with, and as long as we're making
+         progress it's probably worth it anyway. *)
+      let rec normalize_with_fuel ~fuel phi =
+        if fuel <= 0 then (
+          L.d_printfln "ran out of fuel when normalizing" ;
+          Sat phi )
+        else
+          let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in
+          if new_linear_eqs then (
+            L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
+            normalize_with_fuel ~fuel:(fuel - 1) phi )
+          else Sat phi
+      in
+      normalize_with_fuel ~fuel:base_fuel phi
+
+
+    let and_atom atom phi = and_atom atom phi >>| snd
+
+    let implies_atom phi atom =
+      (* [φ ⊢ a] iff [φ ∧ ¬a] is inconsistent *)
+      match and_atom (Atom.nnot atom) phi with Sat _ -> false | Unsat -> true
+  end
 end
 
+(** Instead of a single formula, distinguish what we have observed to be true (coming from
+    assignments) from what we have assumed to be true (coming from conditionals). This lets us delay
+    reporting certain errors until no assumptions are needed (i.e. the issue is certain to arise
+    regardless of context). *)
+type t =
+  { known: Formula.t  (** all the things we know to be true for sure *)
+  ; pruned: Atom.Set.t  (** collection of conditions that have to be true along the path *)
+  ; both: Formula.t  (** [both = known ∧ pruned], allows us to detect contradictions *) }
+
+let ttrue = {known= Formula.ttrue; pruned= Atom.Set.empty; both= Formula.ttrue}
+
+let pp_with_pp_var pp_var fmt {known; pruned; both} =
+  F.fprintf fmt "@[known=%a,@;pruned=%a,@;both=%a@]@." (Formula.pp_with_pp_var pp_var) known
+    (Atom.Set.pp_with_pp_var pp_var) pruned (Formula.pp_with_pp_var pp_var) both
+
+
+let pp = pp_with_pp_var Var.pp
+
+let and_known_atom atom phi =
+  let open SatUnsatMonad in
+  let* known = Formula.Normalizer.and_atom atom phi.known in
+  let+ both = Formula.Normalizer.and_atom atom phi.both in
+  {phi with known; both}
+
+
 let and_mk_atom mk_atom op1 op2 phi =
-  Normalizer.and_atom (mk_atom (Term.of_operand op1) (Term.of_operand op2)) phi
+  let atom = mk_atom (Term.of_operand op1) (Term.of_operand op2) in
+  and_known_atom atom phi
 
 
 let and_equal = and_mk_atom Atom.equal
@@ -1227,22 +1263,49 @@ let and_less_equal = and_mk_atom Atom.less_equal
 let and_less_than = and_mk_atom Atom.less_than
 
 let and_equal_unop v (op : Unop.t) x phi =
-  Normalizer.and_atom (Equal (Var v, Term.of_unop op (Term.of_operand x))) phi
+  and_known_atom (Equal (Var v, Term.of_unop op (Term.of_operand x))) phi
 
 
 let and_equal_binop v (bop : Binop.t) x y phi =
-  Normalizer.and_atom (Equal (Var v, Term.of_binop bop (Term.of_operand x) (Term.of_operand y))) phi
+  and_known_atom (Equal (Var v, Term.of_binop bop (Term.of_operand x) (Term.of_operand y))) phi
 
 
 let prune_binop ~negated (bop : Binop.t) x y phi =
+  let open SatUnsatMonad in
   let tx = Term.of_operand x in
   let ty = Term.of_operand y in
   let t = Term.of_binop bop tx ty in
   let atom = if negated then Atom.Equal (t, Term.zero) else Atom.NotEqual (t, Term.zero) in
-  Normalizer.and_atom atom phi
+  let* both = Formula.Normalizer.and_atom atom phi.both in
+  let+ pruned =
+    (* Use [both] to normalize [atom] here to take previous [prune]s into account. This shouldn't
+       change whether [known |- pruned] overall, which is what we'll want to ultimately check in
+       {!has_no_assumptions}. *)
+    Formula.Normalizer.normalize_atom phi.both atom
+    >>| Option.fold ~init:phi.pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned)
+  in
+  {phi with pruned; both}
 
 
-let normalize phi = Normalizer.normalize phi
+let normalize phi =
+  let open SatUnsatMonad in
+  let* both = Formula.Normalizer.normalize phi.both in
+  let* known = Formula.Normalizer.normalize phi.known in
+  let+ pruned =
+    Atom.Set.fold
+      (fun atom pruned_sat ->
+        let* pruned = pruned_sat in
+        match Formula.Normalizer.normalize_atom known atom with
+        | Unsat ->
+            Unsat
+        | Sat None ->
+            (* normalized to [true] *) pruned_sat
+        | Sat (Some atom) ->
+            Sat (Atom.Set.add atom pruned) )
+      phi.pruned (Sat Atom.Set.empty)
+  in
+  {both; known; pruned}
+
 
 (** translate each variable in [phi_foreign] according to [f] then incorporate each fact into [phi0] *)
 let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
@@ -1255,32 +1318,56 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
   let sat_value_exn (norm : 'a normalized) =
     match norm with Unsat -> raise Contradiction | Sat x -> x
   in
-  let and_var_eqs acc =
-    VarUF.fold_congruences phi_foreign.var_eqs ~init:acc
+  let and_var_eqs var_eqs_foreign acc_phi =
+    VarUF.fold_congruences var_eqs_foreign ~init:acc_phi
       ~f:(fun (acc_f, phi) (repr_foreign, vs_foreign) ->
         let acc_f, repr = f_var acc_f (repr_foreign :> Var.t) in
         IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi)
           ~f:(fun (acc_f, phi) v_foreign ->
             let acc_f, v = f_var acc_f v_foreign in
-            let phi = Normalizer.and_var_var repr v phi |> sat_value_exn in
+            let phi = Formula.Normalizer.and_var_var repr v phi |> sat_value_exn in
             (acc_f, phi) ) )
   in
-  let and_linear_eqs acc =
-    IContainer.fold_of_pervasives_map_fold Var.Map.fold phi_foreign.linear_eqs ~init:acc
+  let and_linear_eqs linear_eqs_foreign acc_phi =
+    IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi
       ~f:(fun (acc_f, phi) (v_foreign, l_foreign) ->
         let acc_f, v = f_var acc_f v_foreign in
         let acc_f, l = LinArith.fold_subst_variables l_foreign ~init:acc_f ~f:f_subst in
-        let phi = Normalizer.and_var_linarith v l phi |> sat_value_exn in
+        let phi = Formula.Normalizer.and_var_linarith v l phi |> sat_value_exn in
         (acc_f, phi) )
   in
-  let and_atoms acc =
-    IContainer.fold_of_pervasives_set_fold Atom.Set.fold phi_foreign.atoms ~init:acc
+  let and_atoms atoms_foreign acc_phi =
+    IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi
       ~f:(fun (acc_f, phi) atom_foreign ->
         let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in
-        let phi = Normalizer.and_atom atom phi |> sat_value_exn in
+        let phi = Formula.Normalizer.and_atom atom phi |> sat_value_exn in
         (acc_f, phi) )
   in
-  try Sat (and_var_eqs (init, phi0) |> and_linear_eqs |> and_atoms) with Contradiction -> Unsat
+  let and_ phi_foreign acc phi =
+    try
+      Sat
+        ( and_var_eqs phi_foreign.Formula.var_eqs (acc, phi)
+        |> and_linear_eqs phi_foreign.Formula.linear_eqs
+        |> and_atoms phi_foreign.Formula.atoms )
+    with Contradiction -> Unsat
+  in
+  let open SatUnsatMonad in
+  let* acc, both = and_ phi_foreign.both init phi0.both in
+  let* acc, known = and_ phi_foreign.known acc phi0.known in
+  let and_pruned pruned_foreign acc_pruned =
+    IContainer.fold_of_pervasives_set_fold Atom.Set.fold pruned_foreign ~init:acc_pruned
+      ~f:(fun (acc_f, pruned) atom_foreign ->
+        let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in
+        let atom_opt = Formula.Normalizer.normalize_atom known atom |> sat_value_exn in
+        let pruned =
+          Option.fold atom_opt ~init:pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned)
+        in
+        (acc_f, pruned) )
+  in
+  let+ acc, pruned =
+    try Sat (and_pruned phi_foreign.pruned (acc, phi0.pruned)) with Contradiction -> Unsat
+  in
+  (acc, {known; pruned; both})
 
 
 (** Intermediate step of [simplify]: build an (undirected) graph between variables where an edge
@@ -1310,14 +1397,14 @@ let build_var_graph phi =
     in
     Var.Set.iter (fun v -> add_set graph v vs) vs
   in
-  Container.iter ~fold:VarUF.fold_congruences phi.var_eqs ~f:(fun ((repr : VarUF.repr), vs) ->
-      add_all (Var.Set.add (repr :> Var.t) vs) ) ;
+  Container.iter ~fold:VarUF.fold_congruences phi.Formula.var_eqs
+    ~f:(fun ((repr : VarUF.repr), vs) -> add_all (Var.Set.add (repr :> Var.t) vs)) ;
   Var.Map.iter
     (fun v l ->
       LinArith.get_variables l
       |> Seq.fold_left (fun vs v -> Var.Set.add v vs) (Var.Set.singleton v)
       |> add_all )
-    phi.linear_eqs ;
+    phi.Formula.linear_eqs ;
   (* add edges between all pairs of variables appearing in [t1] or [t2] (yes this is quadratic in
      the number of variables of these terms) *)
   let add_from_terms t1 t2 =
@@ -1331,7 +1418,7 @@ let build_var_graph phi =
     (fun atom ->
       let t1, t2 = Atom.get_terms atom in
       add_from_terms t1 t2 )
-    phi.atoms ;
+    phi.Formula.atoms ;
   graph
 
 
@@ -1364,31 +1451,50 @@ let get_reachable_from graph vs =
 let simplify ~keep phi =
   let open SatUnsatMonad in
   let+ phi = normalize phi in
-  L.d_printfln "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ;
+  L.d_printfln_escaped "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ;
   (* Get rid of atoms when they contain only variables that do not appear in atoms mentioning
-         variables in [keep], or variables appearing in atoms together with variables in [keep], and
-         so on. In other words, the variables to keep are all the ones transitively reachable from
-         variables in [keep] in the graph connecting two variables whenever they appear together in
-         a same atom of the formula. *)
-  let var_graph = build_var_graph phi in
+     variables in [keep], or variables appearing in atoms together with variables in [keep], and
+     so on. In other words, the variables to keep are all the ones transitively reachable from
+     variables in [keep] in the graph connecting two variables whenever they appear together in
+     a same atom of the formula. *)
+  (* We only consider [phi.both] when building the relation. Considering [phi.known] and
+     [phi.pruned] as well could lead to us keeping more variables around, but that's not necessarily
+     a good idea. Ignoring them means we err on the side of reporting potentially slightly more
+     issues than we would otherwise, as some atoms in [phi.pruned] may vanish unfairly as a
+     result. *)
+  let var_graph = build_var_graph phi.both in
   let vars_to_keep = get_reachable_from var_graph keep in
   L.d_printfln "Reachable vars: {%a}" Var.Set.pp vars_to_keep ;
   (* discard atoms which have variables *not* in [vars_to_keep], which in particular is enough
-         to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive
-         closure on the graph above *)
-  let var_eqs = VarUF.filter_not_in_closed_set ~keep:vars_to_keep phi.var_eqs in
-  let linear_eqs = Var.Map.filter (fun v _ -> Var.Set.mem v vars_to_keep) phi.linear_eqs in
-  let atoms = Atom.Set.filter (fun atom -> not (Atom.has_var_notin vars_to_keep atom)) phi.atoms in
-  {var_eqs; linear_eqs; atoms}
+     to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive
+     closure on the graph above *)
+  let filter_atom atom = not (Atom.has_var_notin vars_to_keep atom) in
+  let simplify_phi phi =
+    let var_eqs = VarUF.filter_not_in_closed_set ~keep:vars_to_keep phi.Formula.var_eqs in
+    let linear_eqs =
+      Var.Map.filter (fun v _ -> Var.Set.mem v vars_to_keep) phi.Formula.linear_eqs
+    in
+    let atoms = Atom.Set.filter filter_atom phi.Formula.atoms in
+    {Formula.var_eqs; linear_eqs; atoms}
+  in
+  let known = simplify_phi phi.known in
+  let both = simplify_phi phi.both in
+  let pruned = Atom.Set.filter filter_atom phi.pruned in
+  {known; pruned; both}
 
 
 let is_known_zero phi v =
-  Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs
+  Var.Map.find_opt (VarUF.find phi.both.var_eqs v :> Var.t) phi.both.linear_eqs
   |> Option.exists ~f:LinArith.is_zero
 
 
 let as_int phi v =
   let maybe_int q = if Z.equal (Q.den q) Z.one then Q.to_int q else None in
   let open Option.Monad_infix in
-  Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs
+  Var.Map.find_opt (VarUF.find phi.both.var_eqs v :> Var.t) phi.both.linear_eqs
   >>= LinArith.get_as_const >>= maybe_int
+
+
+(** test if [phi.known ⊢ phi.pruned] *)
+let has_no_assumptions phi =
+  Atom.Set.for_all (fun atom -> Formula.Normalizer.implies_atom phi.known atom) phi.pruned
diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli
index 47bc9e3f8..2e5d73c38 100644
--- a/infer/src/pulse/PulseFormula.mli
+++ b/infer/src/pulse/PulseFormula.mli
@@ -58,6 +58,8 @@ val is_known_zero : t -> Var.t -> bool
 
 val as_int : t -> Var.t -> int option
 
+val has_no_assumptions : t -> bool
+
 (** {3 Notations} *)
 
 include sig
diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index 26178cc62..3a3171856 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -516,7 +516,7 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
             |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
                    L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
                    ( Diagnostic.AccessToInvalidAddress
-                       {invalidation; invalidation_trace; access_trace}
+                       {calling_context= []; invalidation; invalidation_trace; access_trace}
                    , astate ) ) ) )
     call_state.subst (Ok call_state.astate)
 
diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml
index 114d6e918..a794be9db 100644
--- a/infer/src/pulse/PulseInvalidation.ml
+++ b/infer/src/pulse/PulseInvalidation.ml
@@ -16,7 +16,7 @@ type std_vector_function =
   | PushBack
   | Reserve
   | ShrinkToFit
-[@@deriving compare]
+[@@deriving compare, equal]
 
 let pp_std_vector_function f = function
   | Assign ->
@@ -37,7 +37,7 @@ let pp_std_vector_function f = function
       F.fprintf f "std::vector::shrink_to_fit"
 
 
-type java_iterator_function = Remove [@@deriving compare]
+type java_iterator_function = Remove [@@deriving compare, equal]
 
 let pp_java_iterator_function f = function Remove -> F.pp_print_string f "Iterator.remove"
 
@@ -50,7 +50,7 @@ type t =
   | OptionalEmpty
   | StdVector of std_vector_function
   | JavaIterator of java_iterator_function
-[@@deriving compare]
+[@@deriving compare, equal]
 
 let issue_type_of_cause = function
   | CFree ->
diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli
index e21065bc2..8fcdfbb5e 100644
--- a/infer/src/pulse/PulseInvalidation.mli
+++ b/infer/src/pulse/PulseInvalidation.mli
@@ -17,11 +17,10 @@ type std_vector_function =
   | PushBack
   | Reserve
   | ShrinkToFit
-[@@deriving compare]
 
 val pp_std_vector_function : F.formatter -> std_vector_function -> unit
 
-type java_iterator_function = Remove [@@deriving compare]
+type java_iterator_function = Remove
 
 type t =
   | CFree
@@ -32,7 +31,7 @@ type t =
   | OptionalEmpty
   | StdVector of std_vector_function
   | JavaIterator of java_iterator_function
-[@@deriving compare]
+[@@deriving compare, equal]
 
 val pp : F.formatter -> t -> unit
 
diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml
new file mode 100644
index 000000000..69f5d02da
--- /dev/null
+++ b/infer/src/pulse/PulseLatentIssue.ml
@@ -0,0 +1,32 @@
+(*
+ * 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
+
+type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriving equal]
+
+let to_diagnostic = function
+  | AccessToInvalidAddress access_to_invalid_address ->
+      Diagnostic.AccessToInvalidAddress access_to_invalid_address
+
+
+let add_call call_and_loc = function
+  | AccessToInvalidAddress access ->
+      AccessToInvalidAddress {access with calling_context= call_and_loc :: access.calling_context}
+
+
+let should_report astate = PulseArithmetic.has_no_assumptions astate
+
+let should_report_diagnostic astate (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 diag ->
+      if should_report astate then `ReportNow else `DelayReport (AccessToInvalidAddress diag)
diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli
new file mode 100644
index 000000000..ce9aa378b
--- /dev/null
+++ b/infer/src/pulse/PulseLatentIssue.mli
@@ -0,0 +1,24 @@
+(*
+ * 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
+
+(** A subset of [PulseDiagnostic] that can be "latent", i.e. there is a potential issue in the code
+    but we want to delay reporting until we see the conditions for the bug manifest themselves in
+    some calling context. *)
+
+type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriving equal]
+
+val to_diagnostic : t -> Diagnostic.t
+
+val should_report : PulseAbductiveDomain.t -> bool
+
+val should_report_diagnostic :
+  PulseAbductiveDomain.t -> Diagnostic.t -> [`ReportNow | `DelayReport of t]
+
+val add_call : CallEvent.t * Location.t -> t -> t
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index a2023e1c9..18ab3aa98 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -554,7 +554,7 @@ module GenericArrayBackedCollectionIterator = struct
         let access_trace = Trace.Immediate {location; history= snd pointer} in
         Error
           ( Diagnostic.AccessToInvalidAddress
-              {invalidation= EndIterator; invalidation_trace; access_trace}
+              {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace}
           , astate )
       else Ok astate
     in
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 309a4deb4..685fdf379 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -20,7 +20,9 @@ let check_addr_access location (address, history) astate =
   let access_trace = Trace.Immediate {location; history} in
   AddressAttributes.check_valid access_trace address astate
   |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
-         (Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace}, astate) )
+         ( Diagnostic.AccessToInvalidAddress
+             {calling_context= []; invalidation; invalidation_trace; access_trace}
+         , astate ) )
 
 
 module Closures = struct
@@ -440,9 +442,9 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit
   let apply callee_prepost ~f =
     PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals
       ~formals ~actuals astate
-    >>| function
+    >>= function
     | None ->
-        (* couldn't apply pre/post pair *) None
+        (* couldn't apply pre/post pair *) Ok None
     | Some (post, return_val_opt) ->
         let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
         let post =
@@ -452,17 +454,26 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit
           | None ->
               havoc_id (fst ret) [event] post
         in
-        Some (f post)
+        f post
   in
   let open ExecutionDomain in
   match callee_exec_state with
   | AbortProgram _ ->
-      (* Callee has failed; don't propagate the failure *)
+      (* Callee has failed; propagate the fact that a failure happened. TODO: should only do so if
+         we can apply the precondition? *)
       Ok (Some callee_exec_state)
   | ContinueProgram astate ->
-      apply astate ~f:(fun astate -> ContinueProgram astate)
+      apply astate ~f:(fun astate -> Ok (Some (ContinueProgram astate)))
   | ExitProgram astate ->
-      apply astate ~f:(fun astate -> ExitProgram astate)
+      apply astate ~f:(fun astate -> Ok (Some (ExitProgram astate)))
+  | LatentAbortProgram {astate; latent_issue} ->
+      apply astate ~f:(fun astate ->
+          let latent_issue =
+            LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
+          in
+          if LatentIssue.should_report astate then
+            Error (LatentIssue.to_diagnostic latent_issue, astate)
+          else Ok (Some (LatentAbortProgram {astate; latent_issue})) )
 
 
 let get_captured_actuals location ~captured_vars ~actual_closure astate =
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 0a5b25303..6a2afb4cc 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -385,3 +385,6 @@ let as_int phi v =
   IList.force_until_first_some
     [ lazy (CItvs.find_opt v phi.citvs |> Option.value_map ~default:None ~f:CItv.as_int)
     ; lazy (Formula.as_int phi.formula v) ]
+
+
+let has_no_assumptions phi = Formula.has_no_assumptions phi.formula
diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli
index 160c0a925..b201612ae 100644
--- a/infer/src/pulse/PulsePathCondition.mli
+++ b/infer/src/pulse/PulsePathCondition.mli
@@ -61,3 +61,6 @@ val is_unsat_expensive : t -> t * bool
 val as_int : t -> AbstractValue.t -> int option
 (** [as_int phi t] returns an integer x such that [phi |- t = x], if known for sure; see also
     [is_known_zero] *)
+
+val has_no_assumptions : t -> bool
+(** whether the current path is independent of any calling context *)
diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml
index 1ae4fe6cd..2800fdf96 100644
--- a/infer/src/pulse/PulseTrace.ml
+++ b/infer/src/pulse/PulseTrace.ml
@@ -12,7 +12,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | Immediate of {location: Location.t; history: ValueHistory.t}
   | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: t}
-[@@deriving compare]
+[@@deriving compare, equal]
 
 let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location
 
diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli
index 5795a530b..ed67b71e7 100644
--- a/infer/src/pulse/PulseTrace.mli
+++ b/infer/src/pulse/PulseTrace.mli
@@ -16,7 +16,7 @@ type t =
       ; location: Location.t  (** location of the call event *)
       ; history: ValueHistory.t  (** the call involves a value with this prior history *)
       ; in_call: t  (** last step of the trace is in a call to [f] made at [location] *) }
-[@@deriving compare]
+[@@deriving compare, equal]
 
 val pp : pp_immediate:(F.formatter -> unit) -> F.formatter -> t -> unit
 
diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml
index 3d9c94ecf..3d7c33b70 100644
--- a/infer/src/pulse/PulseValueHistory.ml
+++ b/infer/src/pulse/PulseValueHistory.ml
@@ -19,7 +19,7 @@ type event =
   | VariableAccessed of Pvar.t * Location.t
   | VariableDeclared of Pvar.t * Location.t
 
-and t = event list [@@deriving compare]
+and t = event list [@@deriving compare, equal]
 
 let pp_event_no_location fmt event =
   let pp_pvar fmt pvar =
diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli
index 56db0dc5e..84c12af0a 100644
--- a/infer/src/pulse/PulseValueHistory.mli
+++ b/infer/src/pulse/PulseValueHistory.mli
@@ -19,7 +19,7 @@ type event =
   | VariableAccessed of Pvar.t * Location.t
   | VariableDeclared of Pvar.t * Location.t
 
-and t = event list [@@deriving compare]
+and t = event list [@@deriving compare, equal]
 
 val pp : F.formatter -> t -> unit
 
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
index bcf3fb964..67753dd45 100644
--- a/infer/src/pulse/unit/PulseFormulaTest.ml
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -130,7 +130,10 @@ let%test_module "normalization" =
   ( module struct
     let%expect_test _ =
       normalize (x < y) ;
-      [%expect {|true (no var=var) && true (no linear) && {[x + -y] < 0}|}]
+      [%expect
+        {|
+        known=true (no var=var) && true (no linear) && {[x + -y] < 0}, pruned=true (no atoms),
+        both=true (no var=var) && true (no linear) && {[x + -y] < 0}|}]
 
     let%expect_test _ =
       normalize (x + i 1 - i 1 < x) ;
@@ -160,7 +163,10 @@ let%test_module "normalization" =
 
     let%expect_test _ =
       normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
-      [%expect {|true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no atoms)|}]
+      [%expect
+        {|
+        known=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no atoms)|}]
 
     let%expect_test _ =
       normalize (x = i 0 && x < i 0) ;
@@ -174,77 +180,131 @@ let%test_module "normalization" =
       normalize (z * (x + (v * y) + i 1) / w = i 0) ;
       [%expect
         {|
-        true (no var=var)
-        &&
-        x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
-        &&
-        {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]} |}]
+        known=true (no var=var)
+              &&
+              x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
+              &&
+              {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]},
+        pruned=true (no atoms),
+        both=true (no var=var)
+             &&
+             x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
+             &&
+             {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]} |}]
 
     (* check that this becomes all linear equalities *)
     let%expect_test _ =
       normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ;
       [%expect
         {|
-        true (no var=var)
-        &&
-        x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
-        &&
-        true (no atoms)|}]
+        known=true (no var=var)
+              &&
+              x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+              &&
+              true (no atoms),
+        pruned=true (no atoms),
+        both=true (no var=var)
+             &&
+             x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+             &&
+             true (no atoms)|}]
 
     (* check that this becomes all linear equalities thanks to constant propagation *)
     let%expect_test _ =
       normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ;
       [%expect
         {|
-        true (no var=var)
-        &&
-        x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
-         ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
-        &&
-        true (no atoms)|}]
+        known=true (no var=var)
+              &&
+              x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
+               ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+              &&
+              true (no atoms),
+        pruned=true (no atoms),
+        both=true (no var=var)
+             &&
+             x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
+              ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+             &&
+             true (no atoms)|}]
   end )
 
 let%test_module "variable elimination" =
   ( module struct
     let%expect_test _ =
       simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
-      [%expect {|true (no var=var) && x = 0 && true (no atoms)|}]
+      [%expect
+        {|
+        known=true (no var=var) && x = 0 && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 0 && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ;
-      [%expect {|x=v6 && x = 0 && true (no atoms)|}]
+      [%expect
+        {|
+          known=x=v6 && x = 0 && true (no atoms), pruned=true (no atoms),
+          both=x=v6 && x = 0 && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ;
-      [%expect {|true (no var=var) && y = -1 && true (no atoms)|}]
+      [%expect
+        {|
+        known=true (no var=var) && y = -1 && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && y = -1 && true (no atoms)|}]
 
     (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *)
     let%expect_test _ =
       simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ;
-      [%expect {|x=v6 ∧ z=w=v7 && x = y -1 ∧ z = -1 && true (no atoms)|}]
+      [%expect
+        {|
+        known=x=v6 ∧ z=w=v7 && x = y -1 ∧ z = -1 && true (no atoms), pruned=true (no atoms),
+        both=x=v6 ∧ z=w=v7 && x = y -1 ∧ z = -1 && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ;
       [%expect
-        {|x=v6 ∧ v=v9 && x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1 && true (no atoms)|}]
+        {|
+          known=x=v6 ∧ v=v9
+                &&
+                x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1
+                &&
+                true (no atoms),
+          pruned=true (no atoms),
+          both=x=v6 ∧ v=v9
+               &&
+               x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1
+               &&
+               true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ;
-      [%expect {|x=w=v6 ∧ y=z && x = y +4 && true (no atoms)|}]
+      [%expect
+        {|
+        known=x=w=v6 ∧ y=z && x = y +4 && true (no atoms), pruned=true (no atoms),
+        both=x=w=v6 ∧ y=z && x = y +4 && true (no atoms)|}]
   end )
 
 let%test_module "non-linear simplifications" =
   ( module struct
     let%expect_test "zero propagation" =
       simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ;
-      [%expect {|true (no var=var) && w = 0 && true (no atoms)|}]
+      [%expect
+        {|
+        known=true (no var=var) && w = 0 && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && w = 0 && true (no atoms)|}]
 
     let%expect_test "constant propagation: bitshift" =
       simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ;
-      [%expect {|true (no var=var) && x = 4 && true (no atoms)|}]
+      [%expect
+        {|
+        known=true (no var=var) && x = 4 && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 4 && true (no atoms)|}]
 
     let%expect_test "non-linear becomes linear" =
       normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ;
       [%expect
-        {|z=v8 ∧ w=v7 && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && true (no atoms)|}]
+        {|
+          known=z=v8 ∧ w=v7 && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && true (no atoms),
+          pruned=true (no atoms),
+          both=z=v8 ∧ w=v7 && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && true (no atoms)|}]
   end )
diff --git a/infer/tests/codetoanalyze/cpp/pulse/Makefile b/infer/tests/codetoanalyze/cpp/pulse/Makefile
index a479a7f50..fce546ad8 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/Makefile
+++ b/infer/tests/codetoanalyze/cpp/pulse/Makefile
@@ -7,7 +7,8 @@ TESTS_DIR = ../../..
 
 # see explanations in cpp/biabduction/Makefile for the custom isystem
 CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
-INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
+  --pulse-report-latent-issues
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.cpp)
diff --git a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
index fc28c52e3..1121a6d0f 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
@@ -28,7 +28,11 @@ void call_ifnotthenderef_false_null_bad() { ifnotthenderef(false, nullptr); }
 // should be FN given the current "all allocated addresses are assumed
 // disjoint unless specified otherwise" but we detect the bug because
 // we don't propagate pure equalities that we discover to the heap part
-void alias_null_deref_bad(int* x, int* y) {
+//
+// Well, at the moment it *is* FN but because we mark the issue
+// "latent" because the "if" test is not conclusively true. This is
+// also ok.
+void alias_null_deref_latent(int* x, int* y) {
   *x = 32;
   *y = 52;
   if (x == y) {
diff --git a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp
index d911a2a07..c64321908 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp
@@ -53,7 +53,7 @@ void aggregate_reassign3_ok() {
   }
 }
 
-int multiple_invalidations_branch_bad(int n, int* ptr) {
+int multiple_invalidations_branch_latent(int n, int* ptr) {
   if (n == 7) {
     delete ptr;
   } else {
@@ -62,7 +62,7 @@ int multiple_invalidations_branch_bad(int n, int* ptr) {
   return *ptr;
 }
 
-int multiple_invalidations_loop_bad(int n, int* ptr) {
+int multiple_invalidations_loop_latent(int n, int* ptr) {
   for (int i = 0; i < n; i++) {
     if (i == 7) {
       delete ptr;
diff --git a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp
index 95e288ff1..bac6520c2 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp
@@ -79,7 +79,7 @@ void add_test2_ok(int* x, int y, int z) {
   }
 }
 
-void add_test3_bad(int* x, int y, int z) {
+void add_test3_latent(int* x, int y, int z) {
   free(x);
   if (y > 2 && y + z > 5) { // sometimes true
     *x = 42;
@@ -95,7 +95,7 @@ void add_test4_bad_FN(int* x) {
   *x = 42;
 }
 
-void add_test5_bad(int* x, int n) {
+void add_test5_latent(int* x, int n) {
   free(x);
   // the unknown bound is treated non-deterministically, good thing here
   for (int i = 0; i < n; i++) {
diff --git a/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp b/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp
index 9b588dd71..0c75bfd62 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp
@@ -26,4 +26,4 @@ void store_exit(int* x, bool b) {
   }
 }
 
-void store_exit_null_bad(bool b) { store_exit(NULL, b); }
+void store_exit_null_bad() { store_exit(NULL, true); }
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 980d1fe01..df3d5f4f3 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,11 +1,11 @@
-codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_latent, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here]
 codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here]
 codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 8, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator()` here,parameter `s` of call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_std_fun_constructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator()` here,parameter `s` of call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator(),invalid access occurs here]
@@ -23,8 +23,8 @@ codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_ref_bad, 7, NULLPTR_DERE
 codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_bad, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_ok_FP, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `update_inside_lambda_as_argument`,return from call to `update_inside_lambda_as_argument`,invalid access occurs here]
-codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test3_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_latent, 5, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test5_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here]
@@ -39,8 +39,9 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_nullptr`,return from call to `may_return_nullptr`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
@@ -50,6 +51,8 @@ codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_b
 codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is folly::None,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::Optional(arg)` (modelled),return from call to `folly::Optional::Optional(arg)` (modelled),passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is folly::None,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, operator_arrow_bad, 0, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is folly::None,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional<State>::operator->`,return from call to `folly::Optional<State>::operator->`,invalid access occurs here]
+codetoanalyze/cpp/pulse/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/path.cpp, only_bad_on_42_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here]
@@ -71,12 +74,12 @@ codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_
 codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_latent, 4, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,passed as argument to `<placement new>()` (modelled),return from call to `<placement new>()` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]
@@ -94,7 +97,7 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AF
 codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_ok, 7, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
@@ -104,13 +107,13 @@ codetoanalyze/cpp/pulse/vector.cpp, deref_vector_pointer_element_after_push_back
 codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of insert_bad,was potentially invalidated by `std::vector::insert()`,use-after-lifetime part of the trace starts here,parameter `vec` of insert_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_latent, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),invalid access occurs here]
+codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_latent, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_next_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_read_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
-codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_bad, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
+codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_latent, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_latent,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_prev_after_emplace_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_prev_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_read_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/join.cpp b/infer/tests/codetoanalyze/cpp/pulse/join.cpp
index b980a3e62..d23744073 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/join.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/join.cpp
@@ -22,7 +22,7 @@ struct list {
   struct foo* foo;
 };
 
-int invalidate_node_alias_bad(struct list* head, int cond) {
+int invalidate_node_alias_latent(struct list* head, int cond) {
   int* result = 0;
   struct list* x = head;
   if (cond) {
@@ -37,6 +37,10 @@ int invalidate_node_alias_bad(struct list* head, int cond) {
   return *result;
 }
 
+int invalidate_node_alias_bad(struct list* head) {
+  invalidate_node_alias_latent(head, true);
+}
+
 void list_delete_ok(struct list** l) {
   auto head = *l;
   *l = nullptr;
diff --git a/infer/tests/codetoanalyze/cpp/pulse/path.cpp b/infer/tests/codetoanalyze/cpp/pulse/path.cpp
new file mode 100644
index 000000000..a634b6c68
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/pulse/path.cpp
@@ -0,0 +1,22 @@
+/*
+ * 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.
+ */
+
+int* may_return_null(int x) {
+  if (x == 42) {
+    return nullptr;
+  }
+  return new int();
+}
+
+void only_bad_on_42_latent(int x) {
+  int* p = may_return_null(x);
+  *p = 12;
+}
+
+void faulty_call_bad() { only_bad_on_42_latent(42); }
+
+void call_not_with_42_ok() { only_bad_on_42_latent(41); }
diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp
index 6cf1d9314..40cd22b24 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp
@@ -52,7 +52,7 @@ void double_delete_bad() {
   delete s;
 }
 
-void delete_in_branch_bad(bool b) {
+void delete_in_branch_latent(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;
@@ -69,7 +69,7 @@ void delete_in_branch_ok(bool b) {
   }
 }
 
-void use_in_branch_bad(bool b) {
+void use_in_branch_latent(bool b) {
   auto s = new Simple{1};
   delete s;
   if (b) {
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
index ce2a95785..3a9dee0a6 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
@@ -71,16 +71,17 @@ void reserve_then_push_back_loop_ok(std::vector<int>& vec,
   std::cout << *elt << "\n";
 }
 
-void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
+void FP_init_fill_then_push_back_ok(std::vector<int>& vec_other) {
   std::vector<int> vec(vec_other.size());
   int* elt = &vec[1];
-  for (const auto& i : vec_other) {
-    vec.push_back(i);
-  }
+  vec.push_back(0);
+  vec.push_back(0);
+  vec.push_back(0);
+  vec.push_back(0);
   std::cout << *elt << "\n";
 }
 
-void push_back_loop_bad(std::vector<int>& vec_other) {
+void push_back_loop_latent(std::vector<int>& vec_other) {
   std::vector<int> vec(2);
   int* elt = &vec[1];
   for (const auto& i : vec_other) {
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp
index 4e7955c3a..acdca06d0 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp
@@ -36,7 +36,7 @@ void read_iterator_loop_ok(std::vector<int>& vec) {
   }
 }
 
-void iterator_next_after_emplace_loop_bad(std::vector<int>& vec) {
+void iterator_next_after_emplace_loop_latent(std::vector<int>& vec) {
   int sum = 0;
   for (auto iter = vec.begin(); iter != vec.end(); ++iter) {
     int elem = *iter;
@@ -46,7 +46,7 @@ void iterator_next_after_emplace_loop_bad(std::vector<int>& vec) {
   }
 }
 
-void iterator_after_push_back_loop_bad(std::vector<int>& vec_other) {
+void iterator_after_push_back_loop_latent(std::vector<int>& vec_other) {
   std::vector<int> vec(2);
   auto iter_begin = vec.begin();
   auto iter_end = vec.end();
diff --git a/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java b/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java
index dd4352bbc..aae3123ea 100644
--- a/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java
+++ b/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java
@@ -45,7 +45,7 @@ public class DefaultInInterface {
     }
   }
 
-  static void uncertainCallMethod1NPE(int i) {
+  static void uncertainCallMethod1NPE_latent(int i) {
     A aAorB = new A();
     if (i > 0) { // feasible path
       aAorB = new B();
diff --git a/infer/tests/codetoanalyze/java/pulse/Makefile b/infer/tests/codetoanalyze/java/pulse/Makefile
index 636a8e4ba..e146b8265 100644
--- a/infer/tests/codetoanalyze/java/pulse/Makefile
+++ b/infer/tests/codetoanalyze/java/pulse/Makefile
@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-INFER_OPTIONS = --pulse-only --debug-exceptions
+INFER_OPTIONS = --pulse-only --debug-exceptions --pulse-report-latent-issues
 INFERPRINT_OPTIONS = --issues-tests
 SOURCES = $(wildcard *.java)
 
diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp
index 7509df621..c12072be8 100644
--- a/infer/tests/codetoanalyze/java/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/java/pulse/issues.exp
@@ -1,6 +1,6 @@
 codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$A.defaultCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$B.overridenCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE_latent(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Supertype.bar()`,return from call to `Object DynamicDispatch$Supertype.bar()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]