diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml
index e5dd92949..5a677ad56 100644
--- a/infer/src/backend/callbacks.ml
+++ b/infer/src/backend/callbacks.ml
@@ -179,10 +179,6 @@ let iterate_callbacks store_summary call_graph exe_env =
     (iterate_cluster_callbacks originally_defined_procs exe_env)
     (cluster procs_to_analyze);
 
-  IList.iter
-    (fun proc_name  ->
-       let tenv = Exe_env.get_tenv ~create:true exe_env proc_name in
-       store_summary tenv proc_name)
-    procs_to_analyze;
+  IList.iter store_summary procs_to_analyze;
 
   Config.curr_language := saved_language
diff --git a/infer/src/backend/callbacks.mli b/infer/src/backend/callbacks.mli
index d71368277..cab2874fd 100644
--- a/infer/src/backend/callbacks.mli
+++ b/infer/src/backend/callbacks.mli
@@ -45,4 +45,4 @@ val register_cluster_callback : Config.language option -> cluster_callback_t ->
 val unregister_all_callbacks : unit -> unit
 
 (** Invoke all the registered callbacks. *)
-val iterate_callbacks : (Tenv.t -> Procname.t -> unit) -> Cg.t -> Exe_env.t -> unit
+val iterate_callbacks : (Procname.t -> unit) -> Cg.t -> Exe_env.t -> unit
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 280985521..31c4b77b0 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -1299,10 +1299,11 @@ let update_summary tenv prev_summary specs phase proc_name elapsed res =
       symops;
       stats_failure;
     } in
-  let payload =
-    { prev_summary.Specs.payload with
-      Specs.preposts = Some new_specs;
-    } in
+  let preposts =
+    match phase with
+    | Specs.FOOTPRINT -> Some new_specs
+    | Specs.RE_EXECUTION -> Some (IList.map (Specs.NormSpec.erase_join_info_pre tenv) new_specs) in
+  let payload = { prev_summary.Specs.payload with Specs.preposts; } in
   { prev_summary with
     Specs.phase;
     stats;
@@ -1424,11 +1425,8 @@ let interprocedural_algorithm exe_env : unit =
         None in
   let process_one_proc proc_name =
     match to_analyze proc_name with
-    | Some pdesc ->
-        let tenv = Exe_env.get_tenv ~create:true exe_env proc_name in
-        Ondemand.analyze_proc_name tenv ~propagate_exceptions:false pdesc proc_name
-    | None ->
-        () in
+    | Some pdesc -> Ondemand.analyze_proc_name ~propagate_exceptions:false pdesc proc_name
+    | None -> () in
   IList.iter process_one_proc procs_to_analyze
 
 (** Perform the analysis of an exe_env *)
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index 0fa5fe7af..886f89375 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -102,7 +102,7 @@ let restore_global_state st =
   Timeout.resume_previous_timeout ()
 
 
-let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc =
+let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc =
   let curr_pname = Procdesc.get_proc_name curr_pdesc in
   let callee_pname = Procdesc.get_proc_name callee_pdesc in
 
@@ -146,7 +146,7 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
         Specs.status = Specs.INACTIVE;
         timestamp = summary.Specs.timestamp + 1 } in
     Specs.add_summary callee_pname summary';
-    Checkers.ST.store_summary tenv callee_pname;
+    Checkers.ST.store_summary callee_pname;
     Printer.write_proc_html source false callee_pdesc in
 
   let log_error_and_continue exn kind =
@@ -187,14 +187,13 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
           log_error_and_continue exn (FKcrash (Printexc.to_string exn))
 
 
-let analyze_proc_desc tenv ~propagate_exceptions curr_pdesc callee_pdesc =
+let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc =
   let callee_pname = Procdesc.get_proc_name callee_pdesc in
   let proc_attributes = Procdesc.get_attributes callee_pdesc in
   match !callbacks_ref with
   | Some callbacks
     when should_be_analyzed proc_attributes callee_pname ->
-      run_proc_analysis tenv
-        ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc
+      run_proc_analysis ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc
   | _ -> ()
 
 
@@ -202,17 +201,15 @@ let analyze_proc_desc tenv ~propagate_exceptions curr_pdesc callee_pdesc =
 (** analyze_proc_name curr_pdesc proc_name
     performs an on-demand analysis of proc_name
     triggered during the analysis of curr_pname. *)
-let analyze_proc_name tenv ~propagate_exceptions curr_pdesc callee_pname =
+let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname =
 
   match !callbacks_ref with
   | Some callbacks
     when procedure_should_be_analyzed callee_pname ->
       begin
         match callbacks.get_proc_desc callee_pname with
-        | Some callee_pdesc ->
-            analyze_proc_desc tenv ~propagate_exceptions curr_pdesc callee_pdesc
-        | None ->
-            ()
+        | Some callee_pdesc -> analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc
+        | None -> ()
       end
   | _ ->
       () (* skipping *)
diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli
index 9b768e26c..8b39f41a7 100644
--- a/infer/src/backend/ondemand.mli
+++ b/infer/src/backend/ondemand.mli
@@ -30,12 +30,12 @@ val get_proc_desc : get_proc_desc
 (** analyze_proc_desc curr_pdesc callee_pdesc
     performs an on-demand analysis of callee_pdesc
     triggered during the analysis of curr_pdesc. *)
-val analyze_proc_desc : Tenv.t -> propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> unit
+val analyze_proc_desc : propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> unit
 
 (** analyze_proc_name curr_pdesc proc_name
     performs an on-demand analysis of proc_name
     triggered during the analysis of curr_pdesc. *)
-val analyze_proc_name : Tenv.t -> propagate_exceptions:bool -> Procdesc.t -> Procname.t -> unit
+val analyze_proc_name : propagate_exceptions:bool -> Procdesc.t -> Procname.t -> unit
 
 (** Check if the procedure called needs to be analyzed. *)
 val procedure_should_be_analyzed : Procname.t -> bool
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 03026d54e..5ab934bca 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -554,14 +554,7 @@ let summary_serializer : summary Serialization.serializer =
   Serialization.create_serializer Serialization.summary_key
 
 (** Save summary for the procedure into the spec database *)
-let store_summary tenv pname (summ: summary) =
-  let process_payload payload = match payload.preposts with
-    | Some specs ->
-        { payload with
-          preposts = Some (IList.map (NormSpec.erase_join_info_pre tenv) specs);
-        }
-    | None -> payload in
-  let summ1 = { summ with payload = process_payload summ.payload } in
+let store_summary pname (summ1: summary) =
   let summ2 = if Config.save_compact_summaries
     then summary_compact (Sil.create_sharing_env ()) summ1
     else summ1 in
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 0b2835151..fb460fb57 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -75,6 +75,8 @@ type 'a spec = { pre: 'a Jprop.t; posts: ('a Prop.t * Paths.Path.t) list; visite
 (** encapsulate type for normalized specs *)
 module NormSpec : sig
   type t
+
+  val erase_join_info_pre : Tenv.t -> t -> t (** Erase join info from pre of spec *)
 end
 
 (** module for tracing stats of function calls *)
@@ -275,7 +277,7 @@ val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
 val res_dir_specs_filename : Procname.t -> DB.filename
 
 (** Save summary for the procedure into the spec database *)
-val store_summary : Tenv.t -> Procname.t -> summary -> unit
+val store_summary : Procname.t -> summary -> unit
 
 (** Return a compact representation of the summary *)
 val summary_compact : Sil.sharing_env -> summary -> summary
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index f6c9ed5c5..522016ccf 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -641,12 +641,12 @@ let resolve_and_analyze
      whether the method is defined or generated by the specialization *)
   let analyze_ondemand resolved_pname : unit =
     if Procname.equal resolved_pname callee_proc_name then
-      Ondemand.analyze_proc_name tenv ~propagate_exceptions:true caller_pdesc callee_proc_name
+      Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_proc_name
     else
       (* Create the type sprecialized procedure description and analyze it directly *)
       Option.may
         (fun specialized_pdesc ->
-           Ondemand.analyze_proc_desc tenv ~propagate_exceptions:true caller_pdesc specialized_pdesc)
+           Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
         (match Ondemand.get_proc_desc resolved_pname with
          | Some resolved_proc_desc ->
              Some resolved_proc_desc
@@ -1092,7 +1092,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
               let resolved_pnames =
                 resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in
               let exec_one_pname pname =
-                Ondemand.analyze_proc_name tenv ~propagate_exceptions:true current_pdesc pname;
+                Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc pname;
                 let exec_skip_call ret_annots ret_type = skip_call norm_prop path pname ret_annots
                     loc ret_id (Some ret_type) url_handled_args in
                 match Specs.get_summary pname with
@@ -1116,7 +1116,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                 | resolved_pname :: _ -> resolved_pname
                 | [] -> callee_pname in
               Ondemand.analyze_proc_name
-                tenv ~propagate_exceptions:true current_pdesc resolved_pname;
+                ~propagate_exceptions:true current_pdesc resolved_pname;
               let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in
               let ret_typ_opt = Option.map Procdesc.get_ret_type callee_pdesc_opt in
               let sentinel_result =
diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml
index fe2e0c100..1066a932a 100644
--- a/infer/src/checkers/BoundedCallTree.ml
+++ b/infer/src/checkers/BoundedCallTree.ml
@@ -77,11 +77,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module Domain = Domain
   type extras = extras_t
 
-  let stacktree_of_astate tenv pdesc astate loc location_type get_proc_desc =
+  let stacktree_of_astate pdesc astate loc location_type get_proc_desc =
     let procs = Domain.elements astate in
     let callees = IList.map
         (fun pn ->
-           match SpecSummary.read_summary tenv pdesc pn with
+           match SpecSummary.read_summary pdesc pn with
            | None | Some None -> (match get_proc_desc pn with
                | None -> stacktree_stub_of_procname pn
                (* This can happen when the callee is in the same cluster/ buck
@@ -94,10 +94,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         procs in
     stacktree_of_pdesc pdesc ~loc ~callees location_type
 
-  let output_json_summary tenv pdesc astate loc location_type get_proc_desc =
+  let output_json_summary pdesc astate loc location_type get_proc_desc =
     let caller = Procdesc.get_proc_name pdesc in
-    let stacktree =
-      stacktree_of_astate tenv pdesc astate loc location_type get_proc_desc in
+    let stacktree = stacktree_of_astate pdesc astate loc location_type get_proc_desc in
     let dir = Filename.concat Config.results_dir "crashcontext" in
     let suffix = F.sprintf "%s_%d" location_type loc.Location.line in
     let fname = F.sprintf "%s.%s.json"
@@ -111,7 +110,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Sil.Call (_, Const (Const.Cfun pn), _, loc, _) ->
         let get_proc_desc = proc_data.ProcData.extras.get_proc_desc in
         let traces = proc_data.ProcData.extras.stacktraces in
-        let tenv = proc_data.ProcData.tenv in
         let caller = Procdesc.get_proc_name proc_data.ProcData.pdesc in
         let matches_proc frame =
           let matches_class pname = match pname with
@@ -136,7 +134,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let new_astate = Domain.add pn astate in
             if Stacktrace.frame_matches_location frame loc then begin
               let pdesc = proc_data.ProcData.pdesc in
-              output_json_summary tenv pdesc new_astate loc "call_site" get_proc_desc
+              output_json_summary pdesc new_astate loc "call_site" get_proc_desc
             end;
             new_astate
           with
diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml
index c0014cc1d..f6ba36a5d 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -54,7 +54,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let at_least_bottom =
     Domain.join (Domain.NonBottom SiofTrace.initial)
 
-  let exec_instr astate { ProcData.pdesc; tenv } _ (instr : Sil.instr) = match instr with
+  let exec_instr astate { ProcData.pdesc; } _ (instr : Sil.instr) = match instr with
     | Load (_, exp, _, loc)
     | Store (_, _, exp, loc)
     | Prune (exp, loc, _, _) ->
@@ -62,7 +62,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Call (_, Const (Cfun callee_pname), params, loc, _) ->
         let callsite = CallSite.make callee_pname loc in
         let callee_globals =
-          match Summary.read_summary tenv pdesc callee_pname with
+          match Summary.read_summary pdesc callee_pname with
           | Some (Domain.NonBottom trace) ->
               Domain.NonBottom (SiofTrace.with_callsite trace callsite)
           | _ ->
@@ -98,12 +98,12 @@ let is_foreign tu_opt v =
     | None -> assert false in
   Option.map_default (fun f -> not (is_orig_file f)) false (Pvar.get_source_file v)
 
-let report_siof tenv trace pdesc gname loc =
+let report_siof trace pdesc gname loc =
   let tu_opt =
     let attrs = Procdesc.get_attributes pdesc in
     attrs.ProcAttributes.translation_unit in
   let trace_of_pname pname =
-    match Summary.read_summary tenv pdesc pname with
+    match Summary.read_summary pdesc pname with
     | Some (SiofDomain.NonBottom summary) -> summary
     | _ -> SiofTrace.initial in
 
@@ -147,7 +147,7 @@ let report_siof tenv trace pdesc gname loc =
 
   IList.iter report_one_path (SiofTrace.get_reportable_sink_paths trace ~trace_of_pname)
 
-let siof_check tenv pdesc gname = function
+let siof_check pdesc gname = function
   | Some (SiofDomain.NonBottom post) ->
       let attrs = Procdesc.get_attributes pdesc in
       let foreign_global_sinks =
@@ -155,15 +155,15 @@ let siof_check tenv pdesc gname = function
           (fun sink -> is_foreign attrs.ProcAttributes.translation_unit (SiofTrace.Sink.kind sink))
           (SiofTrace.sinks post) in
       if not (SiofTrace.Sinks.is_empty foreign_global_sinks)
-      then report_siof tenv post pdesc gname attrs.ProcAttributes.loc;
+      then report_siof post pdesc gname attrs.ProcAttributes.loc;
   | Some SiofDomain.Bottom | None ->
       ()
 
-let checker ({ Callbacks.tenv; proc_desc } as callback) =
+let checker ({ Callbacks.proc_desc; } as callback) =
   let post = Interprocedural.checker callback ProcData.empty_extras in
   let pname = Procdesc.get_proc_name proc_desc in
   match Procname.get_global_name_of_initializer pname with
   | Some gname ->
-      siof_check tenv proc_desc gname post
+      siof_check proc_desc gname post
   | None ->
       ()
diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index d138ad9d2..ac2fab8f6 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -63,7 +63,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       pathdomainstate
       (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None))
 
-  let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; tenv } _ =
+  let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ =
     let is_unprotected is_locked =
       not is_locked && not (Procdesc.is_java_synchronized pdesc) in
     function
@@ -77,7 +77,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               false, snd astate
           | None ->
               begin
-                match Summary.read_summary tenv pdesc pn with
+                match Summary.read_summary pdesc pn with
                 | Some ((callee_lockstate, _) as summary) ->
                     let lockstate' = callee_lockstate || lockstate in
                     let _, read_writestate' =
diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml
index d61cce828..9026f4ccf 100644
--- a/infer/src/checkers/abstractInterpreter.ml
+++ b/infer/src/checkers/abstractInterpreter.ml
@@ -155,7 +155,7 @@ module MakeNoCFG
           post_opt
         end
       else
-        Summ.read_summary tenv proc_desc proc_name
+        Summ.read_summary proc_desc proc_name
   end
 end
 
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index e4650812c..f64295032 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -321,7 +321,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let call_site = CallSite.make callee_pname call_loc in
         begin
           (* Runs the analysis of callee_pname if not already analyzed *)
-          match Summary.read_summary tenv pdesc callee_pname with
+          match Summary.read_summary pdesc callee_pname with
           | Some Domain.NonBottom (call_map, _) ->
               add_call call_map tenv callee_pname caller_pname call_site astate
           | None ->
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index 02a481777..331e777bf 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -55,13 +55,13 @@ module ST = struct
           end
     end
 
-  let store_summary tenv proc_name =
+  let store_summary proc_name =
     Option.may
       (fun summary ->
          let summary' =
            { summary with
              Specs.timestamp = summary.Specs.timestamp + 1 } in
-         try Specs.store_summary tenv proc_name summary' with Sys_error s -> L.err "%s@." s)
+         try Specs.store_summary proc_name summary' with Sys_error s -> L.err "%s@." s)
       (Specs.get_summary proc_name)
 
   let report_error tenv
diff --git a/infer/src/checkers/checkers.mli b/infer/src/checkers/checkers.mli
index edd414c41..7d88ebc4d 100644
--- a/infer/src/checkers/checkers.mli
+++ b/infer/src/checkers/checkers.mli
@@ -36,7 +36,7 @@ module ST : sig
     unit
 
   (** Store the summary to a .specs file. *)
-  val store_summary : Tenv.t -> Procname.t -> unit
+  val store_summary : Procname.t -> unit
 
 end (* ST *)
 
diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml
index 3c18ebb85..4e71d73a5 100644
--- a/infer/src/checkers/summary.ml
+++ b/infer/src/checkers/summary.ml
@@ -25,7 +25,7 @@ module type S = sig
   val write_summary : Procname.t -> summary -> unit
   (* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to
      create the summary if needed *)
-  val read_summary : Tenv.t -> Procdesc.t -> Procname.t -> summary option
+  val read_summary : Procdesc.t -> Procname.t -> summary option
 end
 
 module Make (H : Helper) = struct
@@ -40,8 +40,8 @@ module Make (H : Helper) = struct
     | None ->
         failwithf "Summary for %a should exist, but does not!@." Procname.pp pname
 
-  let read_summary tenv caller_pdesc callee_pname =
-    Ondemand.analyze_proc_name tenv ~propagate_exceptions:false caller_pdesc callee_pname;
+  let read_summary caller_pdesc callee_pname =
+    Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname;
     match Specs.get_summary callee_pname with
     | None -> None
     | Some summary -> H.read_from_payload summary.Specs.payload
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index cf9debb06..f3293e5ed 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -563,7 +563,7 @@ let typecheck_instr
        loc,
        cflags)
     ->
-      Ondemand.analyze_proc_name tenv ~propagate_exceptions:true curr_pdesc callee_pname;
+      Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname;
       let callee_attributes =
         match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
         | Some proc_attributes ->
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 0cbe7445f..28131f38e 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -156,7 +156,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     (* log any reportable source-sink flows in [trace] and remove logged sinks from the trace *)
     let report_and_filter_trace trace callee_site (proc_data : formal_map ProcData.t) =
       let trace_of_pname pname =
-        match Summary.read_summary proc_data.tenv proc_data.pdesc pname with
+        match Summary.read_summary proc_data.pdesc pname with
         | Some summary ->
             let join_output_trace acc { QuandarySummary.output_trace; } =
               TraceDomain.join (TaintSpecification.of_summary_trace output_trace) acc in
@@ -434,7 +434,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                 (* don't use a summary for a procedure that is a direct source or sink *)
                 astate_with_source
               else
-                match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with
+                match Summary.read_summary proc_data.pdesc callee_pname with
                 | Some summary ->
                     apply_summary ret actuals summary astate_with_source proc_data call_site
                 | None ->