diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 661764e8b..55c20f15b 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -37,7 +37,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let instantiate_ret ret callee_pname ~callee_exit_mem subst_map mem ret_alias location =
     let copy_reachable_new_locs_from locs mem =
       let copy loc acc =
-        Option.value_map (Dom.Mem.find_heap_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
+        Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
             let v =
               Dom.Val.subst v subst_map location |> Dom.Val.add_trace_elem (Trace.Return location)
             in
@@ -48,7 +48,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     let id = fst ret in
     let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
-    let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in
+    let ret_val = Dom.Mem.find ret_loc callee_exit_mem in
     let ret_var = Loc.of_var (Var.of_id id) in
     let add_ret_alias l = Dom.Mem.load_alias id l mem in
     let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in
@@ -68,28 +68,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           match Tenv.lookup tenv typename with
           | Some str ->
               let formal_locs =
-                Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem
-                |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
+                Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk
+                |> ArrayBlk.get_pow_loc
               in
               let instantiate_fld mem (fn, _, _) =
                 let formal_fields = PowLoc.append_field formal_locs ~fn in
-                let v = Dom.Mem.find_heap_set formal_fields callee_exit_mem in
+                let v = Dom.Mem.find_set formal_fields callee_exit_mem in
                 let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in
                 Dom.Val.subst v subst_map location
-                |> Fn.flip (Dom.Mem.strong_update_heap actual_fields) mem
+                |> Fn.flip (Dom.Mem.strong_update actual_fields) mem
               in
               List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields
           | _ ->
               mem )
         | _ ->
             let formal_locs =
-              Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk
+              Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk
               |> ArrayBlk.get_pow_loc
             in
-            let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in
+            let v = Dom.Mem.find_set formal_locs callee_exit_mem in
             let actual_locs = Dom.Val.get_all_locs actual in
-            Dom.Val.subst v subst_map location
-            |> Fn.flip (Dom.Mem.strong_update_heap actual_locs) mem )
+            Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
       | _ ->
           mem
     in
@@ -159,7 +158,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               | "__inferbo_empty" when Loc.is_return loc_v -> (
                 match Sem.get_formals pdesc with
                 | [(formal, _)] ->
-                    let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in
+                    let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in
                     Dom.Mem.store_empty_alias formal_v loc_v exp2 mem
                 | _ ->
                     assert false )
@@ -171,33 +170,36 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           mem
       | Prune (exp, _, _, _) ->
           Sem.Prune.prune exp mem
-      | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> (
-        match Models.Call.dispatch tenv callee_pname params with
-        | Some {Models.exec} ->
-            let node_hash = CFG.Node.hash node in
-            let model_env =
-              Models.mk_model_env callee_pname node_hash location tenv symbol_table
-            in
-            exec model_env ~ret mem
-        | None ->
-          match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
-          | Some callee_summary -> (
-            match Payload.of_summary callee_summary with
-            | Some payload ->
-                let callee_pdesc = Summary.get_proc_desc callee_summary in
-                instantiate_mem tenv ret callee_pdesc callee_pname params mem payload location
+      | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _)
+        -> (
+          let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
+          match Models.Call.dispatch tenv callee_pname params with
+          | Some {Models.exec} ->
+              let node_hash = CFG.Node.hash node in
+              let model_env =
+                Models.mk_model_env callee_pname node_hash location tenv symbol_table
+              in
+              exec model_env ~ret mem
+          | None ->
+            match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
+            | Some callee_summary -> (
+              match Payload.of_summary callee_summary with
+              | Some payload ->
+                  let callee_pdesc = Summary.get_proc_desc callee_summary in
+                  instantiate_mem tenv ret callee_pdesc callee_pname params mem payload location
+              | None ->
+                  (* This may happen for procedures with a biabduction model. *)
+                  L.(debug BufferOverrun Verbose)
+                    "/!\\ Call to %a at %a has no inferbo payload@\n" Typ.Procname.pp callee_pname
+                    Location.pp location ;
+                  Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
             | None ->
-                (* This may happen for procedures with a biabduction model. *)
                 L.(debug BufferOverrun Verbose)
-                  "/!\\ Call to %a at %a has no inferbo payload@\n" Typ.Procname.pp callee_pname
-                  Location.pp location ;
+                  "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
+                  location ;
                 Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
-          | None ->
-              L.(debug BufferOverrun Verbose)
-                "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
-                location ;
-              Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
       | Call ((id, _), fun_exp, _, location, _) ->
+          let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
           let () =
             L.(debug BufferOverrun Verbose)
               "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp location
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 6ed9c1964..c582bbac2 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -132,6 +132,8 @@ module Val = struct
 
   let of_int n = of_itv (Itv.of_int n)
 
+  let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x}
+
   let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x}
 
   let of_array_alloc : Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> t =
@@ -308,64 +310,17 @@ module Val = struct
   end
 end
 
-module Stack = struct
-  include AbstractDomain.Map (Loc) (Val)
+module StackLocs = struct
+  include AbstractDomain.FiniteSet (Loc)
 
   let bot = empty
-
-  let find : Loc.t -> astate -> Val.t = fun l m -> try find l m with Caml.Not_found -> Val.bot
-
-  let find_set : PowLoc.t -> astate -> Val.t =
-   fun locs mem ->
-    let find_join loc acc = Val.join acc (find loc mem) in
-    PowLoc.fold find_join locs Val.bot
-
-
-  let remove_temps : Ident.t list -> astate -> astate =
-   fun temps mem ->
-    let remove_temp mem temp =
-      let temp_loc = Loc.of_id temp in
-      remove temp_loc mem
-    in
-    List.fold temps ~init:mem ~f:remove_temp
 end
 
-module Heap = struct
+module MemPure = struct
   include AbstractDomain.Map (Loc) (Val)
 
   let bot = empty
 
-  let find : Loc.t -> astate -> Val.t =
-   fun l m -> try find l m with Caml.Not_found -> Val.Itv.top
-
-
-  let find_set : PowLoc.t -> astate -> Val.t =
-   fun locs mem ->
-    let find_join loc acc = Val.join acc (find loc mem) in
-    PowLoc.fold find_join locs Val.bot
-
-
-  let transform : f:(Val.t -> Val.t) -> PowLoc.t -> astate -> astate =
-   fun ~f locs mem -> PowLoc.fold (fun loc -> find loc mem |> f |> add loc) locs mem
-
-
-  let add x v =
-    let sym = if Itv.is_empty (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x in
-    let offset_sym, size_sym =
-      if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot)
-      else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x)
-    in
-    add x {v with Val.sym; Val.offset_sym; Val.size_sym}
-
-
-  let strong_update : PowLoc.t -> Val.t -> astate -> astate =
-   fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem
-
-
-  let weak_update : PowLoc.t -> Val.t -> astate -> astate =
-   fun locs v mem -> PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem
-
-
   let get_return : astate -> Val.t =
    fun mem ->
     let mem = filter (fun l _ -> Loc.is_return l) mem in
@@ -464,10 +419,7 @@ module AliasMap = struct
 
   let find : Ident.t -> t -> AliasTarget.t option = fun k m -> M.find_opt k m
 
-  let remove_temps : Ident.t list -> t -> t =
-   fun temps m ->
-    let remove_temp m temp = M.remove temp m in
-    List.fold temps ~init:m ~f:remove_temp
+  let remove : Ident.t -> t -> t = M.remove
 end
 
 module AliasRet = struct
@@ -554,8 +506,8 @@ module Alias = struct
     else a
 
 
-  let remove_temps : Ident.t list -> astate -> astate =
-   fun temps a -> (AliasMap.remove_temps temps (fst a), snd a)
+  let remove_temp : Ident.t -> astate -> astate =
+   fun temp (alias_map, alias_ret) -> (AliasMap.remove temp alias_map, alias_ret)
 
 
   let pp : F.formatter -> astate -> unit =
@@ -647,8 +599,8 @@ end
 
 module MemReach = struct
   type astate =
-    { stack: Stack.astate
-    ; heap: Heap.astate
+    { stack_locs: StackLocs.astate
+    ; mem_pure: MemPure.astate
     ; alias: Alias.astate
     ; latest_prune: LatestPrune.astate
     ; relation: Relation.astate }
@@ -656,8 +608,8 @@ module MemReach = struct
   type t = astate
 
   let init : t =
-    { stack= Stack.bot
-    ; heap= Heap.bot
+    { stack_locs= StackLocs.bot
+    ; mem_pure= MemPure.bot
     ; alias= Alias.bot
     ; latest_prune= LatestPrune.top
     ; relation= Relation.empty }
@@ -666,7 +618,8 @@ module MemReach = struct
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else
-      Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap
+      StackLocs.( <= ) ~lhs:lhs.stack_locs ~rhs:rhs.stack_locs
+      && MemPure.( <= ) ~lhs:lhs.mem_pure ~rhs:rhs.mem_pure
       && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias
       && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune
       && Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation
@@ -675,8 +628,8 @@ module MemReach = struct
   let widen ~prev ~next ~num_iters =
     if phys_equal prev next then prev
     else
-      { stack= Stack.widen ~prev:prev.stack ~next:next.stack ~num_iters
-      ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters
+      { stack_locs= StackLocs.widen ~prev:prev.stack_locs ~next:next.stack_locs ~num_iters
+      ; mem_pure= MemPure.widen ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters
       ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters
       ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters
       ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters }
@@ -684,8 +637,8 @@ module MemReach = struct
 
   let join : t -> t -> t =
    fun x y ->
-    { stack= Stack.join x.stack y.stack
-    ; heap= Heap.join x.heap y.heap
+    { stack_locs= StackLocs.join x.stack_locs y.stack_locs
+    ; mem_pure= MemPure.join x.mem_pure y.mem_pure
     ; alias= Alias.join x.alias y.alias
     ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune
     ; relation= Relation.join x.relation y.relation }
@@ -693,23 +646,28 @@ module MemReach = struct
 
   let pp : F.formatter -> t -> unit =
    fun fmt x ->
-    F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias ;
+    F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" StackLocs.pp x.stack_locs MemPure.pp x.mem_pure
+      Alias.pp x.alias ;
     if Option.is_some Config.bo_relational_domain then
       F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
 
 
-  let find_stack : Loc.t -> t -> Val.t = fun k m -> Stack.find k m.stack
+  let is_stack_loc : Loc.t -> t -> bool = fun l m -> StackLocs.mem l m.stack_locs
 
-  let find_stack_set : PowLoc.t -> t -> Val.t = fun k m -> Stack.find_set k m.stack
+  let find_opt : Loc.t -> t -> Val.t option = fun l m -> MemPure.find_opt l m.mem_pure
 
-  let find_heap : Loc.t -> t -> Val.t = fun k m -> Heap.find k m.heap
+  let find_stack : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
 
-  let find_heap_opt : Loc.t -> t -> Val.t option = fun k m -> Heap.find_opt k m.heap
+  let find_heap : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.Itv.top
+
+  let find : Loc.t -> t -> Val.t =
+   fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m
 
-  let find_heap_set : PowLoc.t -> t -> Val.t = fun k m -> Heap.find_set k m.heap
 
   let find_set : PowLoc.t -> t -> Val.t =
-   fun k m -> Val.join (find_stack_set k m) (find_heap_set k m)
+   fun locs m ->
+    let find_join loc acc = Val.join acc (find loc m) in
+    PowLoc.fold find_join locs Val.bot
 
 
   let find_alias : Ident.t -> t -> AliasTarget.t option = fun k m -> Alias.find k m.alias
@@ -737,9 +695,29 @@ module MemReach = struct
    fun formal loc e m -> {m with alias= Alias.store_empty formal loc e m.alias}
 
 
-  let add_stack : Loc.t -> Val.t -> t -> t = fun k v m -> {m with stack= Stack.add k v m.stack}
+  let add_stack_loc : Loc.t -> t -> t = fun k m -> {m with stack_locs= StackLocs.add k m.stack_locs}
+
+  let add_stack : Loc.t -> Val.t -> t -> t =
+   fun k v m ->
+    {m with stack_locs= StackLocs.add k m.stack_locs; mem_pure= MemPure.add k v m.mem_pure}
+
+
+  let replace_stack : Loc.t -> Val.t -> t -> t =
+   fun k v m -> {m with mem_pure= MemPure.add k v m.mem_pure}
+
+
+  let add_heap : Loc.t -> Val.t -> t -> t =
+   fun x v m ->
+    let v =
+      let sym = if Itv.is_empty (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x in
+      let offset_sym, size_sym =
+        if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot)
+        else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x)
+      in
+      {v with Val.sym; Val.offset_sym; Val.size_sym}
+    in
+    {m with mem_pure= MemPure.add x v m.mem_pure}
 
-  let add_heap : Loc.t -> Val.t -> t -> t = fun k v m -> {m with heap= Heap.add k v m.heap}
 
   let add_unknown_from
       : Ident.t -> callee_pname:Typ.Procname.t option -> location:Location.t -> t -> t =
@@ -748,37 +726,48 @@ module MemReach = struct
     add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown
 
 
-  let strong_update_heap : PowLoc.t -> Val.t -> t -> t =
-   fun p v m -> {m with heap= Heap.strong_update p v m.heap}
-
+  let strong_update : PowLoc.t -> Val.t -> t -> t =
+   fun locs v m ->
+    let strong_update1 l m = if is_stack_loc l m then replace_stack l v m else add_heap l v m in
+    PowLoc.fold strong_update1 locs m
 
-  let transform_heap : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t =
-   fun ~f p m -> {m with heap= Heap.transform ~f p m.heap}
 
+  let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t =
+   fun ~f locs m ->
+    let transform_mem1 l m =
+      let add, find =
+        if is_stack_loc l m then (replace_stack, find_stack) else (add_heap, find_heap)
+      in
+      add l (f (find l m)) m
+    in
+    PowLoc.fold transform_mem1 locs m
 
-  let weak_update_heap : PowLoc.t -> Val.t -> t -> t =
-   fun p v m -> {m with heap= Heap.weak_update p v m.heap}
 
+  let weak_update locs v m = transform_mem ~f:(fun v' -> Val.join v' v) locs m
 
-  let get_return : t -> Val.t = fun m -> Heap.get_return m.heap
+  let get_return : t -> Val.t = fun m -> MemPure.get_return m.mem_pure
 
   let update_mem : PowLoc.t -> Val.t -> t -> t =
    fun ploc v s ->
-    if can_strong_update ploc then strong_update_heap ploc v s
+    if can_strong_update ploc then strong_update ploc v s
     else
       let () =
         L.(debug BufferOverrun Verbose) "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v
       in
-      weak_update_heap ploc v s
+      weak_update ploc v s
 
 
-  let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t =
-   fun ~f ploc s -> transform_heap ~f ploc s
+  let remove_temp : Ident.t -> t -> t =
+   fun temp m ->
+    let l = Loc.of_id temp in
+    { m with
+      stack_locs= StackLocs.remove l m.stack_locs
+    ; mem_pure= MemPure.remove l m.mem_pure
+    ; alias= Alias.remove_temp temp m.alias }
 
 
   let remove_temps : Ident.t list -> t -> t =
-   fun temps m ->
-    {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias}
+   fun temps m -> List.fold temps ~init:m ~f:(fun acc temp -> remove_temp temp acc)
 
 
   let set_prune_pairs : PrunePairs.t -> t -> t =
@@ -820,14 +809,14 @@ module MemReach = struct
     and add_from_loc heap loc acc =
       if PowLoc.mem loc acc then acc
       else
-        let reachable_locs = Heap.fold (add_reachable1 ~root:loc) heap PowLoc.empty in
+        let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap PowLoc.empty in
         add_from_locs heap reachable_locs (PowLoc.add loc acc)
     in
-    fun locs m -> add_from_locs m.heap locs PowLoc.empty
+    fun locs m -> add_from_locs m.mem_pure locs PowLoc.empty
 
 
-  let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate =
-   fun ~filter_loc {heap} -> Heap.range ~filter_loc heap
+  let range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate =
+   fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure
 
 
   let get_relation : t -> Relation.astate = fun m -> m.relation
@@ -882,30 +871,24 @@ module Mem = struct
    fun f -> f_lift_default ~default:Bottom (fun m' -> NonBottom (f m'))
 
 
-  let find_stack : Loc.t -> t -> Val.t =
-   fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k)
+  let is_stack_loc : Loc.t -> t -> bool =
+   fun k -> f_lift_default ~default:false (MemReach.is_stack_loc k)
 
 
-  let find_stack_set : PowLoc.t -> t -> Val.t =
-   fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack_set k)
+  let find : Loc.t -> t -> Val.t = fun k -> f_lift_default ~default:Val.bot (MemReach.find k)
 
-
-  let find_heap : Loc.t -> t -> Val.t =
-   fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap k)
-
-
-  let find_heap_opt : Loc.t -> t -> Val.t option =
-   fun k -> f_lift_default ~default:None (MemReach.find_heap_opt k)
-
-
-  let find_heap_set : PowLoc.t -> t -> Val.t =
-   fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap_set k)
+  let find_stack : Loc.t -> t -> Val.t =
+   fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k)
 
 
   let find_set : PowLoc.t -> t -> Val.t =
    fun k -> f_lift_default ~default:Val.bot (MemReach.find_set k)
 
 
+  let find_opt : Loc.t -> t -> Val.t option =
+   fun k -> f_lift_default ~default:None (MemReach.find_opt k)
+
+
   let find_alias : Ident.t -> t -> AliasTarget.t option =
    fun k -> f_lift_default ~default:None (MemReach.find_alias k)
 
@@ -934,6 +917,8 @@ module Mem = struct
    fun formal loc e -> f_lift (MemReach.store_empty_alias formal loc e)
 
 
+  let add_stack_loc : Loc.t -> t -> t = fun k -> f_lift (MemReach.add_stack_loc k)
+
   let add_stack : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_stack k v)
 
   let add_heap : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_heap k v)
@@ -947,13 +932,9 @@ module Mem = struct
    fun id ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname:None ~location)
 
 
-  let strong_update_heap : PowLoc.t -> Val.t -> t -> t =
-   fun p v -> f_lift (MemReach.strong_update_heap p v)
-
-
-  let weak_update_heap : PowLoc.t -> Val.t -> t -> t =
-   fun p v -> f_lift (MemReach.weak_update_heap p v)
+  let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.strong_update p v)
 
+  let weak_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.weak_update p v)
 
   let get_return : t -> Val.t = f_lift_default ~default:Val.bot MemReach.get_return
 
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 713a1660d..eaba97227 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -83,7 +83,7 @@ let check_alloc_size size_exp {location} mem cond_set =
 let set_uninitialized location (typ: Typ.t) ploc mem =
   match typ.desc with
   | Tint _ | Tfloat _ ->
-      Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem
+      Dom.Mem.weak_update ploc Dom.Val.Itv.top mem
   | _ ->
       L.(debug BufferOverrun Verbose)
         "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp
@@ -336,7 +336,7 @@ module Collection = struct
 
 
   let change_size_by ~size_f alist_id _ ~ret:_ mem =
-    let alist_v = Dom.Mem.find_stack (Loc.of_id alist_id) mem in
+    let alist_v = Dom.Mem.find (Loc.of_id alist_id) mem in
     let locs = Dom.Val.get_pow_loc alist_v in
     Dom.Mem.transform_mem ~f:size_f locs mem
 
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 033bbcddc..0cd61a0b1 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -140,9 +140,8 @@ let rec eval : Exp.t -> Mem.astate -> Val.t =
     | Exp.Var id ->
         Mem.find_stack (Var.of_id id |> Loc.of_var) mem
     | Exp.Lvar pvar ->
-        let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in
-        let arr = Mem.find_stack_set ploc mem in
-        ploc |> Val.of_pow_loc |> Val.join arr
+        let ploc = Loc.of_pvar pvar in
+        if Mem.is_stack_loc ploc mem then Mem.find ploc mem else Val.of_loc ploc
     | Exp.UnOp (uop, e, _) ->
         eval_unop uop e mem
     | Exp.BinOp (bop, e1, e2) ->
@@ -249,7 +248,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
   | Exp.Var id -> (
     match Mem.find_alias id mem with
     | Some (AliasTarget.Simple loc) ->
-        Mem.find_heap loc mem
+        Mem.find loc mem
     | Some (AliasTarget.Empty _) | None ->
         Val.bot )
   | Exp.Lvar pvar ->
@@ -260,7 +259,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
       eval_arr e mem
   | Exp.Lfield (e, fn, _) ->
       let locs = eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in
-      Mem.find_heap_set locs mem
+      Mem.find_set locs mem
   | Exp.Lindex (e1, e2) ->
       let arr = eval e1 mem in
       let idx = eval e2 mem in
@@ -290,11 +289,11 @@ module Prune = struct
     | Exp.Var x -> (
       match Mem.find_alias x mem with
       | Some (AliasTarget.Simple lv) ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let v' = Val.prune_ne_zero v in
           update_mem_in_prune lv v' astate
       | Some (AliasTarget.Empty lv) ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
       | None ->
@@ -302,11 +301,11 @@ module Prune = struct
     | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
       match Mem.find_alias x mem with
       | Some (AliasTarget.Simple lv) ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
       | Some (AliasTarget.Empty lv) ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in
           let v' = Val.modify_itv itv_v v in
           update_mem_in_prune lv v' astate
@@ -325,7 +324,7 @@ module Prune = struct
     | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> (
       match Mem.find_simple_alias x mem with
       | Some lv ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let v' = Val.prune_comp comp v (eval e' mem) in
           update_mem_in_prune lv v' astate
       | None ->
@@ -333,7 +332,7 @@ module Prune = struct
     | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> (
       match Mem.find_simple_alias x mem with
       | Some lv ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let v' = Val.prune_eq v (eval e' mem) in
           update_mem_in_prune lv v' astate
       | None ->
@@ -341,7 +340,7 @@ module Prune = struct
     | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> (
       match Mem.find_simple_alias x mem with
       | Some lv ->
-          let v = Mem.find_heap lv mem in
+          let v = Mem.find lv mem in
           let v' = Val.prune_ne v (eval e' mem) in
           update_mem_in_prune lv v' astate
       | None ->
@@ -437,11 +436,11 @@ let get_matching_pairs
   let get_size_sym v = Val.get_size_sym v in
   let get_field_name (fn, _, _) = fn in
   let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in
-  let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in
+  let deref_field v fn mem = Mem.find_set (append_field v fn) mem in
   let deref_ptr v mem =
     let array_locs = Val.get_array_locs v in
     let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in
-    Mem.find_heap_set locs mem
+    Mem.find_set locs mem
   in
   let ret_alias = ref None in
   let add_ret_alias v1 v2 =
@@ -563,7 +562,7 @@ let get_subst_map
          * Relation.SubstMap.t =
  fun tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem ->
   let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) =
-    let callee_v = Mem.find_heap (Loc.of_pvar formal) callee_exit_mem in
+    let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in
     let new_bound_matching, ret_alias', new_rel_matching =
       get_matching_pairs tenv (Itv.SymbolPath.of_pvar formal) callee_v actual actual_exp typ
         caller_mem callee_symbol_table callee_exit_mem
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index a44efae87..664ea93dd 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -19,12 +19,12 @@ module TraceSet = Trace.Set
 module Exec = struct
   let get_alist_size alist mem =
     let size_powloc = Dom.Val.get_pow_loc alist in
-    Dom.Mem.find_heap_set size_powloc mem
+    Dom.Mem.find_set size_powloc mem
 
 
   let load_val id val_ mem =
     let locs = val_ |> Dom.Val.get_all_locs in
-    let v = Dom.Mem.find_heap_set locs mem in
+    let v = Dom.Mem.find_set locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
     if PowLoc.is_singleton locs then Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem
     else mem
@@ -155,7 +155,7 @@ module Exec = struct
             let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
             let offset, size = (Itv.zero, length) in
             let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size in
-            mem |> Dom.Mem.strong_update_heap field_loc v
+            mem |> Dom.Mem.strong_update field_loc v
             |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
         | _ ->
             init_fields field_typ field_loc dimension ?dyn_length mem
@@ -188,7 +188,7 @@ module Exec = struct
           | Tarray {length= Some length} ->
               let length = Itv.plus (Itv.of_int_lit length) dyn_length in
               let v = Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_size length in
-              Dom.Mem.strong_update_heap field_loc v mem
+              Dom.Mem.strong_update field_loc v mem
           | _ ->
               set_dyn_length tenv field_typ field_loc dyn_length mem )
       | _ ->
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index b0e18b96f..e4a5aa3da 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -165,8 +165,7 @@ module BoundMap = struct
                        unreachable returning cost 0 \n" ;
                     BasicCost.zero
                 | NonBottom mem ->
-                    BufferOverrunDomain.MemReach.heap_range ~filter_loc:(filter_loc control_vars)
-                      mem
+                    BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_vars) mem
               in
               L.(debug Analysis Medium)
                 "@\n>>>Setting bound for node = %a  to %a@\n\n" Node.pp_id node_id BasicCost.pp