diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml
index e0c0f987c..0e7db7e62 100644
--- a/infer/src/IR/HilExp.ml
+++ b/infer/src/IR/HilExp.ml
@@ -631,3 +631,27 @@ and eval = function
 
 
 let rec ignore_cast e = match e with Cast (_, e) -> ignore_cast e | _ -> e
+
+let access_expr_of_exp ~include_array_indexes ~f_resolve_id exp typ =
+  match ignore_cast (of_sil ~include_array_indexes ~f_resolve_id ~add_deref:true exp typ) with
+  | AccessExpression access_expr ->
+      Some access_expr
+  | BinaryOperator (_, exp0, exp1) -> (
+    (* pointer arithmetic. somewhere in one of the expressions, there should be at least
+               one pointer type represented as an access path. just use that access path and forget
+               about the arithmetic. if you need to model this more precisely, you should be using
+               SIL instead *)
+    match get_access_exprs exp0 with
+    | ap :: _ ->
+        Some ap
+    | [] -> (
+      match get_access_exprs exp1 with ap :: _ -> Some ap | [] -> None ) )
+  | Constant (Const.Cint i) ->
+      (* this can happen in intentionally crashing code like *0xdeadbeef = 0 used for
+               debugging. doesn't really matter what we do here, so just create a dummy var *)
+      let dummy_base_var =
+        Var.of_id (Ident.create_normal (Ident.string_to_name (IntLit.to_string i)) 0)
+      in
+      Some (AccessExpression.base (dummy_base_var, Typ.void_star))
+  | _ ->
+      None
diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli
index 8b3dc6c8e..1bec37c9e 100644
--- a/infer/src/IR/HilExp.mli
+++ b/infer/src/IR/HilExp.mli
@@ -41,6 +41,8 @@ and access_expression = private
 [@@deriving compare]
 
 module AccessExpression : sig
+  val of_id : Ident.t -> Typ.t -> access_expression
+
   val base : AccessPath.base -> access_expression
 
   val field_offset : access_expression -> Typ.Fieldname.t -> access_expression
@@ -121,3 +123,12 @@ val is_int_zero : t -> bool
 val eval : t -> Const.t option
 
 val ignore_cast : t -> t
+
+val access_expr_of_exp :
+     include_array_indexes:bool
+  -> f_resolve_id:(Var.t -> AccessExpression.t option)
+  -> Exp.t
+  -> Typ.t
+  -> access_expression option
+(** best effort translating a SIL expression to an access path, not semantics preserving in
+    particular in the presence of pointer arithmetic *)
diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml
index d5acda020..594079274 100644
--- a/infer/src/IR/HilInstr.ml
+++ b/infer/src/IR/HilInstr.ml
@@ -73,35 +73,12 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) =
       analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc
   | Store (lhs_exp, typ, rhs_exp, loc) ->
       let lhs_access_expr =
-        match HilExp.ignore_cast (exp_of_sil ~add_deref:true lhs_exp typ) with
-        | HilExp.AccessExpression access_expr ->
+        match HilExp.access_expr_of_exp ~include_array_indexes ~f_resolve_id lhs_exp typ with
+        | Some access_expr ->
             access_expr
-        | BinaryOperator (_, exp0, exp1) -> (
-          (* pointer arithmetic. somewhere in one of the expressions, there should be at least
-               one pointer type represented as an access path. just use that access path and forget
-               about the arithmetic. if you need to model this more precisely, you should be using
-               SIL instead *)
-          match HilExp.get_access_exprs exp0 with
-          | ap :: _ ->
-              ap
-          | [] -> (
-            match HilExp.get_access_exprs exp1 with
-            | ap :: _ ->
-                ap
-            | [] ->
-                L.(die InternalError)
-                  "Invalid pointer arithmetic expression %a used as LHS at %a" Exp.pp lhs_exp
-                  Location.pp_file_pos loc ) )
-        | HilExp.Constant (Const.Cint i) ->
-            (* this can happen in intentionally crashing code like *0xdeadbeef = 0 used for
-               debugging. doesn't really matter what we do here, so just create a dummy var *)
-            let dummy_base_var =
-              Var.of_id (Ident.create_normal (Ident.string_to_name (IntLit.to_string i)) 0)
-            in
-            HilExp.AccessExpression.base (dummy_base_var, Typ.void_star)
-        | _ ->
-            L.(die InternalError)
-              "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp Location.pp_file_pos loc
+        | None ->
+            L.die InternalError "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp
+              Location.pp_file_pos loc
       in
       Instr (Assign (lhs_access_expr, exp_of_sil rhs_exp typ, loc))
   | Call ((ret_id, ret_typ), call_exp, formals, loc, call_flags) ->
diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml
index b33f04009..c320dd488 100644
--- a/infer/src/absint/TransferFunctions.ml
+++ b/infer/src/absint/TransferFunctions.ml
@@ -48,18 +48,12 @@ module type DisjReady = sig
 
   type extras
 
-  type instr
-
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t list
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t list
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
 
-module type HILDisjReady = sig
-  include DisjReady with type instr := HilInstr.t
-end
-
-module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) = struct
+module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveConfig) = struct
   module CFG = TransferFunctions.CFG
 
   type extras = TransferFunctions.extras
diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli
index a5d52d89d..8f927f8d2 100644
--- a/infer/src/absint/TransferFunctions.mli
+++ b/infer/src/absint/TransferFunctions.mli
@@ -55,22 +55,16 @@ module type DisjReady = sig
 
   type extras
 
-  type instr
-
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t list
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t list
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
 
-module type HILDisjReady = sig
-  include DisjReady with type instr := HilInstr.t
-end
-
 (** In the disjunctive interpreter, the domain is a set of abstract states representing a
    disjunction between these states. The transfer functions are executed on each state in the
    disjunct independently. The join on the disjunctive state is governed by the policy described in
    [DConfig]. *)
-module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) : sig
+module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveConfig) : sig
   module Disjuncts : sig
     type t
 
@@ -80,7 +74,7 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct
   end
 
   include
-    HIL
+    SIL
     with type extras = TransferFunctions.extras
      and module CFG = TransferFunctions.CFG
      and type Domain.t = Disjuncts.t
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 58a3f5d6b..e6df1c7aa 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -77,21 +77,24 @@ module PulseTransferFunctions = struct
         >>= PulseOperations.havoc [crumb] loc lhs_access
 
 
-  let exec_unknown_call _summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags
+  let exec_unknown_call _summary ret (call : HilInstr.call) (actuals : HilExp.t list) _flags
       call_loc astate =
     let read_all args astate =
       PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
     in
     let crumb = ValueHistory.Call {f= `HilCall call; actuals; location= call_loc} in
+    let havoc_ret (ret, _) astate = PulseOperations.havoc_var [crumb] ret astate in
+    let read_actuals_havoc_ret actuals ret astate = read_all actuals astate >>| havoc_ret ret in
     match call with
     | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> (
         L.d_printfln "constructor call detected@." ;
         match actuals with
         | AccessExpression constructor_access :: rest ->
             let constructed_object = HilExp.AccessExpression.dereference constructor_access in
-            PulseOperations.havoc [crumb] call_loc constructed_object astate >>= read_all rest
+            PulseOperations.havoc [crumb] call_loc constructed_object astate
+            >>= read_actuals_havoc_ret rest ret
         | _ ->
-            Ok astate )
+            Ok (havoc_ret ret astate) )
     | Direct (Typ.Procname.ObjC_Cpp callee_pname)
       when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> (
         L.d_printfln "operator= detected@." ;
@@ -101,12 +104,13 @@ module PulseTransferFunctions = struct
             let lhs_deref = HilExp.AccessExpression.dereference lhs in
             let rhs_deref = HilExp.AccessExpression.dereference rhs in
             PulseOperations.havoc [crumb] call_loc lhs_deref astate
-            >>= fun astate -> PulseOperations.read call_loc rhs_deref astate >>| fst
+            >>= fun astate ->
+            PulseOperations.read call_loc rhs_deref astate >>| fst >>| havoc_ret ret
         | _ ->
-            read_all actuals astate )
+            read_actuals_havoc_ret actuals ret astate )
     | _ ->
         L.d_printfln "skipping unknown procedure@." ;
-        read_all actuals astate
+        read_actuals_havoc_ret actuals ret astate
 
 
   let interprocedural_call caller_summary ret (call : HilInstr.call) (actuals : HilExp.t list)
@@ -191,20 +195,57 @@ module PulseTransferFunctions = struct
             posts )
 
 
-  let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t) =
+  let hil_of_sil ?(add_deref = false) exp typ =
+    HilExp.of_sil ~include_array_indexes:true ~f_resolve_id:(fun _ -> None) ~add_deref exp typ
+
+
+  let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : Sil.instr) =
     match instr with
-    | Assign (lhs_access, rhs_exp, loc) ->
-        let post = exec_assign summary lhs_access rhs_exp loc astate |> check_error summary in
+    | Load (lhs_id, rhs_exp, typ, loc) ->
+        let lhs_access = HilExp.AccessExpression.of_id lhs_id typ in
+        let rhs_hexp = hil_of_sil ~add_deref:true rhs_exp typ in
+        let post = exec_assign summary lhs_access rhs_hexp loc astate |> check_error summary in
+        [post]
+    | Store (lhs_exp, typ, rhs_exp, loc) ->
+        let lhs_access_expr =
+          match
+            HilExp.access_expr_of_exp ~include_array_indexes:true
+              ~f_resolve_id:(fun _ -> None)
+              lhs_exp typ
+          with
+          | Some access_expr ->
+              access_expr
+          | None ->
+              L.die InternalError "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp
+                Location.pp_file_pos loc
+        in
+        let rhs_hexp = hil_of_sil rhs_exp typ in
+        let post =
+          exec_assign summary lhs_access_expr rhs_hexp loc astate |> check_error summary
+        in
         [post]
-    | Assume (condition, _, _, loc) ->
+    | Prune (condition, loc, _is_then_branch, _if_kind) ->
+        let condition_hexp = hil_of_sil condition (Typ.mk (Tint IBool)) in
         let post =
-          PulseOperations.read_all loc (HilExp.get_access_exprs condition) astate
+          PulseOperations.read_all loc (HilExp.get_access_exprs condition_hexp) astate
           |> check_error summary
         in
         [post]
-    | Call (ret, call, actuals, flags, loc) ->
+    | Call ((ret_id, ret_typ), call_exp, actuals, loc, call_flags) ->
+        let ret_hil = (Var.of_id ret_id, ret_typ) in
+        let call_hil =
+          match hil_of_sil call_exp (Typ.mk Tvoid) with
+          | Constant (Cfun procname) | Closure (procname, _) ->
+              HilInstr.Direct procname
+          | HilExp.AccessExpression access_expr ->
+              HilInstr.Indirect access_expr
+          | call_exp ->
+              L.(die InternalError) "Unexpected call expression %a" HilExp.pp call_exp
+        in
+        let actuals_hil = List.map ~f:(fun (exp, typ) -> hil_of_sil exp typ) actuals in
         let posts =
-          dispatch_call summary ret call actuals flags loc astate |> check_error summary
+          dispatch_call summary ret_hil call_hil actuals_hil call_flags loc astate
+          |> check_error summary
         in
         posts
     | Metadata (ExitScope (vars, _)) ->
@@ -221,10 +262,8 @@ module PulseTransferFunctions = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
 end
 
-module HilConfig = LowerHil.DefaultConfig
-
 module DisjunctiveTransferFunctions =
-  TransferFunctions.MakeHILDisjunctive
+  TransferFunctions.MakeDisjunctive
     (PulseTransferFunctions)
     (struct
       let join_policy =
@@ -234,9 +273,7 @@ module DisjunctiveTransferFunctions =
       let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold
     end)
 
-module DisjunctiveAnalyzer =
-  LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (HilConfig)
-    (DisjunctiveTransferFunctions)
+module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFunctions)
 
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 5549dfa13..bc91ee602 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,47 +1,47 @@
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `*ptr` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `ptr` 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,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `a->f` 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,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `a->f` 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,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `a->f` here]
-codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `a->f` here]
-codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `this` here,use-after-lifetime part of the trace starts here,invalid access to `this` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `y`,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,assigned to `z`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` 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,assigned to `y`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,when calling `call_store()` here,when calling `store()` here,invalid access to `y->p` here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `result`,memory was invalidated by `delete` on `result` here,use-after-lifetime part of the trace starts here,assigned to `result`,invalid access to `*result` 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,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `this->b` here,use-after-lifetime part of the trace starts here,assigned to `this->b`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access to `rw.b->f` 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,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,returned from call to `getwrapperStack()`,invalid access to `rw.b->f` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `*n$0` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$6`,memory was invalidated by `delete` on `n$6` here,use-after-lifetime part of the trace starts here,assigned to `n$6`,invalid access to `n$6` 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,assigned to `n$0`,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$2`,when calling `templated_wrapper_access_ok` here,invalid access to `n$0->f` 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,assigned to `n$0`,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$2`,when calling `templated_wrapper_access_ok` here,invalid access to `n$0->f` 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,assigned to `n$0`,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,assigned to `n$1`,when calling `deduplication::templated_access_function` here,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$0`,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,assigned to `n$1`,when calling `deduplication::templated_access_function` here,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `n$0` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$5`,assigned to `y`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$4`,assigned to `z`,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$0`,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$0`,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `n$2`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `n$0`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,assigned to `n$0`,when calling `call_store()` here,when calling `store()` here,invalid access to `n$0->p` here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$13`,assigned to `result`,assigned to `n$9`,memory was invalidated by `delete` on `n$9` here,use-after-lifetime part of the trace starts here,assigned to `n$13`,assigned to `result`,assigned to `n$0`,invalid access to `*n$0` 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,assigned to `n$3`,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,assigned to `n$3`,assigned to `n$1->b`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,assigned to `n$0`,invalid access to `n$0->f` 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,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,returned from call to `getwrapperStack()`,invalid access to `n$0->f` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `y`,returned 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,invalid access to `s->f` 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,invalid access to `s` 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,when calling `Simple` here,invalid access to `__param_0->f` 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,invalid access to `s` 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,invalid access to `s->f` 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,when calling `Simple` here,invalid access to `__param_0->f` 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,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,invalid access to `s->f` 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,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `this->f` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `this->f` 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,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,memory was invalidated by `delete` on `alias` here,use-after-lifetime part of the trace starts here,assigned to `s`,invalid access to `s->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalid access to `alias->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,assigned to `s`,assigned to `alias`,invalid access to `alias->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `this->f` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `this->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `this->f` here,use-after-lifetime part of the trace starts here,assigned to `this->f`,returned from call to `use_after_destructor::S::S()`,invalid access to `*(s.f)` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `this->f` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `this->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,invalid access to `pc->f` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` on `global_pointer` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `global_pointer` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `x` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `*x` here]
-codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,invalid access to `*y` here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
-codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `n$0`,returned here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `n$1`,assigned to `y`,assigned to `n$0`,returned 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,invalid access to `n$2` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$3`,when calling `Simple` here,invalid access to `n$2->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$1`,memory was invalidated by `delete` on `n$1` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$8`,memory was invalidated by `delete` on `n$8` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$4`,when calling `Simple` here,invalid access to `n$2->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,invalid access to `n$2->f` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `n$3` 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,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$4`,returned from call to `<placement new>(sizeof(use_after_destructor::S),n$4)`,assigned to `alias`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$4`,returned from call to `<placement new>(sizeof(use_after_destructor::S),n$4)`,assigned to `alias`,assigned to `n$0`,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$7`,assigned to `alias`,assigned to `n$0`,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `n$3` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(int))`,assigned to `n$3->f`,returned from call to `use_after_destructor::S::S()`,assigned to `n$8`,invalid access to `*n$8` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `n$3` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,invalid access to `n$0->f` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$0`,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` on `n$0` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `n$0` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$2`,memory was invalidated by call to `free()` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `n$0` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$2`,memory was invalidated by call to `free()` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `*n$0` here]
+codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$10,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$9,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$11,(unsigned long) 1)`,assigned to `elt`,assigned to `n$9`,assigned to `y`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$10,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$21,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$21,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$12,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$9,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
index f215a8d18..b345fca87 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
@@ -58,7 +58,7 @@ void reserve_then_push_back_loop_ok(std::vector<int>& vec,
   std::cout << *elt << "\n";
 }
 
-void init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
+void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
   std::vector<int> vec(vec_other.size());
   int* elt = &vec[1];
   for (const auto& i : vec_other) {