diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml
index 09668092d..d8796f64b 100644
--- a/infer/src/IR/Cfg.ml
+++ b/infer/src/IR/Cfg.ml
@@ -68,9 +68,13 @@ let store source_file cfg =
 let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr option =
   let found instr instr' =
     L.(debug Analysis Verbose)
-      "XX inline_synthetic_method found instr: %a@." (Sil.pp_instr Pp.text) instr ;
+      "XX inline_synthetic_method found instr: %a@."
+      (Sil.pp_instr ~print_types:true Pp.text)
+      instr ;
     L.(debug Analysis Verbose)
-      "XX inline_synthetic_method instr': %a@." (Sil.pp_instr Pp.text) instr' ;
+      "XX inline_synthetic_method instr': %a@."
+      (Sil.pp_instr ~print_types:true Pp.text)
+      instr' ;
     Some instr'
   in
   let do_instr instr =
diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml
index 86fb2ab8c..602defe1f 100644
--- a/infer/src/IR/Exp.ml
+++ b/infer/src/IR/Exp.ml
@@ -252,9 +252,12 @@ and pp_captured_var pe pp_t f (exp, var, typ) =
       F.fprintf f "(%a %a:%a)" (pp_ pe pp_t) exp (Pvar.pp pe) var (Typ.pp pe) typ
 
 
-let pp_printenv pe pp_typ f e = pp_ pe (pp_typ pe) f e
+let pp_printenv ~print_types pe f e =
+  let pp_typ = if print_types then Typ.pp_full else Typ.pp in
+  pp_ pe (pp_typ pe) f e
 
-let pp f e = pp_printenv Pp.text Typ.pp f e
+
+let pp f e = pp_printenv ~print_types:false Pp.text f e
 
 let to_string e = F.asprintf "%a" pp e
 
diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli
index 209864081..3ee3c4059 100644
--- a/infer/src/IR/Exp.mli
+++ b/infer/src/IR/Exp.mli
@@ -127,7 +127,7 @@ val program_vars : t -> Pvar.t Sequence.t
 val fold_captured : f:('a -> t -> 'a) -> t -> 'a -> 'a
 (** Fold over the expressions captured by this expression. *)
 
-val pp_printenv : Pp.env -> (Pp.env -> F.formatter -> Typ.t -> unit) -> F.formatter -> t -> unit
+val pp_printenv : print_types:bool -> Pp.env -> F.formatter -> t -> unit
 
 val pp : F.formatter -> t -> unit
 
diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml
index e1b04390f..886a6b025 100644
--- a/infer/src/IR/Instrs.ml
+++ b/infer/src/IR/Instrs.ml
@@ -145,4 +145,5 @@ let last (type r) (t : r t) =
 
 let find_map t ~f = Container.find_map ~iter t ~f
 
-let pp pe fmt t = iter t ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr pe) instr)
+let pp pe fmt t =
+  iter t ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr ~print_types:false pe) instr)
diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml
index 3e2d6cf6b..6234054d7 100644
--- a/infer/src/IR/Sil.ml
+++ b/infer/src/IR/Sil.ml
@@ -257,7 +257,7 @@ let pp_seq_diff pp pe0 f =
 
 
 (** Pretty print an expression. *)
-let pp_exp_printenv pe0 f e0 =
+let pp_exp_printenv ?(print_types = false) pe0 f e0 =
   let pe, changed = color_pre_wrapper pe0 f e0 in
   let e =
     match pe.Pp.obj_sub with
@@ -268,7 +268,7 @@ let pp_exp_printenv pe0 f e0 =
   in
   if not (Exp.equal e0 e) then
     match e with Exp.Lvar pvar -> Pvar.pp_value f pvar | _ -> assert false
-  else Exp.pp_printenv pe Typ.pp f e ;
+  else Exp.pp_printenv ~print_types pe f e ;
   color_post_wrapper changed f
 
 
@@ -299,7 +299,7 @@ let pp_texp_full pe f = function
       F.fprintf f "%a%a%a%a" (Typ.pp_full pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp
         subtype
   | e ->
-      Exp.pp_printenv pe Typ.pp_full f e
+      Exp.pp_printenv ~print_types:true pe f e
 
 
 (** Dump a type expression with all the details. *)
@@ -380,19 +380,22 @@ let if_kind_to_string = function
 
 
 (** Pretty print an instruction. *)
-let pp_instr pe0 f instr =
+let pp_instr ~print_types pe0 f instr =
+  let pp_typ = if print_types then Typ.pp_full else Typ.pp in
   let pe, changed = color_pre_wrapper pe0 f instr in
   ( match instr with
   | Load (id, e, t, loc) ->
-      F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv pe) e (Typ.pp pe) t Location.pp loc
-  | Store (e1, t, e2, loc) ->
-      F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv pe) e1 (Typ.pp pe) t (pp_exp_printenv pe) e2
+      F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e (pp_typ pe0) t
         Location.pp loc
+  | Store (e1, t, e2, loc) ->
+      F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) t
+        (pp_exp_printenv ~print_types pe) e2 Location.pp loc
   | Prune (cond, loc, true_branch, _) ->
-      F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv pe) cond true_branch Location.pp loc
+      F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv ~print_types pe) cond true_branch
+        Location.pp loc
   | Call ((id, _), e, arg_ts, loc, cf) ->
       F.fprintf f "%a=" Ident.pp id ;
-      F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv pe) e
+      F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv ~print_types pe) e
         (Pp.comma_seq (pp_exp_typ pe))
         arg_ts CallFlags.pp cf Location.pp loc
   | Nullify (pvar, loc) ->
@@ -423,7 +426,7 @@ let add_with_block_parameters_flag instr =
 let is_block_pvar pvar = Typ.has_block_prefix (Mangled.to_string (Pvar.get_name pvar))
 
 (** Dump an instruction. *)
-let d_instr (i : instr) = L.add_print_with_pe ~color:Pp.Green pp_instr i
+let d_instr (i : instr) = L.add_print_with_pe ~color:Pp.Green (pp_instr ~print_types:true) i
 
 let pp_atom pe0 f a =
   let pe, changed = color_pre_wrapper pe0 f a in
diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli
index 3951e8402..01cc77bf5 100644
--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@@ -255,7 +255,7 @@ val color_pre_wrapper : Pp.env -> F.formatter -> 'a -> Pp.env * bool
 val color_post_wrapper : bool -> F.formatter -> unit
 (** Close color annotation if changed *)
 
-val pp_exp_printenv : Pp.env -> F.formatter -> Exp.t -> unit
+val pp_exp_printenv : ?print_types:bool -> Pp.env -> F.formatter -> Exp.t -> unit
 (** Pretty print an expression. *)
 
 val d_exp : Exp.t -> unit
@@ -288,7 +288,7 @@ val instr_get_exps : instr -> Exp.t list
 val if_kind_to_string : if_kind -> string
 (** Pretty print an if_kind *)
 
-val pp_instr : Pp.env -> F.formatter -> instr -> unit
+val pp_instr : print_types:bool -> Pp.env -> F.formatter -> instr -> unit
 (** Pretty print an instruction. *)
 
 val d_instr : instr -> unit
diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index f84d04a2d..638ba287d 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/infer/src/absint/AbstractInterpreter.ml
@@ -151,7 +151,9 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
           | exn ->
               IExn.reraise_after exn ~f:(fun () ->
                   if not !logged_error then (
-                    L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ;
+                    L.internal_error "In instruction %a@\n"
+                      (Sil.pp_instr ~print_types:true Pp.text)
+                      instr ;
                     logged_error := true ) )
         in
         Instrs.fold ~f:compute_post ~init:pre instrs
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 6cfcdf826..47287c26a 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -1112,7 +1112,7 @@ let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) =
         Format.fprintf fmt "Skip %s" s
   in
   let instr_string i =
-    let pp f = Sil.pp_instr Pp.text f i in
+    let pp f = Sil.pp_instr ~print_types:false Pp.text f i in
     let str = F.asprintf "%t" pp in
     Escape.escape_dotty str
   in
diff --git a/infer/src/biabduction/SymExecBlocks.ml b/infer/src/biabduction/SymExecBlocks.ml
index d93b42e99..511915869 100644
--- a/infer/src/biabduction/SymExecBlocks.ml
+++ b/infer/src/biabduction/SymExecBlocks.ml
@@ -84,7 +84,9 @@ let resolve_method_with_block_args_and_analyze ~caller_pdesc pname act_params =
       in
       Logging.(debug Analysis Verbose) "Instructions of specialized method:@." ;
       Procdesc.iter_instrs
-        (fun _ instr -> Logging.(debug Analysis Verbose) "%a@." (Sil.pp_instr Pp.text) instr)
+        (fun _ instr ->
+          Logging.(debug Analysis Verbose) "%a@." (Sil.pp_instr ~print_types:false Pp.text) instr
+          )
         specialized_pdesc ;
       Logging.(debug Analysis Verbose) "End of instructions@." ;
       match Ondemand.analyze_proc_desc ~caller_pdesc specialized_pdesc with
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 72d7c362c..5739a8c83 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -143,7 +143,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
    fun instr pre post ->
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
-    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr ;
+    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ;
     L.(debug BufferOverrun Verbose) "@\n@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Post-state : @,%a" Dom.Mem.pp post ;
     L.(debug BufferOverrun Verbose) "@]@\n" ;
@@ -661,7 +661,7 @@ module Report = struct
    fun instr pre cond_set ->
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
-    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr ;
+    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ;
     L.(debug BufferOverrun Verbose) "@[<v 2>@\n@\n%a" PO.ConditionSet.pp cond_set ;
     L.(debug BufferOverrun Verbose) "@]@\n" ;
     L.(debug BufferOverrun Verbose) "================================@\n@."
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index 33a5fd1cb..92d36b0cf 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -89,8 +89,9 @@ module TransferFunctionsNodesBasicCost = struct
           astate
     in
     L.(debug Analysis Medium)
-      "@\n>>>Instr: %a   Cost: %a@\n" (Sil.pp_instr Pp.text) instr
-      CostDomain.NodeInstructionToCostMap.pp astate' ;
+      "@\n>>>Instr: %a   Cost: %a@\n"
+      (Sil.pp_instr ~print_types:false Pp.text)
+      instr CostDomain.NodeInstructionToCostMap.pp astate' ;
     astate'
 
 
@@ -690,8 +691,9 @@ module TransferFunctionsWCET = struct
           assert false
     in
     L.(debug Analysis Medium)
-      "@\n[>>>AnalyzerWCET] Instr: %a   Cost: %a@\n" (Sil.pp_instr Pp.text) instr BasicCost.pp
-      cost_node ;
+      "@\n[>>>AnalyzerWCET] Instr: %a   Cost: %a@\n"
+      (Sil.pp_instr ~print_types:false Pp.text)
+      instr BasicCost.pp cost_node ;
     let astate' =
       let und_node = CFG.Node.underlying_node node in
       let preds = Procdesc.Node.get_preds und_node in
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index cfc6b170f..7316fccf3 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -28,7 +28,7 @@ module StructuredSil = struct
 
   let rec pp_structured_instr fmt = function
     | Cmd instr ->
-        Sil.pp_instr Pp.text fmt instr
+        Sil.pp_instr ~print_types:false Pp.text fmt instr
     | If (exp, then_instrs, else_instrs) ->
         (* TODO (t10287763): indent bodies of if/while *)
         F.fprintf fmt "if (%a) {@.%a@.} else {@.%a@.}" Exp.pp exp pp_structured_instr_list