diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 212c8b42c..cbbe9f5c9 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -32,12 +32,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Dom.Mem
 
-  type extras = ProcData.no_extras
+  type extras = Itv.SymbolTable.t
 
   let declare_symbolic_val
-      : Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> Loc.t
-        -> Typ.typ -> inst_num:int -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t =
-   fun pname path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem ->
+      : Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int
+        -> Location.t -> Loc.t -> Typ.typ -> inst_num:int -> new_sym_num:Itv.Counter.t -> Domain.t
+        -> Domain.t =
+   fun pname symbol_table path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem ->
     let max_depth = 2 in
     let new_alloc_num = Itv.Counter.make 1 in
     let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem =
@@ -48,13 +49,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         | Typ.Tint ikind ->
             let unsigned = Typ.ikind_is_unsigned ikind in
             let v =
-              Dom.Val.make_sym ~unsigned loc pname path new_sym_num
+              Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tfloat _ ->
             let v =
-              Dom.Val.make_sym loc pname path new_sym_num
+              Dom.Val.make_sym loc pname symbol_table path new_sym_num
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
@@ -63,8 +64,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               ~decl_sym_val:(decl_sym_val ~may_last_field:false)
               pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem
         | Typ.Tptr (typ, _) ->
-            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv
-              ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
+            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname
+              symbol_table path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num
+              ~new_alloc_num mem
         | Typ.Tarray {elt; length} ->
             let size =
               match length with
@@ -76,12 +78,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let offset = Itv.zero in
             BoUtils.Exec.decl_sym_arr
               ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              pname path tenv ~node_hash location ~depth loc elt ~offset ?size ~inst_num
-              ~new_sym_num ~new_alloc_num mem
+              pname symbol_table path tenv ~node_hash location ~depth loc elt ~offset ?size
+              ~inst_num ~new_sym_num ~new_alloc_num mem
         | Typ.Tstruct typename -> (
           match Models.TypName.dispatch typename with
           | Some {Models.declare_symbolic} ->
-              let model_env = Models.mk_model_env pname node_hash location tenv in
+              let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in
               declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
                 loc ~inst_num ~new_sym_num ~new_alloc_num mem
           | None ->
@@ -108,34 +110,33 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   let declare_symbolic_parameters
-      : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> inst_num:int
-        -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate =
-   fun pname tenv ~node_hash location ~inst_num formals mem ->
+      : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> Itv.SymbolTable.t
+        -> inst_num:int -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate =
+   fun pname tenv ~node_hash location symbol_table ~inst_num formals mem ->
     let new_sym_num = Itv.Counter.make 0 in
     let add_formal (mem, inst_num) (pvar, typ) =
       let loc = Loc.of_pvar pvar in
       let path = Itv.SymbolPath.of_pvar pvar in
       let mem =
-        declare_symbolic_val pname path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem
+        declare_symbolic_val pname symbol_table path tenv ~node_hash location loc typ ~inst_num
+          ~new_sym_num mem
       in
       (mem, inst_num + 1)
     in
     List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst
 
 
-  let instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map mem ret_alias
-      location =
+  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 =
-        let v =
-          Dom.Mem.find_heap loc callee_exit_mem |> (fun v -> Dom.Val.subst v subst_map location)
-          |> Dom.Val.add_trace_elem (Trace.Return location)
-        in
-        Dom.Mem.add_heap loc v acc
+        Option.value_map (Dom.Mem.find_heap_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
+            Dom.Mem.add_heap loc v acc )
       in
-      let new_locs = Dom.Mem.get_new_heap_locs ~prev:callee_entry_mem ~next:callee_exit_mem in
       let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
-      PowLoc.fold copy (PowLoc.inter new_locs reachable_locs) mem
+      PowLoc.fold copy reachable_locs mem
     in
     let id = fst ret in
     let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
@@ -148,7 +149,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
 
 
-  let instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location mem =
+  let instantiate_param tenv pdesc params callee_exit_mem subst_map location mem =
     let formals = Sem.get_formals pdesc in
     let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in
     let f mem formal actual =
@@ -159,7 +160,7 @@ 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_entry_mem
+                Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem
                 |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
               in
               let instantiate_fld mem (fn, _, _) =
@@ -174,8 +175,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               mem )
         | _ ->
             let formal_locs =
-              Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem
-              |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
+              Dom.Mem.find_heap (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 actual_locs = Dom.Val.get_all_locs actual in
@@ -197,19 +198,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       : Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list
         -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate =
    fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
-    let callee_entry_mem = Dom.Summary.get_input summary in
+    let callee_symbol_table = Dom.Summary.get_symbol_table summary in
     let callee_exit_mem = Dom.Summary.get_output summary in
-    let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in
     match callee_pdesc with
     | Some pdesc ->
         let bound_subst_map, ret_alias, rel_subst_map =
-          Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias
+          Sem.get_subst_map tenv pdesc params caller_mem callee_symbol_table callee_exit_mem
         in
         let caller_mem =
-          instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem bound_subst_map
-            caller_mem ret_alias location
-          |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem bound_subst_map
-               location
+          instantiate_ret ret callee_pname ~callee_exit_mem bound_subst_map caller_mem ret_alias
+            location
+          |> instantiate_param tenv pdesc params callee_exit_mem bound_subst_map location
           |> forget_ret_relation ret callee_pname
         in
         Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
@@ -229,7 +228,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate =
-   fun mem {pdesc; tenv} node instr ->
+   fun mem {pdesc; tenv; extras= symbol_table} node instr ->
     let pname = Procdesc.get_proc_name pdesc in
     let output_mem =
       match instr with
@@ -272,7 +271,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         match Models.Call.dispatch 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 in
+            let model_env =
+              Models.mk_model_env callee_pname node_hash location tenv symbol_table
+            in
             exec model_env ~ret mem
         | None ->
           match Payload.read pdesc callee_pname with
@@ -299,7 +300,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             | Typ.Tstruct typname -> (
               match Models.TypName.dispatch typname with
               | Some {Models.declare_local} ->
-                  let model_env = Models.mk_model_env pname node_hash location tenv in
+                  let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in
                   declare_local ~decl_local model_env loc ~inst_num ~dimension mem
               | None ->
                   (mem, inst_num) )
@@ -312,7 +313,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           in
           let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) locals in
           let formals = Sem.get_formals pdesc in
-          declare_symbolic_parameters pname tenv ~node_hash location ~inst_num formals mem
+          declare_symbolic_parameters pname tenv ~node_hash location symbol_table ~inst_num formals
+            mem
       | Call (_, fun_exp, _, location, _) ->
           let () =
             L.(debug BufferOverrun Verbose)
@@ -443,12 +445,13 @@ module Report = struct
       : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate
         -> Payload.t -> Location.t -> PO.ConditionSet.t =
    fun tenv caller_pname callee_pdesc params caller_mem summary location ->
-    let callee_entry_mem = Dom.Summary.get_input summary in
+    let callee_symbol_table = Dom.Summary.get_symbol_table summary in
+    let callee_exit_mem = Dom.Summary.get_output summary in
     let callee_cond = Dom.Summary.get_cond_set summary in
     match callee_pdesc with
     | Some pdesc ->
         let bound_subst_map, _, rel_subst_map =
-          Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None
+          Sem.get_subst_map tenv pdesc params caller_mem callee_symbol_table callee_exit_mem
         in
         let pname = Procdesc.get_proc_name pdesc in
         let caller_rel = Dom.Mem.get_relation caller_mem in
@@ -459,9 +462,9 @@ module Report = struct
 
 
   let check_instr
-      : Procdesc.t -> Tenv.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t
-        -> PO.ConditionSet.t =
-   fun pdesc tenv node instr mem cond_set ->
+      : Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate
+        -> PO.ConditionSet.t -> PO.ConditionSet.t =
+   fun pdesc tenv symbol_table node instr mem cond_set ->
     let pname = Procdesc.get_proc_name pdesc in
     match instr with
     | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) ->
@@ -470,7 +473,7 @@ module Report = struct
       match Models.Call.dispatch callee_pname params with
       | Some {Models.check} ->
           let node_hash = CFG.Node.hash node in
-          check (Models.mk_model_env pname node_hash location tenv) mem cond_set
+          check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set
       | None ->
         match Payload.read pdesc callee_pname with
         | Some callee_summary ->
@@ -494,9 +497,10 @@ module Report = struct
 
 
   let check_instrs
-      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.Node.t -> Instrs.not_reversed_t
-        -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t -> PO.ConditionSet.t =
-   fun summary pdesc tenv cfg node instrs state cond_set ->
+      : Summary.t -> Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.t -> CFG.Node.t
+        -> Instrs.not_reversed_t -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t
+        -> PO.ConditionSet.t =
+   fun summary pdesc tenv symbol_table cfg node instrs state cond_set ->
     match state with
     | _ when Instrs.is_empty instrs ->
         cond_set
@@ -513,27 +517,30 @@ module Report = struct
           | NonBottom _ ->
               ()
         in
-        let cond_set = check_instr pdesc tenv node instr pre cond_set in
+        let cond_set = check_instr pdesc tenv symbol_table node instr pre cond_set in
         print_debug_info instr pre cond_set ;
         cond_set
 
 
   let check_node
-      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t
-        -> CFG.Node.t -> PO.ConditionSet.t =
-   fun summary pdesc tenv cfg inv_map cond_set node ->
+      : Summary.t -> Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.t -> Analyzer.invariant_map
+        -> PO.ConditionSet.t -> CFG.Node.t -> PO.ConditionSet.t =
+   fun summary pdesc tenv symbol_table cfg inv_map cond_set node ->
     match Analyzer.extract_state (CFG.Node.id node) inv_map with
     | Some state ->
         let instrs = CFG.instrs node in
-        check_instrs summary pdesc tenv cfg node instrs state cond_set
+        check_instrs summary pdesc tenv symbol_table cfg node instrs state cond_set
     | _ ->
         cond_set
 
 
   let check_proc
-      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t =
-   fun summary pdesc tenv cfg inv_map ->
-    CFG.fold_nodes cfg ~f:(check_node summary pdesc tenv cfg inv_map) ~init:PO.ConditionSet.empty
+      : Summary.t -> Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.t -> Analyzer.invariant_map
+        -> PO.ConditionSet.t =
+   fun summary pdesc tenv symbol_table cfg inv_map ->
+    CFG.fold_nodes cfg
+      ~f:(check_node summary pdesc tenv symbol_table cfg inv_map)
+      ~init:PO.ConditionSet.empty
 
 
   let make_err_trace : Trace.t -> string -> Errlog.loc_trace =
@@ -622,21 +629,23 @@ let get_local_decls cfg =
 let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
  fun {proc_desc; tenv; summary} ->
   Preanal.do_preanalysis proc_desc tenv ;
-  let pdata = ProcData.make_default proc_desc tenv in
+  let symbol_table = Itv.SymbolTable.empty () in
+  let pdata = ProcData.make proc_desc tenv symbol_table in
   let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in
   let cfg = CFG.from_pdesc proc_desc in
   let locals = get_local_decls cfg in
-  let forget_locals mem = Option.map ~f:(Dom.Mem.forget_locs locals) mem in
-  let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map |> forget_locals in
-  let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map |> forget_locals in
+  let exit_mem =
+    extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map
+    |> Option.map ~f:(Dom.Mem.forget_locs locals)
+  in
   let cond_set =
-    Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc
-    |> Report.forget_locs locals
+    Report.check_proc summary proc_desc tenv symbol_table cfg inv_map
+    |> Report.report_errors summary proc_desc |> Report.forget_locs locals
   in
   let summary =
-    match (entry_mem, exit_mem) with
-    | Some entry_mem, Some exit_mem ->
-        let post = (entry_mem, exit_mem, cond_set) in
+    match exit_mem with
+    | Some exit_mem ->
+        let post = (Itv.SymbolTable.summary_of symbol_table, exit_mem, cond_set) in
         ( if Config.bo_debug >= 1 then
             let proc_name = Procdesc.get_proc_name proc_desc in
             print_summary proc_name post ) ;
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index a848daca8..60e314238 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -147,10 +147,11 @@ module Val = struct
   let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
 
   let make_sym
-      : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t =
-   fun ?(unsigned= false) loc pname path new_sym_num ->
+      : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
+        -> Itv.Counter.t -> t =
+   fun ?(unsigned= false) loc pname symbol_table path new_sym_num ->
     { bot with
-      itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num
+      itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num
     ; sym= Relation.Sym.of_loc loc }
 
 
@@ -363,14 +364,6 @@ module Heap = struct
    fun locs v mem -> PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem
 
 
-  let pp_summary : F.formatter -> astate -> unit =
-   fun fmt mem ->
-    let pp_map fmt (k, v) = F.fprintf fmt "%a -> %a" Loc.pp k Val.pp_summary v in
-    F.fprintf fmt "@[<v 2>{ " ;
-    F.pp_print_list pp_map fmt (bindings mem) ;
-    F.fprintf fmt " }@]"
-
-
   let get_return : astate -> Val.t =
    fun mem ->
     let mem = filter (fun l _ -> Loc.is_return l) mem in
@@ -703,16 +696,14 @@ module MemReach = struct
       F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
 
 
-  let pp_summary : F.formatter -> t -> unit =
-   fun fmt x -> F.fprintf fmt "@[<v 0>Parameters:@,%a@]" Heap.pp_summary x.heap
-
-
   let find_stack : Loc.t -> t -> Val.t = fun k m -> Stack.find k m.stack
 
   let find_stack_set : PowLoc.t -> t -> Val.t = fun k m -> Stack.find_set k m.stack
 
   let find_heap : Loc.t -> t -> Val.t = fun k m -> Heap.find k m.heap
 
+  let find_heap_opt : Loc.t -> t -> Val.t option = fun k m -> Heap.find_opt k m.heap
+
   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 =
@@ -810,12 +801,6 @@ module MemReach = struct
         {m with latest_prune= LatestPrune.Top}
 
 
-  let get_new_heap_locs : prev:t -> next:t -> PowLoc.t =
-   fun ~prev ~next ->
-    let add_loc loc _val acc = if Heap.mem loc prev.heap then acc else PowLoc.add loc acc in
-    Heap.fold add_loc next.heap PowLoc.empty
-
-
   let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
     let add_reachable1 ~root loc v acc =
       if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v)
@@ -884,28 +869,10 @@ module Mem = struct
    fun ~default f m -> match m with Bottom -> default | NonBottom m' -> f m'
 
 
-  let f_lift_default2 : default:'a -> (MemReach.t -> MemReach.t -> 'a) -> t -> t -> 'a =
-   fun ~default f m1 m2 ->
-    match (m1, m2) with
-    | Bottom, _ | _, Bottom ->
-        default
-    | NonBottom m1', NonBottom m2' ->
-        f m1' m2'
-
-
   let f_lift : (MemReach.t -> MemReach.t) -> t -> t =
    fun f -> f_lift_default ~default:Bottom (fun m' -> NonBottom (f m'))
 
 
-  let pp_summary : F.formatter -> t -> unit =
-   fun fmt m ->
-    match m with
-    | Bottom ->
-        F.pp_print_string fmt "unreachable"
-    | NonBottom m' ->
-        MemReach.pp_summary fmt m'
-
-
   let find_stack : Loc.t -> t -> Val.t =
    fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k)
 
@@ -918,6 +885,10 @@ module Mem = struct
    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)
 
@@ -968,13 +939,6 @@ module Mem = struct
 
   let get_return : t -> Val.t = f_lift_default ~default:Val.bot MemReach.get_return
 
-  let get_new_heap_locs : prev:t -> next:t -> PowLoc.t =
-   fun ~prev ~next ->
-    f_lift_default2 ~default:PowLoc.empty
-      (fun m1 m2 -> MemReach.get_new_heap_locs ~prev:m1 ~next:m2)
-      prev next
-
-
   let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
    fun locs -> f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from locs)
 
@@ -1034,9 +998,9 @@ module Mem = struct
 end
 
 module Summary = struct
-  type t = Mem.t * Mem.t * PO.ConditionSet.t
+  type t = Itv.SymbolTable.summary_t * Mem.t * PO.ConditionSet.t
 
-  let get_input : t -> Mem.t = fst3
+  let get_symbol_table : t -> Itv.SymbolTable.summary_t = fst3
 
   let get_output : t -> Mem.t = snd3
 
@@ -1044,7 +1008,9 @@ module Summary = struct
 
   let get_return : t -> Val.t = fun s -> Mem.get_return (get_output s)
 
-  let pp_symbol_map : F.formatter -> t -> unit = fun fmt s -> Mem.pp_summary fmt (get_input s)
+  let pp_symbol_map : F.formatter -> t -> unit =
+   fun fmt s -> Itv.SymbolTable.pp fmt (get_symbol_table s)
+
 
   let pp_return : F.formatter -> t -> unit =
    fun fmt s -> F.fprintf fmt "Return value: %a" Val.pp_summary (get_return s)
@@ -1057,6 +1023,7 @@ module Summary = struct
 
 
   let pp : F.formatter -> t -> unit =
-   fun fmt (entry_mem, exit_mem, condition_set) ->
-    F.fprintf fmt "%a@;%a@;%a" Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set
+   fun fmt (symbol_table, exit_mem, condition_set) ->
+    F.fprintf fmt "%a@;%a@;%a" Itv.SymbolTable.pp symbol_table Mem.pp exit_mem PO.ConditionSet.pp
+      condition_set
 end
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index e6aa2aaa8..91a168c56 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -17,9 +17,16 @@ module Relation = BufferOverrunDomainRelation
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
-type model_env = {pname: Typ.Procname.t; node_hash: int; location: Location.t; tenv: Tenv.t}
+type model_env =
+  { pname: Typ.Procname.t
+  ; node_hash: int
+  ; location: Location.t
+  ; tenv: Tenv.t
+  ; symbol_table: Itv.SymbolTable.t }
+
+let mk_model_env pname node_hash location tenv symbol_table =
+  {pname; node_hash; location; tenv; symbol_table}
 
-let mk_model_env pname node_hash location tenv = {pname; node_hash; location; tenv}
 
 type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
 
@@ -247,12 +254,12 @@ module StdArray = struct
       BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
         ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location} ~depth loc ~inst_num
-        ~new_sym_num ~new_alloc_num mem =
+    let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location; symbol_table} ~depth
+        loc ~inst_num ~new_sym_num ~new_alloc_num mem =
       let offset = Itv.zero in
       let size = Itv.of_int64 length in
-      BoUtils.Exec.decl_sym_arr ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ
-        ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem
+      BoUtils.Exec.decl_sym_arr ~decl_sym_val pname symbol_table path tenv ~node_hash location
+        ~depth loc typ ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem
     in
     {declare_local; declare_symbolic}
 
@@ -307,9 +314,9 @@ module ArrayList = struct
     let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num ~dimension mem =
       BoUtils.Exec.decl_local_arraylist pname ~node_hash location loc ~inst_num ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val:_ path {pname; location} ~depth:_ loc ~inst_num:_
-        ~new_sym_num ~new_alloc_num:_ mem =
-      BoUtils.Exec.decl_sym_arraylist pname path location loc ~new_sym_num mem
+    let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc
+        ~inst_num:_ ~new_sym_num ~new_alloc_num:_ mem =
+      BoUtils.Exec.decl_sym_arraylist pname symbol_table path location loc ~new_sym_num mem
     in
     {declare_local; declare_symbolic}
 
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index dd897bc69..cc6a77e9c 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -484,12 +484,14 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
 
 
 let get_matching_pairs
-    : Tenv.t -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate -> Mem.astate
-      -> callee_ret_alias:AliasTarget.t option
-      -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
+    : Tenv.t -> Itv.SymbolPath.partial -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate
+      -> Itv.SymbolTable.summary_t -> Mem.astate
+      -> (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
          * AliasTarget.t option
          * (Relation.Var.t * Relation.SymExp.t option) list =
- fun tenv formal actual actual_exp_opt typ caller_mem callee_mem ~callee_ret_alias ->
+ fun tenv formal callee_v actual actual_exp_opt typ caller_mem callee_symbol_table callee_exit_mem ->
+  let open Itv in
+  let callee_ret_alias = Mem.find_ret_alias callee_exit_mem in
   let get_itv v = Val.get_itv v in
   let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in
   let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
@@ -514,13 +516,13 @@ let get_matching_pairs
     | None ->
         ()
   in
-  let add_pair_itv itv1 itv2 traces l =
-    let open Itv in
-    if itv1 <> bot && itv1 <> top then
-      if Itv.eq itv2 bot then
-        (lb itv1, Bottom, TraceSet.empty) :: (ub itv1, Bottom, TraceSet.empty) :: l
-      else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l
-    else l
+  let add_pair_itv path1 itv2 traces l =
+    match SymbolTable.find_opt path1 callee_symbol_table with
+    | Some (lb1, ub1) ->
+        if Itv.eq itv2 bot then (lb1, Bottom, TraceSet.empty) :: (ub1, Bottom, TraceSet.empty) :: l
+        else (lb1, NonBottom (lb itv2), traces) :: (ub1, NonBottom (ub itv2), traces) :: l
+    | _ ->
+        l
   in
   let add_pair_sym_main_value v1 v2 ~e2_opt l =
     Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var ->
@@ -535,12 +537,12 @@ let get_matching_pairs
     Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var ->
         (var, Relation.SymExp.of_sym s2) :: l )
   in
-  let add_pair_val v1 v2 ~e2_opt (bound_pairs, rel_pairs) =
+  let add_pair_val path1 v1 v2 ~e2_opt (bound_pairs, rel_pairs) =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
     let bound_pairs =
-      bound_pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2)
-      |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2)
-      |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2)
+      bound_pairs |> add_pair_itv (SymbolPath.normal path1) (get_itv v2) (Val.get_traces v2)
+      |> add_pair_itv (SymbolPath.offset path1) (get_offset v2) (Val.get_traces v2)
+      |> add_pair_itv (SymbolPath.length path1) (get_size v2) (Val.get_traces v2)
     in
     let rel_pairs =
       rel_pairs |> add_pair_sym_main_value v1 v2 ~e2_opt
@@ -549,44 +551,44 @@ let get_matching_pairs
     in
     (bound_pairs, rel_pairs)
   in
-  let add_pair_field v1 v2 pairs fn =
+  let add_pair_field path1 v1 v2 pairs fn =
     add_ret_alias (append_field v1 fn) (append_field v2 fn) ;
-    let v1' = deref_field v1 fn callee_mem in
+    let path1' = SymbolPath.field (SymbolPath.index path1) fn in
+    let v1' = deref_field v1 fn callee_exit_mem in
     let v2' = deref_field v2 fn caller_mem in
-    add_pair_val v1' v2' ~e2_opt:None pairs
+    add_pair_val path1' v1' v2' ~e2_opt:None pairs
   in
-  let add_pair_ptr typ v1 v2 pairs =
+  let add_pair_ptr typ path1 v1 v2 pairs =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
     match typ.Typ.desc with
     | Typ.Tptr ({desc= Tstruct typename}, _) -> (
       match Tenv.lookup tenv typename with
       | Some str ->
           let fns = List.map ~f:get_field_name str.Typ.Struct.fields in
-          List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns
+          List.fold ~f:(add_pair_field path1 v1 v2) ~init:pairs fns
       | _ ->
           pairs )
     | Typ.Tptr (_, _) ->
-        let v1' = deref_ptr v1 callee_mem in
+        let path1' = SymbolPath.index path1 in
+        let v1' = deref_ptr v1 callee_exit_mem in
         let v2' = deref_ptr v2 caller_mem in
-        add_pair_val v1' v2' ~e2_opt:None pairs
+        add_pair_val path1' v1' v2' ~e2_opt:None pairs
     | _ ->
         pairs
   in
   let bound_pairs, rel_pairs =
-    ([], []) |> add_pair_val formal actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ formal actual
+    ([], []) |> add_pair_val formal callee_v actual ~e2_opt:actual_exp_opt
+    |> add_pair_ptr typ formal callee_v actual
   in
   (bound_pairs, !ret_alias, rel_pairs)
 
 
 let subst_map_of_bound_pairs
-    : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
+    : (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
       -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t =
  fun pairs ->
   let add_pair (bound_map, trace_map) (formal, actual, traces) =
-    if Itv.Bound.is_const formal |> Option.is_some then (bound_map, trace_map)
-    else
-      let symbol = Itv.Bound.get_one_symbol formal in
-      (Itv.SymbolMap.add symbol actual bound_map, Itv.SymbolMap.add symbol traces trace_map)
+    (Itv.SymbolMap.add formal actual bound_map, Itv.SymbolMap.add formal traces trace_map)
   in
   List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs
 
@@ -616,17 +618,17 @@ let rec list_fold2_def
 
 
 let get_subst_map
-    : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
-      -> callee_ret_alias:AliasTarget.t option
+    : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Itv.SymbolTable.summary_t
+      -> Mem.astate
       -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t)
          * AliasTarget.t option
          * Relation.SubstMap.t =
- fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias ->
+ 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 formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in
+    let callee_v = Mem.find_heap (Loc.of_pvar formal) callee_exit_mem in
     let new_bound_matching, ret_alias', new_rel_matching =
-      get_matching_pairs tenv formal actual actual_exp typ caller_mem callee_entry_mem
-        ~callee_ret_alias
+      get_matching_pairs tenv (Itv.SymbolPath.of_pvar formal) callee_v actual actual_exp typ
+        caller_mem callee_symbol_table callee_exit_mem
     in
     ( List.rev_append new_bound_matching bound_l
     , Option.first_some ret_alias ret_alias'
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index a23af28bb..959f80a01 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -80,19 +80,21 @@ module Exec = struct
     -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
 
   let decl_sym_arr
-      : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
-        -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t
+      : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
+        -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t
         -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
         -> Dom.Mem.astate -> Dom.Mem.astate =
-   fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num
-       ~new_sym_num ~new_alloc_num mem ->
+   fun ~decl_sym_val pname symbol_table path tenv ~node_hash location ~depth loc typ ?offset ?size
+       ~inst_num ~new_sym_num ~new_alloc_num mem ->
     let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in
     let offset =
-      option_value offset (fun () -> Itv.make_sym pname (Itv.SymbolPath.offset path) new_sym_num)
+      option_value offset (fun () ->
+          Itv.make_sym pname symbol_table (Itv.SymbolPath.offset path) new_sym_num )
     in
     let size =
       option_value size (fun () ->
-          Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num )
+          Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
+      )
     in
     let alloc_num = Itv.Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
@@ -128,12 +130,12 @@ module Exec = struct
 
 
   let decl_sym_arraylist
-      : Typ.Procname.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t
+      : Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t
         -> new_sym_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate =
-   fun pname path location loc ~new_sym_num mem ->
+   fun pname symbol_table path location loc ~new_sym_num mem ->
     let size =
-      Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num |> Dom.Val.of_itv
-      |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
+      Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
+      |> Dom.Val.of_itv |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
     in
     Dom.Mem.add_heap loc size mem
 
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli
index 546eaceb8..d5d3277ac 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.mli
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli
@@ -34,10 +34,10 @@ module Exec : sig
     -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
 
   val decl_sym_arr :
-    decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
-    -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t
-    -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
-    -> Dom.Mem.astate
+    decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
+    -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t
+    -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
+    -> Dom.Mem.astate -> Dom.Mem.astate
 
   val decl_sym_java_ptr :
     decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
@@ -45,8 +45,8 @@ module Exec : sig
     -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
 
   val decl_sym_arraylist :
-    Typ.Procname.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t -> new_sym_num:Itv.Counter.t
-    -> Dom.Mem.astate -> Dom.Mem.astate
+    Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t
+    -> new_sym_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
 
   val init_array_fields :
     Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index b11486c0a..71b754804 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -45,7 +45,7 @@ module Boolean = struct
 end
 
 module BoundEnd = struct
-  type t = LowerBound | UpperBound
+  type t = LowerBound | UpperBound [@@deriving compare]
 
   let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
 
@@ -54,8 +54,11 @@ end
 
 module SymbolPath = struct
   type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial
+  [@@deriving compare]
+
+  type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare]
 
-  type t = Normal of partial | Offset of partial | Length of partial
+  let equal = [%compare.equal : t]
 
   let of_pvar pvar = Pvar pvar
 
@@ -99,7 +102,7 @@ module Symbol = struct
 
   let equal = [%compare.equal : t]
 
-  let paths_equal s1 s2 = phys_equal s1.path s2.path
+  let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path
 
   let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
    fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end}
@@ -116,6 +119,35 @@ module Symbol = struct
   let is_unsigned : t -> bool = fun x -> x.unsigned
 end
 
+module SymbolTable = struct
+  module M = PrettyPrintable.MakePPMap (SymbolPath)
+
+  type summary_t = (Symbol.t * Symbol.t) M.t
+
+  let find_opt = M.find_opt
+
+  let pp = M.pp ~pp_value:(fun fmt (lb, ub) -> F.fprintf fmt "[%a, %a]" Symbol.pp lb Symbol.pp ub)
+
+  type t = summary_t ref
+
+  let empty () = ref M.empty
+
+  let lookup ~unsigned pname path symbol_table new_sym_num =
+    match M.find_opt path !symbol_table with
+    | Some s ->
+        s
+    | None ->
+        let s =
+          ( Symbol.make ~unsigned pname path LowerBound (Counter.next new_sym_num)
+          , Symbol.make ~unsigned pname path UpperBound (Counter.next new_sym_num) )
+        in
+        symbol_table := M.add path s !symbol_table ;
+        s
+
+
+  let summary_of x = !x
+end
+
 exception Symbol_not_found of Symbol.t
 
 module SymbolMap = struct
@@ -178,9 +210,10 @@ module SymLinear = struct
     M.for_all2 ~f:le_one_pair x y
 
 
-  let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
-   fun ~unsigned pname path bound_end i ->
-    singleton_one (Symbol.make ~unsigned pname path bound_end i)
+  let make : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t * t =
+   fun ~unsigned pname symbol_table path new_sym_num ->
+    let lb, ub = SymbolTable.lookup ~unsigned pname path symbol_table new_sym_num in
+    (singleton_one lb, singleton_one ub)
 
 
   let eq : t -> t -> bool =
@@ -1376,17 +1409,10 @@ module ItvPure = struct
 
   let of_int n = of_bound (Bound.of_int n)
 
-  let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t =
-   fun ~unsigned pname path new_sym_num ->
-    let lower =
-      Bound.of_sym
-        (SymLinear.make ~unsigned pname path BoundEnd.LowerBound (Counter.next new_sym_num))
-    in
-    let upper =
-      Bound.of_sym
-        (SymLinear.make ~unsigned pname path BoundEnd.UpperBound (Counter.next new_sym_num))
-    in
-    (lower, upper)
+  let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t =
+   fun ~unsigned pname symbol_table path new_sym_num ->
+    let lb, ub = SymLinear.make ~unsigned pname symbol_table path new_sym_num in
+    (Bound.of_sym lb, Bound.of_sym ub)
 
 
   let mone = of_bound Bound.mone
@@ -1820,9 +1846,9 @@ let plus : t -> t -> t = lift2 ItvPure.plus
 
 let minus : t -> t -> t = lift2 ItvPure.minus
 
-let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t =
- fun ?(unsigned= false) pname path new_sym_num ->
-  NonBottom (ItvPure.make_sym ~unsigned pname path new_sym_num)
+let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t =
+ fun ?(unsigned= false) pname symbol_table path new_sym_num ->
+  NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num)
 
 
 let neg : t -> t = lift1 ItvPure.neg
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index be0b30747..38ea390bb 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -32,9 +32,9 @@ module Boolean : sig
 end
 
 module SymbolPath : sig
-  type partial
+  type partial [@@deriving compare]
 
-  type t
+  type t [@@deriving compare]
 
   val of_pvar : Pvar.t -> partial
 
@@ -53,6 +53,20 @@ module Symbol : sig
   type t
 end
 
+module SymbolTable : sig
+  type summary_t
+
+  val pp : F.formatter -> summary_t -> unit
+
+  val find_opt : SymbolPath.t -> summary_t -> (Symbol.t * Symbol.t) option
+
+  type t
+
+  val empty : unit -> t
+
+  val summary_of : t -> summary_t
+end
+
 module SymbolMap : PrettyPrintable.PPMap with type key = Symbol.t
 
 module Bound : sig
@@ -66,8 +80,6 @@ module Bound : sig
 
   val is_symbolic : t -> bool
 
-  val get_one_symbol : t -> Symbol.t
-
   val gt : t -> t -> bool
 
   val le : t -> t -> bool
@@ -197,7 +209,7 @@ val of_int_lit : IntLit.t -> t
 
 val of_int64 : Int64.t -> t
 
-val make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t
+val make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
 
 val lb : t -> Bound.t
 
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index 246ef67e5..fa0c028e5 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -58,12 +58,11 @@ module TransferFunctionsNodesBasicCost = struct
             callee_cost Typ.Procname.pp callee_pname
       | Some inferbo_summary ->
           let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
-          let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in
+          let callee_symbol_table = BufferOverrunDomain.Summary.get_symbol_table inferbo_summary in
           let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in
-          let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in
           let (subst_map, _), _, _ =
             BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem
-              callee_entry_mem ~callee_ret_alias
+              callee_symbol_table callee_exit_mem
           in
           BasicCost.subst callee_cost subst_map