diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml
index db67c81ee..2826d69bf 100644
--- a/infer/src/backend/inferconfig.ml
+++ b/infer/src/backend/inferconfig.ml
@@ -154,7 +154,7 @@ module FileOrProcMatcher = struct
     in
     let pp_method_pattern fmt mp =
       let pp_params fmt l =
-        Format.fprintf fmt "[%a]" (Pp.semicolon_seq_oneline Pp.text pp_string) l
+        Format.fprintf fmt "[%a]" (Pp.semicolon_seq ~print_env:Pp.text pp_string) l
       in
       Format.fprintf fmt "%a%a%a" (pp_key_value pp_string) ("class", Some mp.class_name)
         (pp_key_value pp_string) ("method", mp.method_name) (pp_key_value pp_params)
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 4c2c95875..34d13ffce 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -104,11 +104,13 @@ let pp_footprint _pe f fp =
   let pe = {_pe with Pp.cmap_norm= _pe.Pp.cmap_foot} in
   let pp_pi f () =
     if fp.pi_fp <> [] then
-      F.fprintf f "%a ;@\n" (Pp.semicolon_seq_oneline pe (Sil.pp_atom pe)) fp.pi_fp
+      F.fprintf f "%a ;@\n"
+        (Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe))
+        fp.pi_fp
   in
   if fp.pi_fp <> [] || fp.sigma_fp <> [] then
     F.fprintf f "@\n[footprint@\n  @[%a%a@]  ]" pp_pi ()
-      (Pp.semicolon_seq pe (Sil.pp_hpred pe))
+      (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred pe))
       fp.sigma_fp
 
 let pp_texp_simple pe =
@@ -141,7 +143,7 @@ let pp_hpred_stackvar pe0 f (hpred: Sil.hpred) =
 let pp_sub pe f = function
   | `Exp sub
    -> let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
-      Pp.semicolon_seq_oneline pe (Sil.pp_atom pe) f pi_sub
+      Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe) f pi_sub
   | `Typ _
    -> F.fprintf f "Printing typ_subst not implemented."
 
@@ -160,19 +162,19 @@ let pp_sub_entry pe0 f entry =
 
 (** Pretty print a substitution as a list of (ident,exp) pairs *)
 let pp_subl pe =
-  if Config.smt_output then Pp.semicolon_seq pe (pp_sub_entry pe)
-  else Pp.semicolon_seq_oneline pe (pp_sub_entry pe)
+  if Config.smt_output then Pp.semicolon_seq ~print_env:pe (pp_sub_entry pe)
+  else Pp.semicolon_seq ~print_env:{pe with break_lines= false} (pp_sub_entry pe)
 
 (** Pretty print a pi. *)
 let pp_pi pe =
-  if Config.smt_output then Pp.semicolon_seq pe (Sil.pp_atom pe)
-  else Pp.semicolon_seq_oneline pe (Sil.pp_atom pe)
+  if Config.smt_output then Pp.semicolon_seq ~print_env:pe (Sil.pp_atom pe)
+  else Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe)
 
 (** Dump a pi. *)
 let d_pi (pi: pi) = L.add_print_action (PTpi, Obj.repr pi)
 
 (** Pretty print a sigma. *)
-let pp_sigma pe = Pp.semicolon_seq pe (Sil.pp_hpred pe)
+let pp_sigma pe = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred pe)
 
 (** Split sigma into stack and nonstack parts.
     The boolean indicates whether the stack should only include local variales. *)
@@ -190,7 +192,8 @@ let pp_sigma_simple pe env fmt sigma =
   let sigma_stack, sigma_nonstack = sigma_get_stack_nonstack false sigma in
   let pp_stack fmt _sg =
     let sg = List.sort ~cmp:Sil.compare_hpred _sg in
-    if sg <> [] then Format.fprintf fmt "%a" (Pp.semicolon_seq pe (pp_hpred_stackvar pe)) sg
+    if sg <> [] then
+      Format.fprintf fmt "%a" (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) sg
   in
   let pp_nl fmt doit =
     if doit then
@@ -200,7 +203,7 @@ let pp_sigma_simple pe env fmt sigma =
       | LATEX
        -> Format.fprintf fmt " ; \\\\@\n"
   in
-  let pp_nonstack fmt = Pp.semicolon_seq pe (Sil.pp_hpred_env pe (Some env)) fmt in
+  let pp_nonstack fmt = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)) fmt in
   if sigma_stack <> [] || sigma_nonstack <> [] then
     Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl
       (sigma_stack <> [] && sigma_nonstack <> [])
@@ -259,11 +262,11 @@ let pp_hpara_simple _pe env n f pred =
   match pe.kind with
   | TEXT | HTML
    -> F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars
-        (Pp.semicolon_seq pe (Sil.pp_hpred_env pe (Some env)))
+        (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
         pred.Sil.body
   | LATEX
    -> F.fprintf f "P_{%d} = %a%a\\\\" n (pp_evars pe) pred.Sil.evars
-        (Pp.semicolon_seq pe (Sil.pp_hpred_env pe (Some env)))
+        (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
         pred.Sil.body
 
 (** Print an hpara_dll in simple mode *)
@@ -273,11 +276,11 @@ let pp_hpara_dll_simple _pe env n f pred =
   match pe.kind with
   | TEXT | HTML
    -> F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars_dll
-        (Pp.semicolon_seq pe (Sil.pp_hpred_env pe (Some env)))
+        (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
         pred.Sil.body_dll
   | LATEX
    -> F.fprintf f "P_{%d} = %a%a" n (pp_evars pe) pred.Sil.evars_dll
-        (Pp.semicolon_seq pe (Sil.pp_hpred_env pe (Some env)))
+        (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
         pred.Sil.body_dll
 
 (** Create an environment mapping (ident) expressions to the program variables containing them *)
@@ -1654,13 +1657,13 @@ module Normalize = struct
       else
         let p'' =
           match a' with
-            | Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e)
-             -> let mysub = Sil.subst_of_list [(i, e)] in
-                let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
-                let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in
-                footprint_normalize tenv (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp')
-            | _
-             -> footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp))
+          | Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e)
+           -> let mysub = Sil.subst_of_list [(i, e)] in
+              let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
+              let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in
+              footprint_normalize tenv (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp')
+          | _
+           -> footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp))
         in
         unsafe_cast_to_normal p''
 
diff --git a/infer/src/base/Pp.ml b/infer/src/base/Pp.ml
index f5d7293a7..834d6f136 100644
--- a/infer/src/base/Pp.ml
+++ b/infer/src/base/Pp.ml
@@ -32,6 +32,7 @@ type colormap = Obj.t -> color
 type env =
   { opt: simple_kind  (** Current option for simple printing *)
   ; kind: print_kind  (** Current kind of printing *)
+  ; break_lines: bool  (** whether to let Format add its own line breaks or not *)
   ; cmap_norm: colormap  (** Current colormap for the normal part *)
   ; cmap_foot: colormap  (** Current colormap for the footprint part *)
   ; color: color  (** Current color *)
@@ -50,6 +51,7 @@ let colormap_red (_: Obj.t) = Red
 let text =
   { opt= SIM_DEFAULT
   ; kind= TEXT
+  ; break_lines= false
   ; cmap_norm= colormap_black
   ; cmap_foot= colormap_black
   ; color= Black
@@ -64,6 +66,7 @@ let html color =
 let latex color =
   { opt= SIM_DEFAULT
   ; kind= LATEX
+  ; break_lines= false
   ; cmap_norm= colormap_from_color color
   ; cmap_foot= colormap_from_color color
   ; color
@@ -99,59 +102,26 @@ let color_string = function
   | Red
    -> "color_red"
 
-(** Pretty print a space-separated sequence *)
-let rec seq pp f = function
-  | []
-   -> ()
-  | [x]
-   -> F.fprintf f "%a" pp x
-  | x :: l
-   -> F.fprintf f "%a %a" pp x (seq pp) l
-
-(** Print a comma-separated sequence *)
-let rec comma_seq pp f = function
-  | []
-   -> ()
-  | [x]
-   -> F.fprintf f "%a" pp x
-  | x :: l
-   -> F.fprintf f "%a,%a" pp x (comma_seq pp) l
-
-(** Print a ;-separated sequence. *)
-let rec _semicolon_seq oneline pe pp f =
-  let sep fmt () = if oneline then F.fprintf fmt " " else F.fprintf fmt "@\n" in
-  function
+let seq ?(print_env= text) ?sep:(sep_text = " ") ?(sep_html= sep_text) ?(sep_latex= sep_text) pp =
+  let rec aux f = function
     | []
      -> ()
     | [x]
      -> F.fprintf f "%a" pp x
-    | x :: l ->
-      match pe.kind with
-      | TEXT | HTML
-       -> F.fprintf f "%a ; %a%a" pp x sep () (_semicolon_seq oneline pe pp) l
-      | LATEX
-       -> F.fprintf f "%a ;\\\\%a %a" pp x sep () (_semicolon_seq oneline pe pp) l
-
-(** Print a ;-separated sequence with newlines. *)
-let semicolon_seq pe = _semicolon_seq false pe
-
-(** Print a ;-separated sequence on one line. *)
-let semicolon_seq_oneline pe = _semicolon_seq true pe
-
-(** Print an or-separated sequence. *)
-let or_seq pe pp f = function
-  | []
-   -> ()
-  | [x]
-   -> F.fprintf f "%a" pp x
-  | x :: l ->
-    match pe.kind with
-    | TEXT
-     -> F.fprintf f "%a || %a" pp x (semicolon_seq pe pp) l
-    | HTML
-     -> F.fprintf f "%a &or; %a" pp x (semicolon_seq pe pp) l
-    | LATEX
-     -> F.fprintf f "%a \\vee %a" pp x (semicolon_seq pe pp) l
+    | x :: l
+     -> let sep =
+          match print_env.kind with TEXT -> sep_text | HTML -> sep_html | LATEX -> sep_latex
+        in
+        if print_env.break_lines then F.fprintf f "%a%s@ %a" pp x sep aux l
+        else F.fprintf f "%a%s%a" pp x sep aux l
+  in
+  aux
+
+let comma_seq ?print_env pp f l = seq ?print_env ~sep:"," pp f l
+
+let semicolon_seq ?print_env pp f l = seq ?print_env ~sep:";" pp f l
+
+let or_seq ?print_env pp f = seq ?print_env ~sep:" ||" ~sep_html:" &or;" ~sep_latex:" \\vee" pp f
 
 (** Print the current time and date in a format similar to the "date" command *)
 let current_time f () =
@@ -162,4 +132,6 @@ let current_time f () =
 (** Print the time in seconds elapsed since the beginning of the execution of the current command. *)
 let elapsed_time fmt () =
   let elapsed = Unix.gettimeofday () -. Utils.initial_timeofday in
-  Format.fprintf fmt "%f" elapsed
+  F.fprintf fmt "%f" elapsed
+
+let to_string ~f fmt x = F.fprintf fmt "%s" (f x)
diff --git a/infer/src/base/Pp.mli b/infer/src/base/Pp.mli
index 095a441d1..a2c115b6d 100644
--- a/infer/src/base/Pp.mli
+++ b/infer/src/base/Pp.mli
@@ -9,6 +9,7 @@
  *)
 
 open! IStd
+module F = Format
 
 (** Pretty Printing} *)
 
@@ -32,6 +33,8 @@ val equal_print_kind : print_kind -> print_kind -> bool
 type env =
   { opt: simple_kind  (** Current option for simple printing *)
   ; kind: print_kind  (** Current kind of printing *)
+  ; break_lines: bool
+        (** whether to let Format add its own line breaks or not (false by default) *)
   ; cmap_norm: colormap  (** Current colormap for the normal part *)
   ; cmap_foot: colormap  (** Current colormap for the footprint part *)
   ; color: color  (** Current color *)
@@ -65,24 +68,26 @@ val latex : color -> env
 val color_string : color -> string
 (** string representation of colors *)
 
-val seq : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-(** Pretty print a space-separated sequence *)
+val seq :
+  ?print_env:env -> ?sep:string -> ?sep_html:string -> ?sep_latex:string
+  -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
+(** Pretty print a sequence with [sep] followed by a space between each element. By default,
+    [print_env] is [text], [sep] is "", and [sep_html] and [sep_latex] set to [sep]. *)
 
-val comma_seq : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-(** Pretty print a comma-separated sequence *)
+val comma_seq : ?print_env:env -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
+(** Pretty print a comma-separated sequence. *)
 
-val semicolon_seq : env -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+val semicolon_seq : ?print_env:env -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
 (** Pretty print a ;-separated sequence *)
 
-val semicolon_seq_oneline :
-  env -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-(** Pretty print a ;-separated sequence on one line *)
-
-val or_seq : env -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+val or_seq : ?print_env:env -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
 (** Pretty print a or-separated sequence *)
 
-val current_time : Format.formatter -> unit -> unit
+val to_string : f:('a -> string) -> F.formatter -> 'a -> unit
+(** turn a "to_string" function into a "pp_foo" *)
+
+val current_time : F.formatter -> unit -> unit
 (** Print the current time and date in a format similar to the "date" command *)
 
-val elapsed_time : Format.formatter -> unit -> unit
+val elapsed_time : F.formatter -> unit -> unit
 (** Print the time in seconds elapsed since the beginning of the execution of the current command. *)