diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 5de1f0df5..0ee0a56f5 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -245,10 +245,10 @@ module DisjunctiveAnalyzer =
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in
   AbstractAddress.init () ;
-  match
-    DisjunctiveAnalyzer.compute_post proc_data
-      ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty)
-  with
+  let initial =
+    DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial proc_desc)
+  in
+  match DisjunctiveAnalyzer.compute_post proc_data ~initial with
   | Some posts ->
       Payload.update_summary
         (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts))
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index a0e8a9264..3279cb38c 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -86,8 +86,9 @@ let ( <= ) ~lhs ~rhs =
 
 
 module Stack = struct
-  let is_abducible _var =
-    (* TODO: need to keep only formals + return variable + globals in the pre *) true
+  let is_abducible astate var =
+    (* HACK: formals are pre-registered in the initial state *)
+    BaseStack.mem var (astate.pre :> base_domain).stack || Var.is_global var
 
 
   (** [astate] with [astate.post.stack = f astate.post.stack] *)
@@ -104,7 +105,9 @@ module Stack = struct
         let addr_loc_opt' = (AbstractAddress.mk_fresh (), None) in
         let post_stack = BaseStack.add var addr_loc_opt' (astate.post :> base_domain).stack in
         let pre =
-          if is_abducible var then
+          (* do not overwrite values of variables already in the pre *)
+          if (not (BaseStack.mem var (astate.pre :> base_domain).stack)) && is_abducible astate var
+          then
             let foot_stack = BaseStack.add var addr_loc_opt' (astate.pre :> base_domain).stack in
             let foot_heap =
               BaseMemory.register_address (fst addr_loc_opt') (astate.pre :> base_domain).heap
@@ -120,8 +123,12 @@ module Stack = struct
 
 
   let remove_vars vars astate =
+    let vars_to_remove =
+      let is_in_pre var astate = BaseStack.mem var (astate.pre :> base_domain).stack in
+      List.filter vars ~f:(fun var -> not (is_in_pre var astate))
+    in
     map_post_stack astate ~f:(fun stack ->
-        BaseStack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars var)) stack )
+        BaseStack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars_to_remove var)) stack )
 
 
   let fold f astate accum = BaseStack.fold f (astate.post :> base_domain).stack accum
@@ -206,7 +213,31 @@ module Memory = struct
   module Edges = BaseMemory.Edges
 end
 
-let empty = {post= Domain.empty; pre= InvertedDomain.empty}
+let mk_initial proc_desc =
+  (* HACK: save the formals in the stacks of the pre and the post to remember which local variables
+     correspond to formals *)
+  let formals =
+    let proc_name = Procdesc.get_proc_name proc_desc in
+    let location = Some (Procdesc.get_loc proc_desc) in
+    Procdesc.get_formals proc_desc
+    |> List.map ~f:(fun (mangled, _) ->
+           let var = Var.of_pvar (Pvar.mk mangled proc_name) in
+           (var, (AbstractAddress.mk_fresh (), location)) )
+  in
+  let initial_stack =
+    List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack
+      ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack)
+  in
+  let pre =
+    let initial_heap =
+      List.fold formals ~init:(InvertedDomain.empty :> base_domain).heap
+        ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap)
+    in
+    InvertedDomain.make initial_stack initial_heap
+  in
+  let post = Domain.update ~stack:initial_stack Domain.empty in
+  {pre; post}
+
 
 let discard_unreachable ({pre; post} as astate) =
   let pre_addresses = PulseDomain.visit (pre :> PulseDomain.t) in
@@ -542,9 +573,7 @@ module PrePost = struct
 
   let record_post_for_return callee_proc_name call_loc pre_post ~ret call_state =
     let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in
-    match
-      PulseDomain.Stack.find_opt return_var (pre_post.pre :> PulseDomain.t).PulseDomain.stack
-    with
+    match PulseDomain.Stack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with
     | Some (addr_return, _) ->
         record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_return
           ~addr_caller:(fst ret) call_state
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index f8d9ce2f6..9b06367e4 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -16,7 +16,7 @@ module Attributes = PulseDomain.Attributes
 
 include AbstractDomain.NoJoin
 
-val empty : t
+val mk_initial : Procdesc.t -> t
 
 (** stack operations like {!PulseDomain.Stack} but that also take care of propagating facts to the
     precondition *)
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index b478adaf0..33b6df5b2 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -10,6 +10,8 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `wraps_delete()` here,invalidated by during call to `wraps_delete_inner()` here,invalidated by `delete` on `x` here,start of use after lifetime trace,accessed during call to `wraps_read()` here,accessed during call to `wraps_read_inner()` here,accessed `x->f` here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `may_return_invalid_ptr_ok()` here,invalidated by `delete` on `y` here,start of use after lifetime trace,accessed during call to `call_store()` here,accessed during call to `store()` here,accessed `y->p` here,start of value trace,assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `result` here,start of use after lifetime trace,accessed `*(result)` here,start of value trace,assigned to `result`]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `getwrapperHeap()` here,invalidated by during call to `~WrapsB` here,invalidated by during call to `__infer_inner_destructor_~WrapsB` here,invalidated by `delete` on `this->b` here,start of use after lifetime trace,accessed `rw.b->f` here,start of value trace,assigned to `this->b`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `getwrapperStack()` here,invalidated by `&(b)` gone out of scope here,start of use after lifetime trace,accessed `rw.b->f` here,start of value trace,assigned to `this->b`,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack()`]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
@@ -31,7 +33,6 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `&(c)` gone out of scope here,start of use after lifetime trace,accessed `pc->f` here,start of value trace,variable declared,assigned to `pc`]
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by call to `free()` on `x` here,start of use after lifetime trace,accessed `x` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by call to `free()` on `x` here,start of use after lifetime trace,accessed `*(x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`]
 codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::assign()` on `vec` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`]
 codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::clear()` on `vec` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp b/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp
index 9b1ff26f3..acf5613f2 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp
@@ -27,7 +27,7 @@ ReferenceWrapperHeap getwrapperHeap() {
             // destructor of WrapsB
 }
 
-int FN_reference_wrapper_heap_bad() {
+int reference_wrapper_heap_bad() {
   ReferenceWrapperHeap rw = getwrapperHeap();
   return rw.b->f; // we want to report use after lifetime bug here
 }
@@ -42,7 +42,7 @@ ReferenceWrapperStack getwrapperStack() {
   return b;
 }
 
-int FN_reference_wrapper_stack_bad() {
+int reference_wrapper_stack_bad() {
   ReferenceWrapperStack rw = getwrapperStack();
   return rw.b->f; // we want to report use after lifetime bug here
 }
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
index ec6147041..fbf75dd87 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 FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
+void 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) {