diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 64c61a8d93..a30e4de345 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -32,7 +32,7 @@ struct
     emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
 
   let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
-    if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;
+    if M.tracing then M.trace "access" "do_access %a %a %B" CilType.Exp.pp e AccessKind.pp kind reach;
     let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
     let ad = man.ask reach_or_mpt in
     man.emit (Access {exp=e; ad; kind; reach})
@@ -42,7 +42,7 @@ struct
       + [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses.
       + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
   let access_one_top ?(force=false) ?(deref=false) man (kind: AccessKind.t) reach exp =
-    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
+    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pp exp AccessKind.pp kind reach deref;
     if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) then (
       if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
         do_access man kind reach exp;
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 5d66659b43..789304f0ae 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -89,7 +89,7 @@ struct
     let e' = visitCilExpr visitor e in
     let rel = RD.add_vars st.rel (List.map RV.local (VH.to_seq_values v_ins |> List.of_seq)) in (* add temporary g#in-s *)
     let rel' = VH.fold (fun v v_in rel ->
-        if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in;
+        if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pp v CilType.Varinfo.pp v_in;
         read_global ask getg {st with rel} v v_in (* g#in = g; *)
       ) v_ins rel
     in
@@ -124,7 +124,7 @@ struct
 
   let assign_from_globals_wrapper ask getg st e f =
     let (rel', e', v_ins) = read_globals_to_locals ask getg st e in
-    if M.tracing then M.trace "relation" "assign_from_globals_wrapper %a" d_exp e';
+    if M.tracing then M.trace "relation" "assign_from_globals_wrapper %a" CilType.Exp.pp e';
     let rel' = f rel' e' in (* x = e; *)
     let rel'' = RD.remove_vars rel' (List.map RV.local (VH.to_seq_values v_ins |> List.of_seq)) in (* remove temporary g#in-s *)
     rel''
@@ -155,7 +155,7 @@ struct
         v_out.vattr <- v.vattr; (*copy the attributes because the tracking may depend on them. Otherwise an assertion fails *)
         let st = {st with rel = RD.add_vars st.rel [RV.local v_out]} in (* add temporary g#out *)
         let st' = {st with rel = f st v_out} in (* g#out = e; *)
-        if M.tracing then M.trace "relation" "write_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_out;
+        if M.tracing then M.trace "relation" "write_global %a %a" CilType.Varinfo.pp v CilType.Varinfo.pp v_out;
         let st' = write_global ask getg sideg st' v v_out in (* g = g#out; *)
         let rel'' = RD.remove_vars st'.rel [RV.local v_out] in (* remove temporary g#out *)
         {st' with rel = rel''}
@@ -192,7 +192,7 @@ struct
 
   let no_overflow man exp = lazy (
     let res = no_overflow man exp in
-    if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res d_exp exp;
+    if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res CilType.Exp.pp exp;
     res
   )
 
@@ -249,20 +249,20 @@ struct
   let assign man (lv:lval) e =
     let st = man.local in
     let simplified_e = replace_deref_exps man.ask e in
-    if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv  d_exp e d_exp simplified_e;
+    if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" CilType.Lval.pp lv  CilType.Exp.pp e CilType.Exp.pp simplified_e;
     let ask = Analyses.ask_of_man man in
     let r = assign_to_global_wrapper ask man.global man.sideg st lv (fun st v ->
         assign_from_globals_wrapper ask man.global st simplified_e (fun apr' e' ->
-            if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
-            if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
+            if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pp v CilType.Exp.pp e' CilType.Exp.pp e';
+            if M.tracing then M.trace "relation" "st: %a" RD.pp apr';
             let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
             let r' = assert_type_bounds ask r v in
-            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r';
+            if M.tracing then M.traceu "relation" "-> %a" RD.pp r';
             r'
           )
       )
     in
-    if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
+    if M.tracing then M.traceu "relation" "-> %a" D.pp r;
     r
 
   let branch man e b =
@@ -331,7 +331,7 @@ struct
         | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
-    if M.tracing then M.tracel "combine" "relation enter newd: %a" RD.pretty new_rel;
+    if M.tracing then M.tracel "combine" "relation enter newd: %a" RD.pp new_rel;
     new_rel
 
   let enter man r f args =
@@ -386,11 +386,11 @@ struct
     let st = man.local in
     let reachable_from_args = reachable_from_args man args in
     let fundec = Node.find_fundec man.node in
-    if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pretty f.svar;
-    if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals;
-    if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," d_exp) args;
-    if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pretty st;
-    if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pretty fun_st;
+    if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pp f.svar;
+    if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pp) f.sformals;
+    if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," CilType.Exp.pp) args;
+    if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pp st;
+    if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pp fun_st;
     let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in
     let arg_substitutes =
       let filter_actuals (x,e) =
@@ -416,7 +416,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pretty ())) arg_vars;
+    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pp ())) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
@@ -430,7 +430,7 @@ struct
       )
     in
     let unify_rel = RD.unify new_rel new_fun_rel in (* TODO: unify_with *)
-    if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel;
+    if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pp new_rel RD.pp new_fun_rel RD.pp unify_rel;
     {fun_st with rel = unify_rel}
 
   let combine_assign man r fe f args fc fun_st (f_ask : Queries.ask) =
@@ -640,10 +640,10 @@ struct
     in
     match q with
     | EvalInt e ->
-      if M.tracing then M.traceli "evalint" "relation query %a (%a)" d_exp e d_plainexp e;
-      if M.tracing then M.trace "evalint" "relation st: %a" D.pretty man.local;
+      if M.tracing then M.traceli "evalint" "relation query %a (%a)" CilType.Exp.pp e CilType.Exp.pp e;
+      if M.tracing then M.trace "evalint" "relation st: %a" D.pp man.local;
       let r = eval_int e (no_overflow (Analyses.ask_of_man man) e) in
-      if M.tracing then M.traceu "evalint" "relation query %a -> %a" d_exp e ID.pretty r;
+      if M.tracing then M.traceu "evalint" "relation query %a -> %a" CilType.Exp.pp e ID.pp r;
       r
     | Queries.IterSysVars (vq, vf) ->
       let vf' x = vf (Obj.repr x) in
@@ -720,9 +720,9 @@ struct
           in
           match q with
           | EvalInt e ->
-            if M.tracing then M.traceli "relation" "evalint query %a (%a), man %a" d_exp e d_plainexp e D.pretty man.local;
+            if M.tracing then M.traceli "relation" "evalint query %a (%a), man %a" CilType.Exp.pp e CilType.Exp.pp e D.pp man.local;
             let r = eval_int e (no_overflow (dummyask) e) in
-            if M.tracing then M.trace "relation" "evalint response %a -> %a" d_exp e ValueDomainQueries.ID.pretty r;
+            if M.tracing then M.trace "relation" "evalint response %a -> %a" CilType.Exp.pp e ValueDomainQueries.ID.pp r;
             r
           |_ -> Queries.Result.top q
         in
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index cba9084ad7..1b18a7c599 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -893,20 +893,20 @@ struct
 
   let lock_get_m oct local_m get_m =
     let joined = LRD.join local_m get_m in
-    if M.tracing then M.traceli "relationpriv" "lock_get_m:\n  get=%a\n  joined=%a" LRD.pretty get_m LRD.pretty joined;
+    if M.tracing then M.traceli "relationpriv" "lock_get_m:\n  get=%a\n  joined=%a" LRD.pp get_m LRD.pp joined;
     let r = LRD.fold (fun _ -> RD.meet) joined (RD.top ()) in
-    if M.tracing then M.trace "relationpriv" "meet=%a" RD.pretty r;
+    if M.tracing then M.trace "relationpriv" "meet=%a" RD.pp r;
     let r = RD.meet oct r in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r;
     r
 
   let lock oct local_m get_m =
-    if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD.pretty local_m;
+    if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD.pp local_m;
     let r = lock_get_m oct local_m get_m in
     (* is_bot check commented out because it's unnecessarily expensive *)
     (* if RD.is_bot_env r then
        failwith "DownwardClosedCluster.lock: not downward closed?"; *)
-    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r;
     r
 
   let unlock w oct_side =
@@ -989,7 +989,7 @@ struct
     (lad, lad_weak)
 
   let lock oct (local_m, _) (get_m, get_m') =
-    if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD1.pretty local_m;
+    if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD1.pp local_m;
     let r =
       let locked = DCCluster.lock_get_m oct local_m get_m in
       if RD.is_bot_env locked then (
@@ -1002,7 +1002,7 @@ struct
       else
         locked
     in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r;
     r
 
   let unlock w oct_side =
@@ -1044,15 +1044,15 @@ struct
 
   let get_m_with_mutex_inits inits ask getg m =
     let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
-    if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m;
+    if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.MustLock.pp m LRD.pp get_m;
     let r =
       let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
       let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
       let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in
-      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
+      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pp get_mutex_inits LRD.pp get_mutex_inits';
       LRD.join get_m get_mutex_inits'
     in
-    if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pp r;
     r
 
   let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var
@@ -1067,15 +1067,15 @@ struct
       else
         get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g)
     in
-    if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
+    if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a" CilType.Varinfo.pp g LRD.pp get_mutex_global_g;
     let r =
       let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
       let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
       let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in
-      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
+      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pp get_mutex_inits LRD.pp get_mutex_inits';
       LRD.join get_mutex_global_g get_mutex_inits'
     in
-    if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pp r;
     r
 
   let get_mutex_global_g_with_mutex_inits_atomic inits ask getg =
@@ -1349,147 +1349,147 @@ struct
   module RelComponents = RelationDomain.RelComponents (RD) (D)
 
   let read_global ask getg st g x =
-    if M.tracing then M.traceli "relationpriv" "read_global %a %a" CilType.Varinfo.pretty g CilType.Varinfo.pretty x;
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.traceli "relationpriv" "read_global %a %a" CilType.Varinfo.pp g CilType.Varinfo.pp x;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let r = Priv.read_global ask getg st g x in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r;
     r
 
   let write_global ?invariant ask getg sideg st g x =
-    if M.tracing then M.traceli "relationpriv" "write_global %a %a" CilType.Varinfo.pretty g CilType.Varinfo.pretty x;
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.traceli "relationpriv" "write_global %a %a" CilType.Varinfo.pp g CilType.Varinfo.pp x;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = write_global ?invariant ask getg sideg st g x in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let lock ask getg st m =
-    if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pretty m;
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pp m;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let r = lock ask getg st m in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let unlock ask getg sideg st m =
-    if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pretty m;
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pp m;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = unlock ask getg sideg st m in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let enter_multithreaded ask getg sideg st =
     if M.tracing then M.traceli "relationpriv" "enter_multithreaded";
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = enter_multithreaded ask getg sideg st in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let threadenter ask getg st =
     if M.tracing then M.traceli "relationpriv" "threadenter";
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let r = threadenter ask getg st in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let sync ask getg sideg st reason =
     if M.tracing then M.traceli "relationpriv" "sync";
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = sync ask getg sideg st reason in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let escape node ask getg sideg st vs =
     if M.tracing then M.traceli "relationpriv" "escape";
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = escape node ask getg sideg st vs in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let thread_join ?force ask getg e st =
     if M.tracing then M.traceli "relationpriv" "thread_join";
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let r = thread_join ?force ask getg e st in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 
   let thread_return ask getg sideg tid st =
     if M.tracing then M.traceli "relationpriv" "thread_return";
-    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
+    if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = thread_return ask getg sideg tid st in
-    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r;
+    if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r;
     r
 end
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 3cde51b49b..132c7eabe9 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -293,7 +293,7 @@ struct
 
   (* Evaluate binop for two abstract values: *)
   let evalbinop_base ~man (op: binop) (t1:typ) (a1:value) (t2:typ) (a2:value) (t:typ) :value =
-    if M.tracing then M.tracel "eval" "evalbinop %a %a %a" d_binop op VD.pretty a1 VD.pretty a2;
+    if M.tracing then M.tracel "eval" "evalbinop %a %a %a" d_binop op VD.pp a1 VD.pp a2;
     (* We define a conversion function for the easy cases when we can just use
      * the integer domain operations. *)
     let bool_top ik = ID.(join (of_int ik Z.zero) (of_int ik Z.one)) in
@@ -417,7 +417,7 @@ struct
             let ay = AD.choose y in
             let handle_address_is_multiple addr = begin match Addr.to_var addr with
               | Some v when man.ask (Q.IsMultiple v) ->
-                if M.tracing then M.tracel "addr" "IsMultiple %a" CilType.Varinfo.pretty v;
+                if M.tracing then M.tracel "addr" "IsMultiple %a" CilType.Varinfo.pp v;
                 None
               | _ ->
                 Some true
@@ -425,7 +425,7 @@ struct
             in
             match Addr.semantic_equal ax ay with
             | Some true ->
-              if M.tracing then M.tracel "addr" "semantic_equal %a %a" AD.pretty x AD.pretty y;
+              if M.tracing then M.tracel "addr" "semantic_equal %a %a" AD.pp x AD.pp y;
               handle_address_is_multiple ax
             | Some false -> Some false
             | None -> None
@@ -527,7 +527,7 @@ struct
     (* get hold of the variable value, either from local or global state *)
     let var = get_var ~man st x in
     let v = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in
-    if M.tracing then M.tracec "get" "var = %a, %a = %a" VD.pretty var AD.pretty (AD.of_mval (x, offs)) VD.pretty v;
+    if M.tracing then M.tracec "get" "var = %a, %a = %a" VD.pp var AD.pp (AD.of_mval (x, offs)) VD.pp v;
     if full then var else match v with
       | Blob (c,s,_) -> c
       | x -> x
@@ -549,7 +549,7 @@ struct
    *  For the exp argument it is always ok to put None. This means not using precise information about
    *  which part of an array is involved.  *)
   and get ~man ?top ?full (st: store) (addrs:address) (exp:exp option) : value =
-    if M.tracing then M.traceli "get" "Address: %a\nState: %a" AD.pretty addrs CPA.pretty st.cpa;
+    if M.tracing then M.traceli "get" "Address: %a\nState: %a" AD.pp addrs CPA.pp st.cpa;
     (* Finding a single varinfo*offset pair *)
     let res =
       (* We form the collecting function by joining *)
@@ -565,7 +565,7 @@ struct
       let f x a = VD.join (c @@ get_addr ~man ?top ?full st x exp) a in      (* Finally we join over all the addresses in the set. *)
       AD.fold f addrs (VD.bot ())
     in
-    if M.tracing then M.traceu "get" "Result: %a" VD.pretty res;
+    if M.tracing then M.traceu "get" "Result: %a" VD.pp res;
     res
 
 
@@ -590,7 +590,7 @@ struct
 
   let rec reachable_from_value ask (value: value) (t: typ) (description: string)  =
     let empty = AD.empty () in
-    if M.tracing then M.trace "reachability" "Checking value %a" VD.pretty value;
+    if M.tracing then M.trace "reachability" "Checking value %a" VD.pp value;
     match value with
     | Top ->
       if not (VD.is_immediate_type t) then M.info ~category:Unsound "Unknown value in %s could be an escaped pointer address!" description; empty
@@ -617,9 +617,9 @@ struct
    * all pointers within a structure should be considered, but we don't follow
    * pointers. We return a flattend representation, thus simply an address (set). *)
   let reachable_from_addr ~man st (addr: Addr.t): address =
-    if M.tracing then M.tracei "reachability" "Checking for %a" Addr.pretty addr;
+    if M.tracing then M.tracei "reachability" "Checking for %a" Addr.pp addr;
     let res = reachable_from_value (Analyses.ask_of_man man) (get_addr ~man st addr None) (Addr.type_of addr) (Addr.show addr) in
-    if M.tracing then M.traceu "reachability" "Reachable addresses: %a" AD.pretty res;
+    if M.tracing then M.traceu "reachability" "Reachable addresses: %a" AD.pp res;
     res
 
   (* The code for getting the variables reachable from the list of parameters.
@@ -627,7 +627,7 @@ struct
    * addresses, as both AD elements abstracting individual (ambiguous) addresses
    * and the workset of visited addresses. *)
   let reachable_vars ~man (st: store) (args: address): address =
-    if M.tracing then M.traceli "reachability" "Checking reachable arguments from %a!" AD.pretty args;
+    if M.tracing then M.traceli "reachability" "Checking reachable arguments from %a!" AD.pp args;
     let empty = AD.empty () in
     (* We begin looking at the parameters: *)
     let workset = ref args in
@@ -643,7 +643,7 @@ struct
       workset := AD.diff collected !visited
     done;
     (* Return the list of elements that have been visited. *)
-    if M.tracing then M.traceu "reachability" "All reachable vars: %a" AD.pretty !visited;
+    if M.tracing then M.traceu "reachability" "All reachable vars: %a" AD.pp !visited;
     !visited
 
   let reachable_vars ~man st args = Timing.wrap "reachability" (reachable_vars ~man st) args
@@ -757,7 +757,7 @@ struct
 
   (* The evaluation function as mutually recursive eval_lv & eval_rv *)
   let rec eval_rv ~(man: _ man) (st: store) (exp:exp): value =
-    if M.tracing then M.traceli "evalint" "base eval_rv %a" d_exp exp;
+    if M.tracing then M.traceli "evalint" "base eval_rv %a" CilType.Exp.pp exp;
     let r =
       (* we have a special expression that should evaluate to top ... *)
       if exp = MyCFG.unknown_exp then
@@ -765,7 +765,7 @@ struct
       else
         eval_rv_ask_evalint ~man st exp
     in
-    if M.tracing then M.traceu "evalint" "base eval_rv %a -> %a" d_exp exp VD.pretty r;
+    if M.tracing then M.traceu "evalint" "base eval_rv %a -> %a" CilType.Exp.pp exp VD.pp r;
     r
 
   (** Evaluate expression using EvalInt query.
@@ -774,13 +774,13 @@ struct
       Non-integer expression just delegate to next eval_rv function. *)
   and eval_rv_ask_evalint ~man st exp =
     let eval_next () = eval_rv_no_ask_evalint ~man st exp in
-    if M.tracing then M.traceli "evalint" "base eval_rv_ask_evalint %a" d_exp exp;
+    if M.tracing then M.traceli "evalint" "base eval_rv_ask_evalint %a" CilType.Exp.pp exp;
     let r:value =
       match Cilfacade.typeOf exp with
       | typ when Cil.isIntegralType typ && not (Cil.isConstant exp) -> (* don't EvalInt integer constants, base can do them precisely itself *)
-        if M.tracing then M.traceli "evalint" "base ask EvalInt %a" d_exp exp;
+        if M.tracing then M.traceli "evalint" "base ask EvalInt %a" CilType.Exp.pp exp;
         let a = man.ask (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *)
-        if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a" d_exp exp Queries.ID.pretty a;
+        if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a" CilType.Exp.pp exp Queries.ID.pp a;
         begin match a with
           | `Bot -> eval_next () (* Base EvalInt returns bot on incorrect type (e.g. pthread_t); ignore and continue. *)
           (* | x -> Some (Int x) *)
@@ -790,7 +790,7 @@ struct
       | exception Cilfacade.TypeOfError _ (* Bug: typeOffset: Field on a non-compound *)
       | _ -> eval_next ()
     in
-    if M.tracing then M.traceu "evalint" "base eval_rv_ask_evalint %a -> %a" d_exp exp VD.pretty r;
+    if M.tracing then M.traceu "evalint" "base eval_rv_ask_evalint %a -> %a" CilType.Exp.pp exp VD.pp r;
     r
 
   (** Evaluate expression without EvalInt query on outermost expression.
@@ -815,13 +815,13 @@ struct
       Subexpressions delegate to [eval_rv], which may use queries on them. *)
   and eval_rv_base ~man (st: store) (exp:exp): value =
     let eval_rv = eval_rv_back_up in
-    if M.tracing then M.traceli "evalint" "base eval_rv_base %a" d_exp exp;
+    if M.tracing then M.traceli "evalint" "base eval_rv_base %a" CilType.Exp.pp exp;
     let binop_remove_same_casts ~extra_is_safe ~e1 ~e2 ~t1 ~t2 ~c1 ~c2 =
       let te1 = Cilfacade.typeOf e1 in
       let te2 = Cilfacade.typeOf e2 in
       let both_arith_type = isArithmeticType te1 && isArithmeticType te2 in
       let is_safe = (extra_is_safe || VD.is_statically_safe_cast t1 te1 && VD.is_statically_safe_cast t2 te2) && not both_arith_type in
-      if M.tracing then M.tracel "cast" "remove cast on both sides for %a? -> %b" d_exp exp is_safe;
+      if M.tracing then M.tracel "cast" "remove cast on both sides for %a? -> %b" CilType.Exp.pp exp is_safe;
       if is_safe then ( (* we can ignore the casts if the casts can't change the value *)
         let e1 = if isArithmeticType te1 then c1 else e1 in
         let e2 = if isArithmeticType te2 then c2 else e2 in
@@ -969,7 +969,7 @@ struct
       | AddrOfLabel _ ->
         VD.top ()
     in
-    if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a" d_exp exp VD.pretty r;
+    if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a" CilType.Exp.pp exp VD.pp r;
     r
 
   and eval_rv_base_lval ~eval_lv ~man (st: store) (exp: exp) (lv: lval): value =
@@ -995,7 +995,7 @@ struct
         | Addr (x, o) ->
           begin
             let at = Addr.Mval.type_of (x, o) in
-            if M.tracing then M.tracel "evalint" "cast_ok %a %a %a" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at;
+            if M.tracing then M.tracel "evalint" "cast_ok %a %a %a" Addr.pp (Addr (x, o)) CilType.Typ.pp (Cil.unrollType x.vtype) CilType.Typ.pp at;
             if at = TVoid [] then (* HACK: cast from alloc variable is always fine *)
               true
             else
@@ -1023,7 +1023,7 @@ struct
             VD.top () (* upcasts not! *)
         in
         let v' = VD.cast ~kind:Internal t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) (* TODO: proper castkind *)
-        if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!" VD.pretty v d_type t VD.pretty v';
+        if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!" VD.pp v CilType.Typ.pp t VD.pp v';
         let v' = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x (Some exp)) v' (convert_offset ~man st ofs) (Some exp) None t in (* handle offset *)
         v'
       in
@@ -1047,7 +1047,7 @@ struct
         (* Fallback to MustBeEqual query, could get extra precision from exprelation/var_eq. *)
         let must_be_equal () =
           let r = Q.must_be_equal (Analyses.ask_of_man man) e1 e2 in
-          if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b" d_exp e1 d_exp e2 r;
+          if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b" CilType.Exp.pp e1 CilType.Exp.pp e2 r;
           r
         in
         match op with
@@ -1156,13 +1156,13 @@ struct
   let eval_rv ~man (st: store) (exp:exp): value =
     try
       let r = eval_rv ~man st exp in
-      if M.tracing then M.tracel "eval" "eval_rv %a = %a" d_exp exp VD.pretty r;
+      if M.tracing then M.tracel "eval" "eval_rv %a = %a" CilType.Exp.pp exp VD.pp r;
       if VD.is_bot r then VD.top_value (Cilfacade.typeOf exp) else r
     with IntDomain.ArithmeticOnIntegerBot _ ->
       ValueDomain.Compound.top_value (Cilfacade.typeOf exp)
 
   let query_evalint ~man st e =
-    if M.tracing then M.traceli "evalint" "base query_evalint %a" d_exp e;
+    if M.tracing then M.traceli "evalint" "base query_evalint %a" CilType.Exp.pp e;
     let r = match eval_rv_no_ask_evalint ~man st e with
       | Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *)
       | Bot   -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *)
@@ -1170,7 +1170,7 @@ struct
       | v      -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot ()
       | exception (IntDomain.ArithmeticOnIntegerBot _)  when not !AnalysisState.should_warn -> Queries.ID.bot ()
     in
-    if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a" d_exp e Queries.ID.pretty r;
+    if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a" CilType.Exp.pp e Queries.ID.pp r;
     r
 
   (* Evaluate an expression containing only locals. This is needed for smart joining the partitioned arrays where man is not accessible. *)
@@ -1451,7 +1451,7 @@ struct
         | AddrOf lval
         | StartOf lval -> lval_may_signed_overflow man lval
     in
-    if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp exp res; res
+    if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" CilType.Exp.pp exp res; res
   and lval_may_signed_overflow man (lval : lval) =
     let (host, offset) = lval in
     let host_may_signed_overflow = function
@@ -1636,7 +1636,7 @@ struct
       let g: V.t = Obj.obj g in
       query_invariant_global man g
     | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow man e in
-                                if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp e res; res
+                                if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" CilType.Exp.pp e res; res
                                )
     | _ -> Q.Result.top q
 
@@ -1666,9 +1666,9 @@ struct
     | _ ->  st
 
   let update_variable x t y z =
-    if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pretty y CPA.pretty z;
+    if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pp y CPA.pp z;
     let r = update_variable x t y z in (* refers to definition above *)
-    if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pretty y CPA.pretty z CPA.pretty r;
+    if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pp y CPA.pp z CPA.pp r;
     r
 
   (* Updating a single varinfo*offset pair. NB! This function's type does
@@ -1708,9 +1708,9 @@ struct
       else
         new_value
     in
-    if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pretty (AD.of_mval (x,offs)) d_type x.vtype D.pretty st;
+    if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pp (AD.of_mval (x,offs)) CilType.Typ.pp x.vtype D.pp st;
     if isFunctionType x.vtype then begin
-      if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " d_type x.vtype;
+      if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " CilType.Typ.pp x.vtype;
       st
     end else
     if get_bool "exp.globs_are_top" then begin
@@ -1731,9 +1731,9 @@ struct
           Priv.read_global ask priv_getg st x
       in
       let new_value = update_offset old_value in
-      if M.tracing then M.tracel "set" "update_offset %a -> %a" VD.pretty old_value VD.pretty new_value;
+      if M.tracing then M.tracel "set" "update_offset %a -> %a" VD.pp old_value VD.pp new_value;
       let r = Priv.write_global ~invariant ask priv_getg (priv_sideg man.sideg) st x new_value in
-      if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a" x.vname D.pretty r;
+      if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a" x.vname D.pp r;
       r
     end else begin
       if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: update a local var '%s' ..." x.vname;
@@ -1823,18 +1823,18 @@ struct
    * precise information about arrays. *)
   let set ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
     let lval_raw = (Option.map (fun x -> Lval x) lval_raw) in
-    if M.tracing then M.tracel "set" "lval: %a\nvalue: %a\nstate: %a" AD.pretty lval VD.pretty value CPA.pretty st.cpa;
+    if M.tracing then M.tracel "set" "lval: %a\nvalue: %a\nstate: %a" AD.pp lval VD.pp value CPA.pp st.cpa;
     let update_one x store =
       set_addr ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override store x lval_type value
     in try
       (* We start from the current state and an empty list of global deltas,
        * and we assign to all the different possible places: *)
       let nst = AD.fold update_one lval st in
-      (* if M.tracing then M.tracel "set" "new state1 %a" CPA.pretty nst; *)
+      (* if M.tracing then M.tracel "set" "new state1 %a" CPA.pp nst; *)
       (* If the address was definite, then we just return it. If the address
        * was ambiguous, we have to join it with the initial state. *)
       let nst = if AD.cardinal lval > 1 then D.join st nst else nst in
-      (* if M.tracing then M.tracel "set" "new state2 %a" CPA.pretty nst; *)
+      (* if M.tracing then M.tracel "set" "new state2 %a" CPA.pp nst; *)
       nst
     with
     (* If any of the addresses are unknown, we ignore it!?! *)
@@ -1917,7 +1917,7 @@ struct
 
 
   let set_savetop ~man ?lval_raw ?rval_raw st adr lval_t v : store =
-    if M.tracing then M.tracel "set" "savetop %a %a %a" AD.pretty adr d_type lval_t VD.pretty v;
+    if M.tracing then M.tracel "set" "savetop %a %a %a" AD.pp adr CilType.Typ.pp lval_t VD.pp v;
     match v with
     | Top -> set ~man st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw
     | v -> set ~man st adr lval_t v ?lval_raw ?rval_raw
@@ -2001,7 +2001,7 @@ struct
             | [(x,offs)] ->
               let t = v.vtype in
               let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *)
-              if M.tracing then M.tracel "set" "init bot value (%a): %a" d_plaintype t VD.pretty iv;
+              if M.tracing then M.tracel "set" "init bot value (%a): %a" d_plaintype t VD.pp iv;
               let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) iv offs rval_val (Some  (Lval lval)) lval t in (* do desired update to value *)
               set_savetop ~man  man.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *)
             | _ ->
@@ -2018,8 +2018,8 @@ struct
     let valu = eval_rv ~man man.local exp in
     let refine () =
       let res = invariant man man.local exp tv in
-      if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a" d_exp exp Queries.ES.pretty (man.ask (Queries.EqualSet exp));
-      if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a" d_exp exp Queries.ES.pretty (man.ask (Queries.CondVars exp));
+      if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a" CilType.Exp.pp exp Queries.ES.pp (man.ask (Queries.EqualSet exp));
+      if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a" CilType.Exp.pp exp Queries.ES.pp (man.ask (Queries.CondVars exp));
       if M.tracing then M.traceu "branch" "Invariant enforced!";
       match man.ask (Queries.CondVars exp) with
       | s when Queries.ES.cardinal s = 1 ->
@@ -2027,12 +2027,12 @@ struct
         invariant man res e tv
       | _ -> res
     in
-    if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a" d_exp exp VD.pretty valu;
+    if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a" CilType.Exp.pp exp VD.pp valu;
     (* First we want to see, if we can determine a dead branch: *)
     match valu with
     (* For a boolean value: *)
     | Int value ->
-      if M.tracing then M.traceu "branch" "Expression %a evaluated to %a" d_exp exp ID.pretty value;
+      if M.tracing then M.traceu "branch" "Expression %a evaluated to %a" CilType.Exp.pp exp ID.pp value;
       Option.map_default_delayed (fun v ->
           (* Eliminate the dead branch and just propagate to the true branch *)
           if v = tv then
@@ -2069,7 +2069,7 @@ struct
     let st: store = man.local in
     match fundec.svar.vname with
     | "__goblint_dummy_init" ->
-      if M.tracing then M.trace "init" "dummy init: %a" D.pretty st;
+      if M.tracing then M.trace "init" "dummy init: %a" D.pp st;
       publish_all man `Init;
       (* otherfun uses __goblint_dummy_init, where we can properly side effect global initialization *)
       (* TODO: move into sync `Init *)
@@ -2128,7 +2128,7 @@ struct
     )
 
   let invalidate ~(must: bool) ?(deep=true) ~man (st:store) (exps: exp list): store =
-    if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " d_plainexp) exps;
+    if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " CilType.Exp.pp) exps;
     if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps;
     (* To invalidate a single address, we create a pair with its corresponding
      * top value. *)
@@ -2150,7 +2150,7 @@ struct
     if M.tracing && exps <> [] then (
       let addrs = List.map (Tuple3.first) invalids' in
       let vs = List.map (Tuple3.third) invalids' in
-      M.tracel "invalidate" "Setting addresses [%a] to values [%a]" (d_list ", " Addr.pretty) addrs (d_list ", " VD.pretty) vs
+      M.tracel "invalidate" "Setting addresses [%a] to values [%a]" (d_list ", " Addr.pp) addrs (d_list ", " VD.pp) vs
     );
     (* copied from set_many *)
     let f (acc: store) ((lval:Addr.t),(typ:Cil.typ),(value:value)): store =
@@ -2389,7 +2389,7 @@ struct
       (addr, AD.type_of addr)
     in
     let forks = forkfun man lv f args in
-    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks);
+    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a" f.vname (d_list "," CilType.Varinfo.pp) (List.map BatTuple.Tuple4.second forks);
     List.iter (fun (lval, f, args, multiple) -> man.spawn ~multiple lval f args) forks;
     let st: store = man.local in
     let desc = LF.find f in
@@ -2817,7 +2817,7 @@ struct
         | Address jmp_buf ->
           let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (man.prev_node, man.control_context ())), false) in
           let r = set ~man st jmp_buf (Cilfacade.typeOf env) value in
-          if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a" d_exp env D.pretty st D.pretty r;
+          if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a" CilType.Exp.pp env D.pp st D.pp r;
           r
         | _ -> failwith "problem?!"
       in
@@ -2870,7 +2870,7 @@ struct
         | Addr.Addr ((v,o) as mval) when CPA.mem v fun_st.cpa ->
           begin
             let lval_type = Addr.type_of addr in
-            if M.tracing then M.trace "taintPC" "updating %a; type: %a" Addr.Mval.pretty (v,o) d_type lval_type;
+            if M.tracing then M.trace "taintPC" "updating %a; type: %a" Addr.Mval.pp (v,o) CilType.Typ.pp lval_type;
             match CPA.find_opt v (fun_st.cpa) with
             | None -> st
             (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
@@ -2880,7 +2880,7 @@ struct
             | _ ->
               let address = AD.singleton addr in
               let new_val = get_mval ~man fun_st mval None in
-              if M.tracing then M.trace "taintPC" "update val: %a" VD.pretty new_val;
+              if M.tracing then M.trace "taintPC" "update val: %a" VD.pp new_val;
               let st' = set_savetop ~man st address lval_type new_val in
               (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
               Option.map_default (fun deps ->
@@ -2896,7 +2896,7 @@ struct
 
   let combine_env man lval fexp f args fc au (f_ask: Queries.ask) =
     let combine_one (st: D.t) (fun_st: D.t) =
-      if M.tracing then M.tracel "combine" "%a\n%a" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
+      if M.tracing then M.tracel "combine" "%a\n%a" CPA.pp st.cpa CPA.pp fun_st.cpa;
       (* This function does miscellaneous things, but the main task was to give the
        * handle to the global state to the state return from the function, but now
        * the function tries to add all the context variables back to the callee.
@@ -2907,29 +2907,29 @@ struct
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
         let ask = Analyses.ask_of_man man in
         let tainted = f_ask.f Q.MayBeTainted in
-        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a" f.svar.vname AD.pretty tainted;
-        if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
+        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a" f.svar.vname AD.pp tainted;
+        if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a" CPA.pp st.cpa CPA.pp fun_st.cpa;
         if AD.is_top tainted then
           let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
           let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
-          if M.tracing then M.trace "taintPC" "combined: %a" CPA.pretty cpa';
+          if M.tracing then M.trace "taintPC" "combined: %a" CPA.pp cpa';
           { fun_st with cpa = cpa' }
         else
           (* remove variables from caller cpa, that are global and not in the callee cpa *)
           let cpa_caller = CPA.filter (fun x _ -> (not (is_global ask x)) || CPA.mem x fun_st.cpa) st.cpa in
-          if M.tracing then M.trace "taintPC" "cpa_caller: %a" CPA.pretty cpa_caller;
+          if M.tracing then M.trace "taintPC" "cpa_caller: %a" CPA.pp cpa_caller;
           (* add variables from callee that are not in caller yet *)
           let cpa_new = CPA.filter (fun x _ -> not (CPA.mem x cpa_caller)) cpa_noreturn in
-          if M.tracing then M.trace "taintPC" "cpa_new: %a" CPA.pretty cpa_new;
+          if M.tracing then M.trace "taintPC" "cpa_new: %a" CPA.pp cpa_new;
           let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
-          if M.tracing then M.trace "taintPC" "cpa_caller': %a" CPA.pretty cpa_caller';
+          if M.tracing then M.trace "taintPC" "cpa_caller': %a" CPA.pp cpa_caller';
           (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
           let tainted = AD.filter (function
               | Addr.Addr (v,_) -> not (CPA.mem v cpa_new)
               | _ -> false
             ) tainted in
           let st_combined = combine_st man {st with cpa = cpa_caller'} fun_st tainted in
-          if M.tracing then M.trace "taintPC" "combined: %a" CPA.pretty st_combined.cpa;
+          if M.tracing then M.trace "taintPC" "combined: %a" CPA.pp st_combined.cpa;
           { fun_st with cpa = st_combined.cpa }
       in
       let nst = add_globals st fun_st in
@@ -3130,7 +3130,7 @@ struct
     let st: store = man.local in
     match e with
     | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pretty addr;
+      if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pp addr;
       CommonPriv.lift_lock ask (fun st m ->
           Priv.lock ask (priv_getg man.global) st m
         ) st addr
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 1386df31aa..f751fddcd8 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -56,7 +56,7 @@ struct
     with Lattice.Uncomparable -> old_val
 
   let refine_lv_fallback man st lval value tv =
-    if M.tracing then M.tracec "invariant" "Restricting %a with %a" d_lval lval VD.pretty value;
+    if M.tracing then M.tracec "invariant" "Restricting %a with %a" CilType.Lval.pp lval VD.pp value;
     let addr = eval_lv ~man st lval in
     if (AD.is_top addr) then st
     else
@@ -65,7 +65,7 @@ struct
       let old_val = map_oldval old_val t_lval in
       let old_val =
         if is_some_bot old_val then (
-          if M.tracing then M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" d_lval lval;
+          if M.tracing then M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" CilType.Lval.pp lval;
           VD.top ()
         )
         else
@@ -74,7 +74,7 @@ struct
       let state_with_excluded = set st addr t_lval value ~man in
       let value =  get ~man state_with_excluded addr None in
       let new_val = apply_invariant ~old_val ~new_val:value in
-      if M.tracing then M.traceu "invariant" "New value is %a" VD.pretty new_val;
+      if M.tracing then M.traceu "invariant" "New value is %a" VD.pp new_val;
       (* make that address meet the invariant, i.e exclusion sets will be joined *)
       if is_some_bot new_val then (
         if M.tracing then M.tracel "branch" "C The branch %B is dead!" tv;
@@ -93,7 +93,7 @@ struct
       let v = apply_invariant ~old_val ~new_val:c' in
       if is_some_bot v then contra st
       else (
-        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
+        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" CilType.Lval.pp x VD.pp old_val VD.pp v pretty c VD.pp c';
         set' x v st
       )
     in
@@ -107,9 +107,9 @@ struct
       let v = apply_invariant ~old_val ~new_val in
       if is_some_bot v then contra st
       else (
-        if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)" CilType.Varinfo.pretty var VD.pretty old_val VD.pretty v pretty c VD.pretty c';
+        if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)" CilType.Varinfo.pp var VD.pp old_val VD.pp v pretty c VD.pp c';
         let r = set' (Cil.var var) v st in
-        if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r;
+        if M.tracing then M.tracel "inv" "st from %a to %a" D.pp st D.pp r;
         r
       )
     | Mem (Lval lv), off when GobConfig.get_bool "ana.base.branch.refine-pointer-by-pointee" ->
@@ -122,7 +122,7 @@ struct
               match base_a with
               | Addr base_mval ->
                 let (lval_a:VD.t) = Address (AD.singleton base_a) in
-                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a;
+                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" CilType.Lval.pp lv VD.pp lval_a;
                 let st = set' lv lval_a st in
                 let orig = PreValueDomain.Addr.Mval.add_offset base_mval original_offset in
                 let old_val = get_mval ~man st orig None in
@@ -134,7 +134,7 @@ struct
                 if is_some_bot v then
                   Some (D.join acc (try contra st with Analyses.Deadcode -> D.bot ()))
                 else (
-                  if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
+                  if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" CilType.Lval.pp x VD.pp old_val VD.pp v pretty c VD.pp c';
                   Some (D.join acc (set' x v st))
                 )
               | _ -> None
@@ -154,7 +154,7 @@ struct
       match (op, lval, value, tv) with
       (* The true-branch where x == value: *)
       | Eq, x, value, true ->
-        if M.tracing then M.tracec "invariant" "Yes, %a equals %a" d_lval x VD.pretty value;
+        if M.tracing then M.tracec "invariant" "Yes, %a equals %a" CilType.Lval.pp x VD.pp value;
         (match value with
          | Int n ->
            let ikind = Cilfacade.get_ikind_exp (Lval lval) in
@@ -167,20 +167,20 @@ struct
               match ID.to_int n with
               | Some n ->
                 (* When x != n, we can return a singleton exclusion set *)
-                if M.tracing then M.tracec "invariant" "Yes, %a is not %a" d_lval x GobZ.pretty n;
+                if M.tracing then M.tracec "invariant" "Yes, %a is not %a" CilType.Lval.pp x GobZ.pp n;
                 let ikind = Cilfacade.get_ikind_exp (Lval lval) in
                 `Refine (x, Int (ID.of_excl_list ikind [n]))
               | None -> `NotUnderstood
             end
           | Address n -> begin
-              if M.tracing then M.tracec "invariant" "Yes, %a is not %a" d_lval x AD.pretty n;
+              if M.tracing then M.tracec "invariant" "Yes, %a is not %a" CilType.Lval.pp x AD.pp n;
               match eval_rv_address ~man st (Lval x) with
               | Address a when AD.is_definite n ->
                 `Refine (x, Address (AD.diff a n))
               | Top when AD.is_null n ->
                 `Refine (x, Address AD.not_null)
               | v ->
-                if M.tracing then M.tracec "invariant" "No address invariant for: %a != %a" VD.pretty v AD.pretty n;
+                if M.tracing then M.tracec "invariant" "No address invariant for: %a != %a" VD.pp v AD.pp n;
                 `NotUnderstood
             end
           (* | Address a -> `Refine (x, value) *)
@@ -200,7 +200,7 @@ struct
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
-                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" d_lval x GobZ.pretty n;
+                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" CilType.Lval.pp x GobZ.pp n;
                 `Refine (x, Int (range_from n))
               | None -> `NotUnderstood
             end
@@ -215,7 +215,7 @@ struct
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
-                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" d_lval x GobZ.pretty n;
+                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" CilType.Lval.pp x GobZ.pp n;
                 `Refine (x, Int (range_from n))
               | None -> `NotUnderstood
             end
@@ -227,7 +227,7 @@ struct
         if M.tracing then M.trace "invariant" "Failed! (operation not supported)";
         `NotUnderstood
     in
-    if M.tracing then M.traceli "invariant" "assume expression %a is %B" d_exp exp tv;
+    if M.tracing then M.traceli "invariant" "assume expression %a is %B" CilType.Exp.pp exp tv;
     let null_val (typ:typ):VD.t =
       match Cil.unrollType typ with
       | TPtr _                    -> Address AD.null_ptr
@@ -269,7 +269,7 @@ struct
         helper Ne x (null_val (Cilfacade.typeOf exp)) tv
       | UnOp (LNot,uexp,typ) -> derived_invariant uexp (not tv)
       | _ ->
-        if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)" d_plainexp exp;
+        if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)" CilType.Exp.pp exp;
         `NotUnderstood
     in
     match derived_invariant exp tv with
@@ -285,7 +285,7 @@ struct
 
   let invariant man st exp tv: D.t =
     let fallback reason st =
-      if M.tracing then M.tracel "inv" "Can't handle %a.\n%t" d_plainexp exp reason;
+      if M.tracing then M.tracel "inv" "Can't handle %a.\n%t" CilType.Exp.pp exp reason;
       invariant_fallback man st exp tv
     in
     (* inverse values for binary operation a `op` b == c *)
@@ -415,7 +415,7 @@ struct
             in
             let a' = excl b a in
             let b' = excl a b in
-            if M.tracing then M.tracel "inv" "inv_bin_int: unequal: %a and %a; ikind: %a; a': %a, b': %a" ID.pretty a ID.pretty b d_ikind ikind ID.pretty a' ID.pretty b';
+            if M.tracing then M.tracel "inv" "inv_bin_int: unequal: %a and %a; ikind: %a; a': %a, b': %a" ID.pp a ID.pp b d_ikind ikind ID.pp a' ID.pp b';
             meet_bin a' b'
           | _, _ -> a, b
         end
@@ -578,7 +578,7 @@ struct
                 else
                   b
               | _ -> b) in
-          if M.tracing then M.trace "inv_float" "Div: (%a,%a) = %a   yields (%a,%a)" FD.pretty a FD.pretty b FD.pretty c FD.pretty a' FD.pretty b';
+          if M.tracing then M.trace "inv_float" "Div: (%a,%a) = %a   yields (%a,%a)" FD.pp a FD.pp b FD.pp c FD.pp a' FD.pp b';
           meet_bin a' b'
         | Eq | Ne as op ->
           let both x = x, x in
@@ -737,20 +737,20 @@ struct
         | (BinOp (op, e1, e2, _) as e, Float _)
         | (BinOp (op, e1, e2, _) as e, Int _) ->
           let invert_binary_op c pretty c_int c_float =
-            if M.tracing then M.tracel "inv" "binop %a with %a %a %a == %a" d_exp e VD.pretty (eval e1 st) d_binop op VD.pretty (eval e2 st) pretty c;
+            if M.tracing then M.tracel "inv" "binop %a with %a %a %a == %a" CilType.Exp.pp e VD.pp (eval e1 st) d_binop op VD.pp (eval e2 st) pretty c;
             (match eval e1 st, eval e2 st with
              | Int a, Int b ->
                let ikind = Cilfacade.get_ikind_exp e1 in (* both operands have the same type (except for Shiftlt, Shiftrt)! *)
                let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *)
                let a', b' = inv_bin_int (a, b) ikind (c_int ikres) op in
-               if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" d_exp e ID.pretty (c_int ikind) ID.pretty a' ID.pretty b';
+               if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" CilType.Exp.pp e ID.pp (c_int ikind) ID.pp a' ID.pp b';
                let st' = inv_exp (Int a') e1 st in
                let st'' = inv_exp (Int b') e2 st' in
                st''
              | Float a, Float b ->
                let fkind = Cilfacade.get_fkind_exp e1 in (* both operands have the same type *)
                let a', b' = inv_bin_float (a, b) (c_float fkind) op in
-               if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" d_exp e FD.pretty (c_float fkind) FD.pretty a' FD.pretty b';
+               if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" CilType.Exp.pp e FD.pp (c_float fkind) FD.pp a' FD.pp b';
                let st' = inv_exp (Float a') e1 st in
                let st'' = inv_exp (Float b') e2 st' in
                st''
@@ -766,7 +766,7 @@ struct
         | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *)
           let update_lval c x c' pretty = refine_lv man st c x c' pretty exp in
           let t = Cil.unrollType (Cilfacade.typeOfLval x) in  (* unroll type to deal with TNamed *)
-          if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a" d_lval x VD.pretty c_typed d_type t;
+          if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a" CilType.Lval.pp x VD.pp c_typed CilType.Typ.pp t;
           begin match c_typed with
             | Int c ->
               let c' = match t with
@@ -781,7 +781,7 @@ struct
               begin match x, t with
                 | (Var v, offs), TInt (ik, _) ->
                   let tmpSpecial = man.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in
-                  if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pretty tmpSpecial;
+                  if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pp tmpSpecial;
                   begin match tmpSpecial with
                     | `Lifted (Abs (ik, xInt)) ->
                       let c' = ID.cast_to ~kind:Internal ik c in (* different ik! *) (* TODO: proper castkind *)
@@ -816,7 +816,7 @@ struct
               begin match x, t with
                 | (Var v, offs), TFloat (fk, _) ->
                   let tmpSpecial = man.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in
-                  if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pretty tmpSpecial;
+                  if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pp tmpSpecial;
                   begin match tmpSpecial with
                     | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
                     | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
@@ -859,7 +859,7 @@ struct
                       (* Suppressing overflow warnings as this is not a computation that comes from the program *)
                       let res_range = (ID.cast_to ~suppress_ovwarn:true ~kind:Internal ik (ID.top_of ik_e)) in (* TODO: proper castkind *)
                       let c' = ID.cast_to ~kind:Internal ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *) (* TODO: proper castkind *)
-                      if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
+                      if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" CilType.Exp.pp e d_ikind ik_e d_ikind ik ID.pp i ID.pp c d_ikind ik_e ID.pp c';
                       inv_exp (Int c') e st
                     else
                       fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 20826195db..86b4f05def 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -216,7 +216,7 @@ struct
     let get_mutex_inits = getg V.mutex_inits in
     let is_in_Gm x _ = is_protected_by ask m x in
     let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in
-    if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n  get_m: %a\n  get_mutex_inits: %a\n  get_mutex_inits': %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits';
+    if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n  get_m: %a\n  get_mutex_inits: %a\n  get_mutex_inits': %a" LockDomain.MustLock.pp m CPA.pp get_m CPA.pp get_mutex_inits CPA.pp get_mutex_inits';
     CPA.join get_m get_mutex_inits'
 
   (** [get_m_with_mutex_inits] optimized for implementation-specialized [read_global]. *)
@@ -240,7 +240,7 @@ struct
 
     let cpa' = CPA.fold (fun x v acc ->
         if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then (
-          if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+          if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
           sideg (V.global x) (CPA.singleton x v);
           CPA.remove x acc
         )
@@ -256,8 +256,8 @@ struct
 
     let cpa' = CPA.fold (fun x v acc ->
         if is_global ask x (* && is_unprotected ask x *) then (
-          if M.tracing then M.tracel "priv" "enter_multithreaded remove %a" CilType.Varinfo.pretty x;
-          if M.tracing then M.tracel "priv" "ENTER MULTITHREADED SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+          if M.tracing then M.tracel "priv" "enter_multithreaded remove %a" CilType.Varinfo.pp x;
+          if M.tracing then M.tracel "priv" "ENTER MULTITHREADED SIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
           sideg (V.global x) (CPA.singleton x v);
           CPA.remove x acc
         )
@@ -317,7 +317,7 @@ struct
          No other privatization uses is_unprotected, so this hack is only needed here. *)
       let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
       let cpa' = CPA.filter is_in_V get_m in
-      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pretty m CPA.pretty cpa';
+      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pp m CPA.pp cpa';
       {st with cpa = CPA.fold CPA.add cpa' st.cpa}
     )
     else
@@ -326,7 +326,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     let side_m_cpa = CPA.filter is_in_Gm st.cpa in
-    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pretty m CPA.pretty side_m_cpa;
+    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pp m CPA.pp side_m_cpa;
     sideg (V.mutex m) side_m_cpa;
     st
 
@@ -413,7 +413,7 @@ struct
       CPA.find x st.cpa
   let read_global ask getg st x =
     let v = read_global ask getg st x in
-    if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pretty x (is_unprotected ask x) CPA.pretty st.cpa VD.pretty v;
+    if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pp x (is_unprotected ask x) CPA.pp st.cpa VD.pp v;
     v
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let cpa' =
@@ -423,7 +423,7 @@ struct
         CPA.add x v st.cpa
     in
     if not invariant then (
-      if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+      if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
       let side_cpa = CPA.singleton x v in
       sideg (V.global x) side_cpa;
       if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then
@@ -444,7 +444,7 @@ struct
       let get_m = CPA.filter is_in_Gm get_m in
       let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
       let meet = long_meet st.cpa get_m in
-      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet;
+      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.MustLock.pp m CPA.pp get_m CPA.pp meet;
       {st with cpa = meet}
     )
     else
@@ -471,12 +471,12 @@ struct
 
       let cpa' = CPA.fold (fun x v cpa ->
           if is_global ask x && is_unprotected ask x (* && not (VD.is_top v) *) then (
-            if M.tracing then M.tracel "priv" "SYNC SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+            if M.tracing then M.tracel "priv" "SYNC SIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
             sideg (V.global x) (CPA.singleton x v);
             CPA.remove x cpa
           )
           else (
-            if M.tracing then M.tracel "priv" "SYNC NOSIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+            if M.tracing then M.tracel "priv" "SYNC NOSIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
             cpa
           )
         ) st.cpa st.cpa
@@ -563,7 +563,7 @@ struct
 
   let read_global ask getg st x =
     let v = read_global ask getg st x in
-    if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pretty x (is_unprotected ~protection:Weak ask x) CPA.pretty st.cpa VD.pretty v;
+    if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pp x (is_unprotected ~protection:Weak ask x) CPA.pp st.cpa VD.pp v;
     v
 
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
@@ -575,7 +575,7 @@ struct
       else
         CPA.add x v st.cpa
     in
-    if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+    if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
     let digest = Digest.current ask in
     let sidev = GMutex.singleton digest (CPA.singleton x v) in
     let l' = L.add lm (CPA.singleton x v) l in
@@ -675,7 +675,7 @@ struct
     sideg V.mutex_inits (G.create_mutex sidev);
     let cpa' = CPA.fold (fun x v acc ->
         if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then (
-          if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
+          if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pp x VD.pp v;
           let sidev = GMutex.singleton digest (CPA.singleton x v) in
           sideg (V.global x) (G.create_global sidev);
           CPA.remove x acc
@@ -1533,10 +1533,10 @@ struct
       else
         GWeak.find lockset_init weaks
     in
-    if M.tracing then M.trace "priv" "d_cpa: %a" VD.pretty d_cpa;
-    if M.tracing then M.trace "priv" "d_sync: %a" VD.pretty d_sync;
-    if M.tracing then M.trace "priv" "d_weak: %a" VD.pretty d_weak;
-    if M.tracing then M.trace "priv" "d_init: %a" VD.pretty d_init;
+    if M.tracing then M.trace "priv" "d_cpa: %a" VD.pp d_cpa;
+    if M.tracing then M.trace "priv" "d_sync: %a" VD.pp d_sync;
+    if M.tracing then M.trace "priv" "d_weak: %a" VD.pp d_weak;
+    if M.tracing then M.trace "priv" "d_init: %a" VD.pp d_init;
     let d_weak = VD.join d_weak d_init in
     let d = VD.join d_cpa (VD.join d_sync d_weak) in
     d
@@ -1708,9 +1708,9 @@ struct
           acc
       ) weaks (VD.bot ())
     in
-    if M.tracing then M.trace "priv" "d_cpa: %a" VD.pretty d_cpa;
-    if M.tracing then M.trace "priv" "d_sync: %a" VD.pretty d_sync;
-    if M.tracing then M.trace "priv" "d_weak: %a" VD.pretty d_weak;
+    if M.tracing then M.trace "priv" "d_cpa: %a" VD.pp d_cpa;
+    if M.tracing then M.trace "priv" "d_sync: %a" VD.pp d_sync;
+    if M.tracing then M.trace "priv" "d_weak: %a" VD.pp d_weak;
     let d = VD.join d_cpa (VD.join d_sync d_weak) in
     d
 
@@ -1742,11 +1742,11 @@ struct
     let s = MustLockset.remove m (current_lockset ask) in
     let (w, p) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
-    if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pretty m CPA.pretty st.cpa;
+    if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pp m CPA.pp st.cpa;
     let side_gsyncw = CPA.fold (fun x v acc ->
         if is_global ask x then (
           let w_x = W.find x w in
-          if M.tracing then M.trace "priv" "gsyncw %a %a %a" CilType.Varinfo.pretty x VD.pretty v MinLocksets.pretty w_x;
+          if M.tracing then M.trace "priv" "gsyncw %a %a %a" CilType.Varinfo.pp x VD.pp v MinLocksets.pp w_x;
           MinLocksets.fold (fun w acc ->
               let v = distr_init getg x v in
               GSyncW.add w (CPA.add x v (GSyncW.find w acc)) acc
@@ -1755,7 +1755,7 @@ struct
           acc
       ) st.cpa (GSyncW.bot ())
     in
-    if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pretty m GSyncW.pretty side_gsyncw;
+    if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pp m GSyncW.pp side_gsyncw;
     sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw));
     {st with priv = (w, p')}
 
@@ -2050,109 +2050,109 @@ struct
   module BaseComponents = BaseComponents (D)
 
   let read_global ask getg st x =
-    if M.tracing then M.traceli "priv" "read_global %a" CilType.Varinfo.pretty x;
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.traceli "priv" "read_global %a" CilType.Varinfo.pp x;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let v = Priv.read_global ask getg st x in
-    if M.tracing then M.traceu "priv" "-> %a" VD.pretty v;
+    if M.tracing then M.traceu "priv" "-> %a" VD.pp v;
     v
 
   let write_global ?invariant ask getg sideg st x v =
-    if M.tracing then M.traceli "priv" "write_global %a %a" CilType.Varinfo.pretty x VD.pretty v;
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.traceli "priv" "write_global %a %a" CilType.Varinfo.pp x VD.pp v;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = write_global ?invariant ask getg sideg st x v in
-    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r;
     r
 
   let lock ask getg st m =
-    if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pretty m;
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pp m;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let r = lock ask getg st m in
-    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r;
     r
 
   let unlock ask getg sideg st m =
-    if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pretty m;
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pp m;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = unlock ask getg sideg st m in
-    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r;
     r
 
   let enter_multithreaded ask getg sideg st =
     if M.tracing then M.traceli "priv" "enter_multithreaded";
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = enter_multithreaded ask getg sideg st in
-    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r;
     r
 
   let threadenter ask st =
     if M.tracing then M.traceli "priv" "threadenter";
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let r = threadenter ask st in
-    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r;
     r
 
   let sync ask getg sideg st reason =
     if M.tracing then M.traceli "priv" "sync";
-    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
+    if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let sideg x v =
-      if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v;
+      if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v;
       sideg x v
     in
     let r = sync ask getg sideg st reason in
-    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r;
     r
 
   let invariant_global ask getg g =
-    if M.tracing then M.traceli "priv" "invariant_global %a" V.pretty g;
+    if M.tracing then M.traceli "priv" "invariant_global %a" V.pp g;
     let getg x =
       let r = getg x in
-      if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r;
+      if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r;
       r
     in
     let r = invariant_global ask getg g in
-    if M.tracing then M.traceu "priv" "-> %a" Invariant.pretty r;
+    if M.tracing then M.traceu "priv" "-> %a" Invariant.pp r;
     r
 
 end
diff --git a/src/analyses/c2poAnalysis.ml b/src/analyses/c2poAnalysis.ml
index b5bff3431a..0a18675206 100644
--- a/src/analyses/c2poAnalysis.ml
+++ b/src/analyses/c2poAnalysis.ml
@@ -61,7 +61,7 @@ struct
     let f a prop =
       try
         let exp = T.prop_to_cil prop in (* May raise UnsupportedCilExpression *)
-        if M.tracing then M.trace "c2po-invariant" "Adding invariant: %a" d_exp exp;
+        if M.tracing then M.trace "c2po-invariant" "Adding invariant: %a" CilType.Exp.pp exp;
         Invariant.(a && of_exp exp)
       with T.UnsupportedCilExpression _ ->
         a
@@ -100,7 +100,7 @@ struct
     | lval_size, (Some rterm, Some roffset) ->
       let dummy_var = MayBeEqual.dummy_var lval_t in
 
-      if M.tracing then M.trace "c2po-assign" "assigning: var: %s; expr: %s + %s. \nTo_cil: lval: %a; expr: %a\n" (T.show lterm) (T.show rterm) (Z.to_string roffset) d_exp (T.to_cil lterm) d_exp (T.to_cil rterm);
+      if M.tracing then M.trace "c2po-assign" "assigning: var: %s; expr: %s + %s. \nTo_cil: lval: %a; expr: %a\n" (T.show lterm) (T.show rterm) (Z.to_string roffset) CilType.Exp.pp (T.to_cil lterm) CilType.Exp.pp (T.to_cil rterm);
 
       let equal_dummy_rterm = [Equal (dummy_var, rterm, roffset)] in
       let equal_dummy_lterm = [Equal (lterm, dummy_var, Z.zero)] in
@@ -126,7 +126,7 @@ struct
          We have to forget all the information we had.
          This should almost never happen.
          Except if the left hand side is a complicated expression like myStruct.field1[i]->field2[z+k], and Goblint can't infer the offset.*)
-      if M.tracing then M.trace "c2po-invalidate" "Invalidate lval: %a" d_lval lval;
+      if M.tracing then M.trace "c2po-invalidate" "Invalidate lval: %a" CilType.Lval.pp lval;
       C2PODomain.top ()
 
   let assign ctx lval expr =
@@ -138,7 +138,7 @@ struct
       let cc = assign_lval d ask lval (T.of_cil ask expr) in
       let cc = reset_normal_form cc in
       let res = `Lifted cc in
-      if M.tracing then M.trace "c2po-assign" "assign: var: %a; expr: %a; result: %s.\n" d_lval lval d_plainexp expr (D.show res);
+      if M.tracing then M.trace "c2po-assign" "assign: var: %a; expr: %a; result: %s.\n" CilType.Lval.pp lval CilType.Exp.pp expr (D.show res);
       res
 
   let branch ctx e pos =
@@ -158,7 +158,7 @@ struct
           with Unsat ->
             `Bot
     in
-    if M.tracing then M.trace "c2po" "branch:\n Actual equality: %a; pos: %b; valid_prop_list: %s; is_bot: %b\n" d_exp e pos (show_conj valid_props) (D.is_bot res);
+    if M.tracing then M.trace "c2po" "branch:\n Actual equality: %a; pos: %b; valid_prop_list: %s; is_bot: %b\n" CilType.Exp.pp e pos (show_conj valid_props) (D.is_bot res);
     if D.is_bot res then raise Deadcode;
     res
 
@@ -188,7 +188,7 @@ struct
         end
       | None -> ctx.local
     in
-    if M.tracing then M.trace "c2po-function" "return: exp_opt: %a; state: %s; result: %s\n" d_exp (BatOption.default (MayBeEqual.dummy_lval_print (TVoid [])) exp_opt) (D.show ctx.local) (D.show res);
+    if M.tracing then M.trace "c2po-function" "return: exp_opt: %a; state: %s; result: %s\n" CilType.Exp.pp (BatOption.default (MayBeEqual.dummy_lval_print (TVoid [])) exp_opt) (D.show ctx.local) (D.show res);
     res
 
   (** var_opt is the variable we assign to. It has type lval. v=malloc.*)
@@ -249,7 +249,7 @@ struct
       if M.tracing then begin
         let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid [])) in
         let lval = BatOption.default dummy_lval var_opt in
-        M.trace "c2po-function" "enter1: var_opt: %a; state: %s; state_with_ghosts: %s\n" d_lval lval (D.show ctx.local) (C2PODomain.show state_with_ghosts);
+        M.trace "c2po-function" "enter1: var_opt: %a; state: %s; state_with_ghosts: %s\n" CilType.Lval.pp lval (D.show ctx.local) (C2PODomain.show state_with_ghosts);
       end;
       (* remove callee vars that are not reachable and not global *)
       let reachable_variables =
@@ -285,7 +285,7 @@ struct
 
       (*remove all variables that were tainted by the function*)
       let tainted = f_ask.f (MayBeTainted) in
-      if M.tracing then M.trace "c2po-tainted" "combine_env1: %a\n" MayBeEqual.AD.pretty tainted;
+      if M.tracing then M.trace "c2po-tainted" "combine_env1: %a\n" MayBeEqual.AD.pp tainted;
 
       let local = D.remove_tainted_terms caller_ask tainted state_with_assignments.data in
       let local = data_to_t local in
@@ -297,7 +297,7 @@ struct
         if M.tracing then begin
           let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid[])) in
           let lval = BatOption.default dummy_lval lval_opt in
-          M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
+          M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" CilType.Lval.pp lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
         end;
         `Lifted d
 
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index b504750a85..f6e4e3e7ac 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -108,7 +108,7 @@ struct
     let save_expr lval expr =
       match mustPointTo man (AddrOf lval) with
       | Some clval ->
-        if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a" Mval.Exp.pretty clval d_exp expr;
+        if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a" Mval.Exp.pp clval CilType.Exp.pp expr;
         D.add clval (D.V.singleton expr) d (* if lval must point to clval, add expr *)
       | None -> d
     in
diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml
index 61fc797585..905614ca81 100644
--- a/src/analyses/creationLockset.ml
+++ b/src/analyses/creationLockset.ml
@@ -140,6 +140,7 @@ module Spec = struct
     (* TID and Lockset components are directly queried from other analyses and already are printed by them *)
     let pretty () (_, _, cl) = G.pretty () cl
     let show (_, _, cl) = G.show cl
+    let pp ppf x = Format.pp_print_string ppf (show x)
     let to_yojson (_, _, cl) = G.to_yojson cl
     let printXml f (_, _, cl) = G.printXml f cl
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index b972195bad..a4a637fa64 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -213,9 +213,9 @@ struct
           let oman' : (S.D.t, S.G.t, S.C.t, S.V.t) man = inner_man "do_emits" ~splits ~post_all oman'' n od in
           n, Obj.repr @@ S.event man' e oman'
         in
-        if M.tracing then M.traceli "event" "%a\n  before: %a" Events.pretty e D.pretty man.local;
+        if M.tracing then M.traceli "event" "%a\n  before: %a" Events.pp e D.pp man.local;
         let d, q = map_deadcode f @@ spec_list2 man.local oman.local in
-        if M.tracing then M.traceu "event" "%a\n  after:%a" Events.pretty e D.pretty d;
+        if M.tracing then M.traceu "event" "%a\n  after:%a" Events.pp e D.pp d;
         do_sideg man !sides;
         do_spawns man !spawns;
         do_splits man d !splits !emits;
@@ -265,7 +265,7 @@ struct
   (* Explicitly polymorphic type required here for recursive GADT call in ask. *)
   and query': type a. querycache:Obj.t Queries.Hashtbl.t -> Queries.Set.t -> (D.t, G.t, C.t, V.t) man -> a Queries.t -> a Queries.result = fun ~querycache asked man q ->
     let anyq = Queries.Any q in
-    if M.tracing then M.traceli "query" "query %a" Queries.Any.pretty anyq;
+    if M.tracing then M.traceli "query" "query %a" Queries.Any.pp anyq;
     let r = match Queries.Hashtbl.find_option querycache anyq with
       | Some r ->
         if M.tracing then M.trace "query" "cached";
@@ -291,7 +291,7 @@ struct
             in
             (* meet results so that precision from all analyses is combined *)
             let res = S.query man' q in
-            if M.tracing then M.trace "queryanswers" "analysis %s query %a -> answer %a" (S.name ()) Queries.Any.pretty anyq Result.pretty res;
+            if M.tracing then M.trace "queryanswers" "analysis %s query %a -> answer %a" (S.name ()) Queries.Any.pp anyq Result.pp res;
             Result.meet a @@ res
           in
           match q with
@@ -337,7 +337,7 @@ struct
     in
     if M.tracing then (
       let module Result = (val Queries.Result.lattice q) in
-      M.traceu "query" "-> %a" Result.pretty r
+      M.traceu "query" "-> %a" Result.pp r
     );
     r
 
diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 05519dbb62..09975b5027 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -169,6 +169,8 @@ struct
     in
     IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) (rev xs)
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let to_yojson xs =
     let f a n (module S : Printable.S) x =
       let name = find_spec_name n in
@@ -246,6 +248,8 @@ struct
       analysis_name ^ ":" ^ S.show (Obj.obj x)
     )
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let to_yojson x =
     `Assoc [
       unop_map (fun n (module S: Printable.S) x ->
diff --git a/src/analyses/startStateAnalysis.ml b/src/analyses/startStateAnalysis.ml
index ac649d59ea..7e8cf62c89 100644
--- a/src/analyses/startStateAnalysis.ml
+++ b/src/analyses/startStateAnalysis.ml
@@ -55,7 +55,7 @@ struct
       let lval = Lval (Var var, NoOffset) in
       let value = get_value (ask_of_man ctx) lval in
       let duplicated_var = to_varinfo (DuplicVar var) in
-      if M.tracing then M.trace "startState" "added value: var: %a; value: %a" CilType.Varinfo.pretty duplicated_var AD.pretty value;
+      if M.tracing then M.trace "startState" "added value: var: %a; value: %a" CilType.Varinfo.pp duplicated_var AD.pp value;
       D.add duplicated_var value st
     in
     (* assign function parameters *)
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 02a0477016..0b33878250 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -63,11 +63,11 @@ struct
       | a when not (Queries.ES.is_bot a) -> Queries.ES.add e a
       | _ -> Queries.ES.singleton e
     in
-    if M.tracing then M.tracel "symb_locks" "get_all_locks exps %a = %a" d_plainexp e Queries.ES.pretty exps;
-    if M.tracing then M.tracel "symb_locks" "get_all_locks st = %a" D.pretty st;
+    if M.tracing then M.tracel "symb_locks" "get_all_locks exps %a = %a" CilType.Exp.pp e Queries.ES.pp exps;
+    if M.tracing then M.tracel "symb_locks" "get_all_locks st = %a" D.pp st;
     let add_locks x xs = PS.union (get_locks x st) xs in
     let r = Queries.ES.fold add_locks exps (PS.empty ()) in
-    if M.tracing then M.tracel "symb_locks" "get_all_locks %a = %a" d_plainexp e PS.pretty r;
+    if M.tracing then M.tracel "symb_locks" "get_all_locks %a = %a" CilType.Exp.pp e PS.pp r;
     r
 
   let same_unknown_index (ask: Queries.ask) exp slocks =
@@ -136,7 +136,7 @@ struct
     *)
     let one_perelem (e,a,l) xs =
       (* ignore (printf "one_perelem (%a,%a,%a)\n" Exp.pretty e Exp.pretty a Exp.pretty l); *)
-      if M.tracing then M.tracel "symb_locks" "one_perelem (%a,%a,%a)" Exp.pretty e Exp.pretty a Exp.pretty l;
+      if M.tracing then M.tracel "symb_locks" "one_perelem (%a,%a,%a)" Exp.pp e Exp.pp a Exp.pp l;
       match Exp.fold_offs (Exp.replace_base (dummyFunDec.svar,`NoOffset) e l) with
       | Some (v, o) ->
         (* ignore (printf "adding lock %s\n" l); *)
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 52f772ac47..07eff6d502 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -36,7 +36,7 @@ struct
             | _ -> false
           ) d
     in
-    if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a" f.svar.vname D.pretty d D.pretty d_return;
+    if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a" f.svar.vname D.pp d D.pp d_return;
     d_return
 
 
@@ -45,7 +45,7 @@ struct
     [man.local, (D.bot ())]
 
   let combine_env man lval fexp f args fc au f_ask =
-    if M.tracing then M.trace "taintPC" "combine for %s in TaintPC: tainted: in function: %a before call: %a" f.svar.vname D.pretty au D.pretty man.local;
+    if M.tracing then M.trace "taintPC" "combine for %s in TaintPC: tainted: in function: %a before call: %a" f.svar.vname D.pp au D.pp man.local;
     D.union man.local au
 
   let combine_assign man (lvalOpt:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 2bf67f4bb9..e39f8bd7ec 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -36,7 +36,7 @@ struct
       Queries.AD.fold to_extra ad (D.empty ())
     (* Ignore soundness warnings, as invalidation proper will raise them. *)
     | ad ->
-      if M.tracing then M.tracel "escape" "reachable %a: %a" d_exp e Queries.AD.pretty ad;
+      if M.tracing then M.tracel "escape" "reachable %a: %a" CilType.Exp.pp e Queries.AD.pp ad;
       D.empty ()
 
   let mpt (ask: Queries.ask) e: D.t =
@@ -50,7 +50,7 @@ struct
       AD.fold to_extra (AD.remove UnknownPtr ad) (D.empty ())
     (* Ignore soundness warnings, as invalidation proper will raise them. *)
     | ad ->
-      if M.tracing then M.tracel "escape" "mpt %a: %a" d_exp e AD.pretty ad;
+      if M.tracing then M.tracel "escape" "mpt %a: %a" CilType.Exp.pp e AD.pp ad;
       D.empty ()
 
   let thread_id man =
@@ -174,7 +174,7 @@ struct
       (* not reusing fman.local to avoid unnecessarily early join of extra *)
       let escaped = reachable (Analyses.ask_of_man man) ptc_arg in
       let escaped = D.filter (fun v -> not v.vglob) escaped in
-      if M.tracing then M.tracel "escape" "%a: %a" d_exp ptc_arg D.pretty escaped;
+      if M.tracing then M.tracel "escape" "%a: %a" CilType.Exp.pp ptc_arg D.pp escaped;
       let thread_id = thread_id man in
       emit_escape_event man escaped;
       side_effect_escape man escaped thread_id;
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index fd2b6f71e3..fe2025d730 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -22,7 +22,7 @@ struct
 
   (* transfer functions *)
   let assign man (lval:lval) (rval:exp) : D.t =
-    if M.tracing then M.tracel "tmpSpecial" "assignment of %a" d_lval lval;
+    if M.tracing then M.tracel "tmpSpecial" "assignment of %a" CilType.Lval.pp lval;
     (* Invalidate all entrys from the map that are possibly written by the assignment *)
     invalidate (Analyses.ask_of_man man) (mkAddrOf lval) man.local
 
@@ -41,7 +41,7 @@ struct
     (* Just dbg prints *)
     (if M.tracing then
        match lval with
-       | Some lv -> if M.tracing then M.tracel "tmpSpecial" "Special: %s with lval %a" f.vname d_lval lv
+       | Some lv -> if M.tracing then M.tracel "tmpSpecial" "Special: %s with lval %a" f.vname CilType.Lval.pp lv
        | _ -> if M.tracing then M.tracel "tmpSpecial" "Special: %s" f.vname);
 
 
@@ -73,7 +73,7 @@ struct
 
     in
 
-    if M.tracing then M.tracel "tmpSpecial" "Result: %a" D.pretty d;
+    if M.tracing then M.tracel "tmpSpecial" "Result: %a" D.pp d;
     d
 
 
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 0c51cbaf60..bbb9f70dea 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -316,7 +316,7 @@ struct
           else (Messages.warn ~category:Analyzer ~msg:("Keep " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r)
           Messages.warn ~category:Analyzer ~msg:(sprint 80 (Exp.pretty () b) ^" changed lvalues: "^sprint 80 (Queries.LS.pretty () bls)) ();
     *)
-    if M.tracing then M.tracel "var_eq" "may_change %a %a = %B" CilType.Exp.pretty b CilType.Exp.pretty a r;
+    if M.tracing then M.tracel "var_eq" "may_change %a %a = %B" CilType.Exp.pp b CilType.Exp.pp a r;
     r
 
   (* Remove elements, that would change if the given lval would change.*)
@@ -372,8 +372,8 @@ struct
     let lvt = unrollType @@ Cilfacade.typeOfLval lv in
     if M.tracing then (
       M.tracel "var_eq" "add_eq is_global_var %a = %B" d_plainlval lv (is_global_var ask (Lval lv) = Some false);
-      M.tracel "var_eq" "add_eq interesting %a = %B" d_plainexp rv (interesting rv);
-      M.tracel "var_eq" "add_eq is_global_var %a = %B" d_plainexp rv (is_global_var ask rv = Some false);
+      M.tracel "var_eq" "add_eq interesting %a = %B" CilType.Exp.pp rv (interesting rv);
+      M.tracel "var_eq" "add_eq is_global_var %a = %B" CilType.Exp.pp rv (is_global_var ask rv = Some false);
       M.tracel "var_eq" "add_eq type %a = %B" d_plainlval lv (isIntegralType lvt || isPointerType lvt);
     );
     if is_global_var ask (Lval lv) = Some false
@@ -493,7 +493,7 @@ struct
 
   let remove_reachable ~deep ask es st =
     let rs = reachables ~deep ask es in
-    if M.tracing then M.tracel "var_eq" "remove_reachable %a: %a" (Pretty.d_list ", " d_exp) es AD.pretty rs;
+    if M.tracing then M.tracel "var_eq" "remove_reachable %a: %a" (Pretty.d_list ", " CilType.Exp.pp) es AD.pp rs;
     (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction":
        each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from.
        It is unknown, why that was necessary. *)
@@ -550,7 +550,7 @@ struct
       D.B.fold add es (Queries.ES.empty ())
 
   let rec eq_set_clos e s =
-    if M.tracing then M.traceli "var_eq" "eq_set_clos %a" d_plainexp e;
+    if M.tracing then M.traceli "var_eq" "eq_set_clos %a" CilType.Exp.pp e;
     let r = match e with
       | AddrOf (Mem (BinOp (IndexPI, a, i, _)), os) ->
         (* convert IndexPI to Index offset *)
@@ -586,7 +586,7 @@ struct
       | CastE (k,t,e) ->
         Queries.ES.map (fun e -> CastE (k,t,e)) (eq_set_clos e s)
     in
-    if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a" d_plainexp e Queries.ES.pretty r;
+    if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a" CilType.Exp.pp e Queries.ES.pp r;
     r
 
 
@@ -596,7 +596,7 @@ struct
       Queries.ID.of_bool (Cilfacade.get_ikind t) true
     | Queries.EqualSet e ->
       let r = eq_set_clos e man.local in
-      if M.tracing then M.tracel "var_eq" "equalset %a = %a" d_plainexp e Queries.ES.pretty r;
+      if M.tracing then M.tracel "var_eq" "equalset %a = %a" CilType.Exp.pp e Queries.ES.pp r;
       r
     | Queries.Invariant context when GobConfig.get_bool "ana.var_eq.invariant.enabled" && GobConfig.get_bool "witness.invariant.exact" -> (* only exact equalities here *)
       let scope = Node.find_fundec man.node in
diff --git a/src/arg/argConstraints.ml b/src/arg/argConstraints.ml
index 8ff2367607..a602c39b7f 100644
--- a/src/arg/argConstraints.ml
+++ b/src/arg/argConstraints.ml
@@ -226,11 +226,11 @@ struct
     | Queries.IterPrevVars f ->
       if M.tracing then M.tracei "witness" "IterPrevVars";
       Dom.iter (fun x r ->
-          if M.tracing then M.tracei "witness" "x = %a" Spec.D.pretty x;
+          if M.tracing then M.tracei "witness" "x = %a" Spec.D.pp x;
           R.iter (function ((n, c, j), e) ->
               if M.tracing then M.tracec "witness" "n = %a" Node.pretty_plain n;
-              if M.tracing then M.tracec "witness" "c = %a" Spec.C.pretty c;
-              if M.tracing then M.tracec "witness" "j = %a" Spec.D.pretty j;
+              if M.tracing then M.tracec "witness" "c = %a" Spec.C.pp c;
+              if M.tracing then M.tracec "witness" "j = %a" Spec.D.pp j;
               f (I.to_int x) (n, Obj.repr c, I.to_int j) e
             ) r;
           if M.tracing then M.traceu "witness" "" (* unindent! *)
diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml
index 1b096a88f3..0bd08653dc 100644
--- a/src/cdomain/value/cdomains/arrayDomain.ml
+++ b/src/cdomain/value/cdomains/arrayDomain.ml
@@ -136,6 +136,7 @@ struct
 
   let show x = "Array: " ^ Val.show x
   let pretty () x = text "Array: " ++ pretty () x
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
   let get ?(checkBounds=true) (ask: VDQ.t) a i = a
   let set (ask: VDQ.t) a (ie, i) v =
@@ -201,6 +202,7 @@ struct
     "Array (unrolled to " ^ (Stdlib.string_of_int (factor ())) ^ "): " ^
     (show_list xl) ^ Val.show xr ^ ")"
   let pretty () x = text "Array: " ++ text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
   let get ?(checkBounds=true)  (ask: VDQ.t) (xl, xr) (_,i) =
     let search_unrolled_values min_i max_i =
@@ -376,6 +378,7 @@ struct
       Val.show xr ^ ")"
 
   let pretty () x = text "Array: " ++ text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
 
   let printXml f = function
@@ -523,7 +526,7 @@ struct
   let move_if_affected ?replace_with_const = move_if_affected_with_length ?replace_with_const None
 
   let set_with_length length (ask:VDQ.t) x (i,_) a =
-    if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
+    if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pp a;
     match i with
     | Some i when Offset.Index.Exp.is_all i ->
       (* TODO: Doesn't seem to work for unassume. *)
@@ -1848,6 +1851,7 @@ struct
   let printXml f x = delegate_if_no_nullbytes x (printXml f) (A.printXml f)
   let to_yojson x = delegate_if_no_nullbytes x to_yojson A.to_yojson
   let pretty () x = delegate_if_no_nullbytes x (pretty ()) (A.pretty ())
+  let pp ppf x = Format.pp_print_string ppf (show x)
 
   let construct a n =
     if get_bool "ana.base.arrays.nullbytes" then
diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml
index 4f117bc8a2..ee76da5699 100644
--- a/src/cdomain/value/cdomains/int/intDomTuple.ml
+++ b/src/cdomain/value/cdomains/int/intDomTuple.ml
@@ -382,6 +382,7 @@ module IntDomTupleImpl = struct
     | _ -> mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) } x
            |> to_list
            |> String.concat "; "
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }
 
   (* `map/opt_map` are used by `project` *)
diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml
index 296cbe5dd5..2b07754d7d 100644
--- a/src/cdomain/value/cdomains/intDomain0.ml
+++ b/src/cdomain/value/cdomains/intDomain0.ml
@@ -201,6 +201,7 @@ struct
       "⊤"
     else
       I.show x.v  (* TODO add ikind to output *)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty () x =
     if not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then
       Pretty.text "⊤"
@@ -306,7 +307,7 @@ module Size = struct (* size in bits as int, range as int64 *)
   let is_cast_injective ~from_type ~to_type =
     let (from_min, from_max) = range (Cilfacade.get_ikind from_type) in
     let (to_min, to_max) = range (Cilfacade.get_ikind to_type) in
-    if M.tracing then M.trace "int" "is_cast_injective %a (%a, %a) -> %a (%a, %a)" CilType.Typ.pretty from_type GobZ.pretty from_min GobZ.pretty from_max CilType.Typ.pretty to_type GobZ.pretty to_min GobZ.pretty to_max;
+    if M.tracing then M.trace "int" "is_cast_injective %a (%a, %a) -> %a (%a, %a)" CilType.Typ.pp from_type GobZ.pp from_min GobZ.pp from_max CilType.Typ.pp to_type GobZ.pp to_min GobZ.pp to_max;
     Z.compare to_min from_min <= 0 && Z.compare from_max to_max <= 0
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
@@ -321,7 +322,7 @@ module Size = struct (* size in bits as int, range as int64 *)
         else if Z.lt y a then Z.add y c
         else y
       in
-      if M.tracing then M.tracel "cast" "Cast %a to range [%a, %a] (%a) = %a (%s in int64)" GobZ.pretty x GobZ.pretty a GobZ.pretty b GobZ.pretty c GobZ.pretty y (if is_int64_big_int y then "fits" else "does not fit");
+      if M.tracing then M.tracel "cast" "Cast %a to range [%a, %a] (%a) = %a (%s in int64)" GobZ.pp x GobZ.pp a GobZ.pp b GobZ.pp c GobZ.pp y (if is_int64_big_int y then "fits" else "does not fit");
       y
 
   (** @return Bit range always includes 0. *)
diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
index 7954a3a6ff..8e1ca0f506 100644
--- a/src/cdomain/value/cdomains/offset.ml
+++ b/src/cdomain/value/cdomains/offset.ml
@@ -248,7 +248,7 @@ struct
   let semantic_equal ~typ1 xoffs ~typ2 yoffs =
     let x_index = to_index ~typ:typ1 xoffs in
     let y_index = to_index ~typ:typ2 yoffs in
-    if M.tracing then M.tracel "addr" "xoffs=%a typ1=%a xindex=%a yoffs=%a typ2=%a yindex=%a" pretty xoffs d_plaintype typ1 Idx.pretty x_index pretty yoffs d_plaintype typ2 Idx.pretty y_index;
+    if M.tracing then M.tracel "addr" "xoffs=%a typ1=%a xindex=%a yoffs=%a typ2=%a yindex=%a" pretty xoffs d_plaintype typ1 Idx.pp x_index pretty yoffs d_plaintype typ2 Idx.pp y_index;
     Idx.eq x_index y_index
 
   include Lattice.NoBotTop
diff --git a/src/cdomain/value/cdomains/structDomain.ml b/src/cdomain/value/cdomains/structDomain.ml
index 29277b0dab..ab230a38f1 100644
--- a/src/cdomain/value/cdomains/structDomain.ml
+++ b/src/cdomain/value/cdomains/structDomain.ml
@@ -49,6 +49,7 @@ struct
     Printable.get_short_list "<" ">" whole_str_list
 
   let pretty () = M.pretty ()
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let replace s field value = M.add field value s
   let get s field =
     match M.find_opt field s with
@@ -150,7 +151,7 @@ struct
   let create = hs_create
 
   let replace s field value =
-    if Messages.tracing then Messages.tracel "simplesets" "Normalize top Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pretty s Basetype.CilField.pretty field Val.pretty value;
+    if Messages.tracing then Messages.tracel "simplesets" "Normalize top Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pp s Basetype.CilField.pp field Val.pp value;
     HS.map (fun s -> SS.replace s field value) s
 
   let get = hs_get
@@ -219,7 +220,7 @@ struct
           let (overlapping, rem_uniq) = List.partition (fun ss -> SS.leq h ss || SS.leq ss h ) unique in
           let joined = List.fold_left (fun el acc ->
               let res = join_f acc el in
-              if Messages.tracing then Messages.tracel "simplesets-fct" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pretty acc SS.pretty el SS.pretty res;
+              if Messages.tracing then Messages.tracel "simplesets-fct" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pp acc SS.pp el SS.pp res;
               res
             ) h overlapping in
           aux (joined::rem_uniq) t
@@ -253,6 +254,8 @@ struct
     | Some k -> (HS.pretty () s) ++ (text " with key ") ++ (F.pretty () k)
     | None -> (HS.pretty () s) ++ (text " without key")
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let top () = (hs_top (), None)
   let is_top (s, _) = hs_is_top s
   let bot () = (hs_bot (), None)
@@ -312,14 +315,14 @@ struct
             aux (joined::rem_uniq) t
         in
         let res = aux [] (HS.elements s) in
-        if Messages.tracing then Messages.tracel "reduce-key" "Reduced - s:\n%a\nto:\n%a\n---------" HS.pretty s HS.pretty res;
+        if Messages.tracing then Messages.tracel "reduce-key" "Reduced - s:\n%a\nto:\n%a\n---------" HS.pp s HS.pp res;
         (res, Some key)
 
   let reduce_key (x: t): t = reduce_key_with_fct (SS.join) x
 
   let replace (s,k) field value : t =
     let join_set s =if HS.is_bot s then s else HS.singleton (join_ss s) in
-    if Messages.tracing then Messages.tracel "keyedsets" "Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pretty s Basetype.CilField.pretty field Val.pretty value ;
+    if Messages.tracing then Messages.tracel "keyedsets" "Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pp s Basetype.CilField.pp field Val.pp value ;
     let replaced = HS.map (fun s -> SS.replace s field value) s in
     let result_key =
       match find_key_field (s,k) with
@@ -411,7 +414,7 @@ struct
 
   let join_with_fct f (x, k) (y, _) =
     let appended = List.append (HS.elements x) (HS.elements y) in
-    if Messages.tracing then Messages.tracel "bettersets" "Join-fct start!\nx: %a\ny: %a" HS.pretty x HS.pretty y;
+    if Messages.tracing then Messages.tracel "bettersets" "Join-fct start!\nx: %a\ny: %a" HS.pp x HS.pp y;
     let reduce_list_key_with_fct join_f (xs: variant list) (x: t) =
       match find_key_field x with
       | None -> x
@@ -427,14 +430,14 @@ struct
               ) unique in
             let joined = List.fold_left (fun el acc ->
                 let res = join_f acc el in
-                if Messages.tracing then Messages.tracel "bettersets" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pretty acc SS.pretty el SS.pretty res;
+                if Messages.tracing then Messages.tracel "bettersets" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pp acc SS.pp el SS.pp res;
                 res
               ) h overlapping in
             aux (joined::rem_uniq) t
         in (aux [] xs, Some key)
     in
     let res = reduce_list_key_with_fct (SS.join_with_fct f) appended (x,k) in
-    if Messages.tracing then Messages.tracel "bettersets" "Join-fct result!\nx: %a\ny: %a\nconverted: %a\nres: %a" HS.pretty x HS.pretty y HS.pretty (HS.of_list appended) pretty res;
+    if Messages.tracing then Messages.tracel "bettersets" "Join-fct result!\nx: %a\ny: %a\nconverted: %a\nres: %a" HS.pp x HS.pp y HS.pp (HS.of_list appended) pretty res;
     res
 
   let join = join_with_fct Val.join
diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 5ac8f02d9c..5fcec1d3e0 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -127,6 +127,7 @@ struct
       Pretty.dprintf "%a, %a" P.pretty p S.pretty s
 
   let show x = GobPretty.sprint pretty x
+  let pp ppf x = Format.pp_print_string ppf (show x)
 
   module D = Lattice.Prod (struct
       include S
@@ -326,6 +327,8 @@ struct
     | Thread tid -> FlagConfiguredTID.show tid
     | UnknownThread -> "Unknown thread id"
 
+  let pp ppf t = Format.pp_print_string ppf (show t)
+
   let printXml f t =
     match t with
     | Thread tid -> FlagConfiguredTID.printXml f tid
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 401da647a2..eab15249a3 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -337,6 +337,8 @@ struct
     | Bot -> bot_name
     | Top -> top_name
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let pretty_diff () (x,y) =
     match (x,y) with
     | (Int x, Int y) -> ID.pretty_diff () (x,y)
@@ -471,7 +473,7 @@ struct
       | x -> x (* TODO we should also keep track of the type here *)
     in
     let a' = AD.map one_addr a in
-    if M.tracing then M.tracel "cast" "cast_addr %a to %a is %a!" AD.pretty a d_type t AD.pretty a';
+    if M.tracing then M.tracel "cast" "cast_addr %a to %a is %a!" AD.pp a CilType.Typ.pp t AD.pp a';
     a'
 
   (* this is called for:
@@ -488,7 +490,7 @@ struct
     | JmpBuf _ ->
       v
     | _ ->
-      let log_top (_,l,_,_) = if Messages.tracing then Messages.tracel "cast" "log_top at %d: %a to %a is top!" l pretty v d_type t in
+      let log_top (_,l,_,_) = if Messages.tracing then Messages.tracel "cast" "log_top at %d: %a to %a is top!" l pretty v CilType.Typ.pp t in
       let t = unrollType t in
       let v' = match t with
         | TInt (ik,_) ->
@@ -564,7 +566,7 @@ struct
           log_top __POS__; Top
         | _ -> log_top __POS__; assert false
       in
-      if Messages.tracing then Messages.tracel "cast" "cast %a to %a is %a!" pretty v d_type t pretty v';
+      if Messages.tracing then Messages.tracel "cast" "cast %a to %a is %a!" pretty v CilType.Typ.pp t pretty v';
       v'
 
 
@@ -903,7 +905,7 @@ struct
   (* Funny, this does not compile without the final type annotation! *)
   let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
     let rec do_eval_offset (x:t) (offs:offs) (l:lval option) (o:offset option): t =
-      if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp;
+      if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pp offs (Pretty.docOpt (CilType.Exp.pp ())) exp;
       let r =
         match x, offs with
         | Blob((va, _, zeroinit) as c), `Index (_, ox) ->
@@ -979,7 +981,7 @@ struct
 
   let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
     let rec do_update_offset ?(bitfield:int option=None) (x:t) (offs:offs) (l:lval option) (o:offset option) (t:typ):t = (* TODO: why does inner t argument change here, but not in eval_offset? *)
-      if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
+      if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pp offs (Pretty.docOpt (CilType.Exp.pp ())) exp pretty value;
       let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in
       let r =
         match x, offs with
diff --git a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
index 1db52f15a2..f00e0c0ca0 100644
--- a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
@@ -136,7 +136,7 @@ struct
     let res = bound_texpr d texpr1 in
     (if M.tracing then
        match res with
-       | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pretty min GobZ.pretty max
+       | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pp min GobZ.pp max
        | _ -> ()
     );
     res
@@ -210,6 +210,7 @@ struct
       "[|"^ (String.concat "; " constraint_list) ^"|]"
 
   let pretty () (x:t) = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
@@ -443,7 +444,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pp v Var.pp v' (show res);
     res
 
   let assign_var_parallel t vv's =                                (* vv's is a list of pairs of lhs-variables and their rhs-values *)
@@ -514,7 +515,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pp var CilType.Exp.pp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
@@ -573,7 +574,7 @@ struct
     res
 
   let assert_constraint ask d e negate no_ov =
-    if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov);
+    if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" CilType.Exp.pp e (Lazy.force no_ov);
     match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with
     | tcons1 -> meet_tcons ask d tcons1 e
     | exception Convert.Unsupported_CilExp _ -> d
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 06e131bbec..8f47c7926b 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -137,7 +137,7 @@ struct
     let res = bound_texpr d texpr1 in
     (if M.tracing then
        match res with
-       | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pretty min GobZ.pretty max
+       | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pp min GobZ.pp max
        | _ -> ()
     );
     res
@@ -212,6 +212,7 @@ struct
       "[|"^ (String.concat "; " constraint_list) ^"|]"
 
   let pretty () (x:t) = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
@@ -397,7 +398,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pp v Var.pp v' (show res);
     res
 
   let assign_var_parallel t vv's =                                (* vv's is a list of pairs of lhs-variables and their rhs-values *)
@@ -465,7 +466,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pp var CilType.Exp.pp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
@@ -524,7 +525,7 @@ struct
     res
 
   let assert_constraint ask d e negate no_ov =
-    if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov);
+    if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" CilType.Exp.pp e (Lazy.force no_ov);
     match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with
     | tcons1 -> meet_tcons ask d tcons1 e
     | exception Convert.Unsupported_CilExp _ -> d
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 2273ec5306..292967657f 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -283,7 +283,7 @@ struct
   let assign_exp_with ask nd v e no_ov =
     match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with
     | texpr1 ->
-      if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pretty texpr1;
+      if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pp texpr1;
       A.assign_texpr_with Man.mgr nd v texpr1 None
     | exception Convert.Unsupported_CilExp _ ->
       if M.tracing then M.trace "apron" "assign_exp unsupported";
@@ -446,6 +446,7 @@ struct
   let show (x:t) =
     GobFormat.asprintf "%a (env: %a)" A.print x Environment.pp (A.env x)
   let pretty () (x:t) = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
 
   let equal x y =
     Environment.equal (A.env x) (A.env y) && A.is_eq Man.mgr x y
@@ -501,7 +502,7 @@ struct
       LAnd, LOr, LNot are directly supported by Apron domain in order to
       confirm logic-containing Apron invariants from witness while deep-query is disabled *)
   let rec assert_constraint ask d e negate (no_ov: bool Lazy.t) =
-    if M.tracing then M.trace "assert_constraint_apron" "%a ;;; %a" d_exp e d_plainexp e;
+    if M.tracing then M.trace "assert_constraint_apron" "%a ;;; %a" CilType.Exp.pp e CilType.Exp.pp e;
     match e with
     (* Apron doesn't properly meet with DISEQ constraints: https://github.com/antoinemine/apron/issues/37.
        Join Gt and Lt versions instead. *)
@@ -533,14 +534,14 @@ struct
     | _ ->
       begin match Convert.tcons1_of_cil_exp ask d (A.env d) e negate no_ov with
         | tcons1 ->
-          if M.tracing then M.trace "apron" "assert_constraint %a %a" d_exp e Tcons1.pretty tcons1;
-          if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d;
-          if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1;
+          if M.tracing then M.trace "apron" "assert_constraint %a %a" CilType.Exp.pp e Tcons1.pp tcons1;
+          if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pp d;
+          if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pp tcons1;
           let r = meet_tcons ask d tcons1 e in
-          if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r;
+          if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pp r;
           r
         | exception Convert.Unsupported_CilExp reason ->
-          if M.tracing then M.trace "apron" "assert_constraint %a unsupported: %s" d_exp e (SharedFunctions.show_unsupported_cilExp reason);
+          if M.tracing then M.trace "apron" "assert_constraint %a unsupported: %s" CilType.Exp.pp e (SharedFunctions.show_unsupported_cilExp reason);
           d
       end
 
@@ -618,7 +619,7 @@ struct
     let x_cons = A.to_lincons_array Man.mgr x_j in
     let y_cons = A.to_lincons_array Man.mgr y_j in
     let try_add_con j con1 =
-      if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pretty con1;
+      if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pp con1;
       let t = meet_lincons j con1 in
       let t_x = A.change_environment Man.mgr t x_env false in
       let t_y = A.change_environment Man.mgr t y_env false in
@@ -657,7 +658,7 @@ struct
       in
       let env_exists_mem_con1 env con1 =
         let r = env_exists_mem_con1 env con1 in
-        if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pretty env Lincons1.pretty con1 r;
+        if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pp env Lincons1.pp con1 r;
         r
       in
       (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *)
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index e5c89d0e80..81db898057 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -328,7 +328,7 @@ struct
 
   let simplified_monomials_from_texp (t: t) texp =
     let res = simplified_monomials_from_texp t texp in
-    if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
+    if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pp texp
         (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);
     res
 
@@ -358,7 +358,7 @@ struct
     else
       match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with
       | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in
-        (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res;
+        (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pp res GobZ.pp res;
          Some res, Some res)
       | _ -> None, None
 
@@ -424,6 +424,7 @@ struct
         EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
 
   let pretty () (x:t) = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
@@ -646,7 +647,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pp v Var.pp v' (show res);
     res
 
   (** Parallel assignment of variables.
@@ -699,7 +700,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pp var CilType.Exp.pp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = Timing.wrap "substitution" (substitute_exp ask t var exp) no_ov
@@ -754,7 +755,7 @@ struct
           | _ -> t (* For equalities of more then 2 vars we just return t *))
 
   let meet_tcons ask t tcons original_expr no_ov  =
-    if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b" d_exp original_expr (Lazy.force no_ov);
+    if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b" CilType.Exp.pp original_expr (Lazy.force no_ov);
     meet_tcons ask t tcons original_expr no_ov
 
   let meet_tcons t tcons expr = Timing.wrap "meet_tcons" (meet_tcons t tcons) expr
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 5d266cf474..1d713f7d47 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -161,6 +161,8 @@ struct
     let third  = PrivD.show r.priv in
     "(" ^ first ^ ", " ^ third  ^ ")"
 
+  let pp ppf r = Format.pp_print_string ppf (show r)
+
   let pretty () r =
     text "(" ++
     RD.pretty () r.rel
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 53c8db8099..1b9c97964c 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -110,7 +110,7 @@ struct
         | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 ->
           ()
         | min_opt, max_opt ->
-          if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt;
+          if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)" CilType.Exp.pp exp (Pretty.docOpt (IntOps.BigIntOps.pp ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pp ())) max_opt;
           raise (Unsupported_CilExp Overflow)
       )
 
@@ -122,7 +122,7 @@ struct
           | `Bot  (* This happens when called on a pointer type; -> we can safely return top *)
           | `Top -> IntDomain.IntDomTuple.top_of ik
           | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in
-        if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res;
+        if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" CilType.Exp.pp e IntDomain.IntDomTuple.pp res;
         res
       in
       (* recurse without env and ask arguments *)
@@ -161,7 +161,7 @@ struct
                 let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))   in
                 let simp = query e ikind in
                 let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ~kind:Internal ikind simp in (* TODO: proper castkind *)
-                if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp;
+                if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" CilType.Exp.pp e IntDomain.IntDomTuple.pp simp;
                 BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const
               in
               let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in
@@ -222,7 +222,7 @@ struct
         M.tracel "rel-texpr-cil-conv" "unsuccessfull: %s" (show_unsupported_cilExp ex);
         raise (Unsupported_CilExp ex)
       | res ->
-        M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
+        M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" CilType.Exp.pp exp Texpr1.Expr.pp res (Lazy.force no_ov);
         M.tracel "rel-texpr-cil-conv" "successfull: Good";
         res
     else conv exp
@@ -584,7 +584,7 @@ struct
     | exception Invalid_argument _ ->
       ID.top () (* real top, not a top of any ikind because we don't even know the ikind *)
     | ik ->
-      if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" d_plainexp e (Cilfacade.exp_is_boolean e);
+      if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" CilType.Exp.pp e (Cilfacade.exp_is_boolean e);
       if Cilfacade.exp_is_boolean e then
         match check_assert ask d e no_ov with
         | `True -> ID.of_bool ik true
diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
index 64b5a174e8..24553fef47 100644
--- a/src/cdomains/baseDomain.ml
+++ b/src/cdomains/baseDomain.ml
@@ -70,6 +70,8 @@ struct
     PrivD.pretty () r.priv
     ++ text ")"
 
+  let pp ppf r = Format.pp_print_string ppf (show r)
+
   let printXml f r =
     let e = XmlUtil.escape in
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a\n<key>\n%s\n</key>\n%a</map>\n</value>\n"
diff --git a/src/cdomains/c2poDomain.ml b/src/cdomains/c2poDomain.ml
index edb42f64c7..5af518937c 100644
--- a/src/cdomains/c2poDomain.ml
+++ b/src/cdomains/c2poDomain.ml
@@ -281,7 +281,7 @@ module D = struct
   (** Remove terms from the data structure.
       It removes all terms that may point to one of the tainted addresses.*)
   let remove_tainted_terms ask address cc =
-    if M.tracing then M.tracel "c2po-tainted" "remove_tainted_terms: %a\n" MayBeEqual.AD.pretty address;
+    if M.tracing then M.tracel "c2po-tainted" "remove_tainted_terms: %a\n" MayBeEqual.AD.pp address;
     let may_be_tainted =
       MayBeEqual.may_point_to_one_of_these_addresses ask address cc
     in
diff --git a/src/cdomains/duplicateVars.ml b/src/cdomains/duplicateVars.ml
index fdeb99428b..c1aa8c0bd6 100644
--- a/src/cdomains/duplicateVars.ml
+++ b/src/cdomains/duplicateVars.ml
@@ -118,7 +118,7 @@ struct
 
   let to_varinfo v =
     let res = VarVarinfoMap.to_varinfo v in
-    if M.tracing then M.trace "c2po-varinfo" "to_varinfo: %a -> %a" d_type (get_type v) d_type res.vtype;
+    if M.tracing then M.trace "c2po-varinfo" "to_varinfo: %a -> %a" CilType.Typ.pp (get_type v) CilType.Typ.pp res.vtype;
     res
 
 end
diff --git a/src/cdomains/musteqDomain.ml b/src/cdomains/musteqDomain.ml
index c7a1cbc176..04c63da872 100644
--- a/src/cdomains/musteqDomain.ml
+++ b/src/cdomains/musteqDomain.ml
@@ -100,6 +100,8 @@ struct
     let content () = fold f mapping nil in
     dprintf "@[%s {\n  @[%t@]}@]" (show mapping) content
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let add_old = add
   let rec add (x,y) fd d =
     if V.equal x y || mem (x,y) d then d else
diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml
index 020ac9120e..6ce07940c1 100644
--- a/src/cdomains/symbLocksDomain.ml
+++ b/src/cdomains/symbLocksDomain.ml
@@ -237,7 +237,7 @@ struct
     | _            ,             _ -> raise (Invalid_argument "")
 
   let from_exps a l : t option =
-    if M.tracing then M.tracel "symb_locks" "from_exps %a (%s) %a (%s)" d_plainexp a (ees_to_str (toEl a)) d_plainexp l (ees_to_str (toEl l));
+    if M.tracing then M.tracel "symb_locks" "from_exps %a (%s) %a (%s)" CilType.Exp.pp a (ees_to_str (toEl a)) CilType.Exp.pp l (ees_to_str (toEl l));
     let a, l = toEl a, toEl l in
     (* ignore (printf "from_exps:\n %s\n %s\n" (ees_to_str a) (ees_to_str l)); *)
     (*let rec fold_left2 f a xs ys =
diff --git a/src/cdomains/unionFind.ml b/src/cdomains/unionFind.ml
index 585ea117ca..4ccbb8d0c1 100644
--- a/src/cdomains/unionFind.ml
+++ b/src/cdomains/unionFind.ml
@@ -357,7 +357,7 @@ module T = struct
         let const = to_cil_constant off (Some typ) in
         BinOp (PlusPI, cil_t, const, typ)
     in
-    if M.tracing then M.trace "c2po-2cil" "exp: %a; offset: %s; res: %a" d_exp cil_t (Z.to_string off) d_exp res;
+    if M.tracing then M.trace "c2po-2cil" "exp: %a; offset: %s; res: %a" CilType.Exp.pp cil_t (Z.to_string off) CilType.Exp.pp res;
     res
 
   let is_field = function
@@ -413,7 +413,7 @@ module T = struct
   (** Get a Cil expression that is equivalent to *(exp + offset),
       by taking into account type correctness.*)
   let dereference_exp exp offset =
-    if M.tracing then M.trace "c2po-deref" "exp: %a, offset: %s" d_exp exp (Z.to_string offset);
+    if M.tracing then M.trace "c2po-deref" "exp: %a, offset: %s" CilType.Exp.pp exp (Z.to_string offset);
     let res =
       let find_field cinfo =
         try
@@ -461,7 +461,7 @@ module T = struct
       else
         raise (UnsupportedCilExpression "not a pointer variable")
     in
-    if M.tracing then M.trace "c2po-deref" "deref result: %a" d_exp res;
+    if M.tracing then M.trace "c2po-deref" "deref result: %a" CilType.Exp.pp res;
     res
 
   let get_size t =  get_size_in_bits @@ type_of_term t
@@ -603,14 +603,14 @@ module T = struct
     | false ->
       let res = match of_cil_neg ask neg (Cil.constFold false e) with
         | exception (UnsupportedCilExpression s) ->
-          if M.tracing then M.trace "c2po-cil-conversion" "unsupported exp: %a\n%s\n" d_plainexp e s;
+          if M.tracing then M.trace "c2po-cil-conversion" "unsupported exp: %a\n%s\n" CilType.Exp.pp e s;
           None, None
         | t, z -> t, Some z
       in
       (if M.tracing && not neg then
          match res with
-         | None, Some z ->  M.trace "c2po-cil-conversion" "constant exp: %a --> %s\n" d_plainexp e (Z.to_string z)
-         | Some t, Some z -> M.trace "c2po-cil-conversion" "exp: %a --> %s + %s\n" d_plainexp e (show t) (Z.to_string z);
+         | None, Some z ->  M.trace "c2po-cil-conversion" "constant exp: %a --> %s\n" CilType.Exp.pp e (Z.to_string z)
+         | Some t, Some z -> M.trace "c2po-cil-conversion" "exp: %a --> %s + %s\n" CilType.Exp.pp e (show t) (Z.to_string z);
          | _ -> ());
       res
 
@@ -625,7 +625,7 @@ module T = struct
       if check_valid_pointer exp then
         Some t, Some z
       else begin
-        if M.tracing then M.trace "c2po-cil-conversion" "invalid exp: %a --> %s + %s\n" d_plainexp e (show t) (Z.to_string z);
+        if M.tracing then M.trace "c2po-cil-conversion" "invalid exp: %a --> %s + %s\n" CilType.Exp.pp e (show t) (Z.to_string z);
         None, None
       end
     | t, z -> t, z
diff --git a/src/common/cdomains/basetype.ml b/src/common/cdomains/basetype.ml
index 5ec9b22b44..fa86fbc50e 100644
--- a/src/common/cdomains/basetype.ml
+++ b/src/common/cdomains/basetype.ml
@@ -11,6 +11,7 @@ struct
       let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in
       "(" ^ x.vname ^ ", " ^ description ^ ")"
     else x.vname
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty () x = Pretty.text (show x)
   type group = Global | Local | Parameter | Temp [@@deriving ord, show { with_path = false }]
   let to_group = function
@@ -28,6 +29,7 @@ struct
   open Pretty
   type t = string [@@deriving eq, ord, hash, to_yojson]
   let show x = "\"" ^ x ^ "\""
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty () x = text (show x)
   let name () = "raw strings"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
@@ -125,6 +127,7 @@ module CilStmt: Printable.S with type t = stmt =
 struct
   include CilType.Stmt
   let show x = "<stmt>"
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty = Cilfacade.stmt_pretty_short
 
   let name () = "expressions"
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index 45a66ea336..3d5bfe4eeb 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -12,6 +12,7 @@ sig
   val compare: t -> t -> int
   val show: t -> string
   val pretty: unit -> t -> doc
+  val pp: Format.formatter -> t -> unit
   (* These two lets us reuse the short function, and allows some overriding
    * possibilities. *)
   val printXml : 'a BatInnerIO.output -> t -> unit
@@ -35,6 +36,7 @@ struct
   type t = | [@@deriving eq, ord, hash]
   let show (x: t) = match x with _ -> .
   let pretty () (x: t) = match x with _ -> .
+  let pp _ (x: t) = match x with _ -> .
   let printXml _ (x: t) = match x with _ -> .
   let name () = "empty"
   let to_yojson (x: t) = match x with _ -> .
@@ -71,6 +73,7 @@ end
 module SimpleShow (P: Showable) =
 struct
   let pretty () x = text (P.show x)
+  let pp ppf x = Format.pp_print_string ppf (P.show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (P.show x))
   let to_yojson x = `String (P.show x)
 end
@@ -84,6 +87,7 @@ end
 module SimplePretty (P: Prettyable) =
 struct
   let show x = GobPretty.sprint P.pretty x
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
   let to_yojson x = `String (show x)
 end
@@ -96,6 +100,7 @@ end
 
 module SimpleFormat (P: Formatable) =
 struct
+  let pp = P.pp
   let show x = GobFormat.asprint P.pp x
   let pretty () x = text (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
@@ -109,6 +114,7 @@ struct
   type t = unit [@@deriving eq, ord, hash]
   include StdLeaf
   let pretty () _ = text N.name
+  let pp ppf _ = Format.pp_print_string ppf N.name
   let show _ = N.name
   let name () = "Unit"
   let printXml f () = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape N.name)
@@ -132,6 +138,7 @@ struct
 
   let show = lift_f Base.show
   let pretty () = lift_f (Base.pretty ())
+  let pp ppf = lift_f (Base.pp ppf)
 
   (* Debug printing with tags *)
   (* let pretty () x = Pretty.dprintf "%a[%d,%d]" Base.pretty x.BatHashcons.obj x.BatHashcons.tag x.BatHashcons.hcode
@@ -189,6 +196,7 @@ struct
   let show = lift_f Base.show
 
   let pretty () = lift_f (Base.pretty ())
+  let pp ppf = lift_f (Base.pp ppf)
 
   let printXml f = lift_f (Base.printXml f)
   let to_yojson = lift_f (Base.to_yojson)
@@ -220,6 +228,8 @@ struct
     else
       Base.show x
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let printXml f x =
     if Conf.expand then
       BatPrintf.fprintf f "<value><map>\n<key>\n%s\n</key>\n%a</map>\n</value>\n" (Base.name ()) Base.printXml x
@@ -268,6 +278,8 @@ struct
     | `Bot -> bot_name
     | `Top -> top_name
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let pretty () (state:t) =
     match state with
     | `Lifted n ->  Base.pretty () n
@@ -329,6 +341,8 @@ struct
     | `Left n -> Base1.show n
     | `Right n -> Base2.show n
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name ()
   let printXml f = function
     | `Left x -> Base1.printXml f x
@@ -374,6 +388,8 @@ struct
     | `Middle n -> Base2.show n
     | `Right n -> Base3.show n
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () ^ " or " ^ Base3.name ()
   let printXml f = function
     | `Left x  -> Base1.printXml f x
@@ -408,6 +424,8 @@ struct
     | None -> N.name
     | Some n -> Base.show n
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let name () = Base.name () ^ " option"
   let printXml f = function
     | None -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape N.name)
@@ -451,6 +469,8 @@ struct
     | `Bot -> bot_name
     | `Top -> top_name
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let relift x = match x with
     | `Lifted1 n -> `Lifted1 (Base1.relift n)
     | `Lifted2 n -> `Lifted2 (Base2.relift n)
@@ -512,6 +532,8 @@ struct
     else
       text (show (x,y))
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let printXml f (x,y) =
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y
 
@@ -560,6 +582,8 @@ struct
     ++ unalign
     ++ text ")"
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let printXml f (x,y,z) =
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y (XmlUtil.escape (Base3.name ())) Base3.printXml z
 
@@ -579,6 +603,7 @@ struct
   let show x = "[" ^ (BatDeque.fold_right (fun a acc -> Base.show a ^ ", " ^ acc) x "]")
 
   let pretty () x = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let name () = Base.name () ^ "queue"
 
   let relift x = BatDeque.map Base.relift x
@@ -618,6 +643,7 @@ struct
     "[" ^ (String.concat ", " elems) ^ "]"
 
   let pretty () x = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
 
   let relift x = List.map Base.relift x
 
@@ -647,6 +673,7 @@ struct
 
   let show x = P.names x
   let pretty () x = text (show x)
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (P.names x)
   let to_yojson x = `String (P.names x)
 
@@ -665,6 +692,8 @@ struct
     | `Lifted n ->  Base.show n
     | `Bot -> "bot of " ^ (Base.name ())
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let pretty () (state:t) =
     match state with
     | `Lifted n ->  Base.pretty () n
@@ -696,6 +725,8 @@ struct
     | `Lifted n ->  Base.show n
     | `Top -> "top of " ^ (Base.name ())
 
+  let pp ppf x = Format.pp_print_string ppf (show x)
+
   let pretty () (state:t) =
     match state with
     | `Lifted n ->  Base.pretty () n
@@ -733,6 +764,7 @@ struct
   type t = string [@@deriving eq, ord, hash, to_yojson]
   include StdLeaf
   let pretty () n = text n
+  let pp ppf n = Format.pp_print_string ppf n
   let show n = n
   let name () = "String"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" x
@@ -756,6 +788,7 @@ struct
 
   let show _ = failwith Message.message
   let pretty _ _ = failwith Message.message
+  let pp _ _ = failwith Message.message
   let printXml _ _ = failwith Message.message
   let to_yojson _ = failwith Message.message
 
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index d2d1a92f8c..17a918e658 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -122,6 +122,10 @@ let rec pretty_edges () = function
   | [_,x] -> Edge.pretty_plain () x
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
+let pp_edges ppf edges =
+  let pp_sep ppf () = Format.pp_print_string ppf "; " in
+  Format.pp_print_list ~pp_sep (fun ppf (_,e) -> Edge.pp ppf e) ppf edges
+
 let node_scc_global = NH.create 113
 
 exception Not_connect of fundec
@@ -149,9 +153,9 @@ let createCFG (file: file) =
   let addEdges ?(skippedStatements = []) fromNode edges toNode =
     if Messages.tracing then
       Messages.trace "cfg" "Adding edges [%a] from\n\t%a\nto\n\t%a ... "
-        pretty_edges edges
-        Node.pretty_trace fromNode
-        Node.pretty_trace toNode;
+        pp_edges edges
+        Node.pp_trace fromNode
+        Node.pp_trace toNode;
     NH.replace fd_nodes fromNode ();
     NH.replace fd_nodes toNode ();
     H.modify_def [] toNode (List.cons (edges,fromNode)) cfgB;
diff --git a/src/common/framework/controlSpecC.ml b/src/common/framework/controlSpecC.ml
index eaec77f6c5..d83db16f8d 100644
--- a/src/common/framework/controlSpecC.ml
+++ b/src/common/framework/controlSpecC.ml
@@ -31,6 +31,7 @@ let tag x =
 let show x =
   let module C = (val !control_spec_c) in
   C.show (Obj.obj x)
+let pp ppf x = Format.pp_print_string ppf (show x)
 let pretty () x =
   let module C = (val !control_spec_c) in
   C.pretty () (Obj.obj x)
diff --git a/src/common/framework/edge.ml b/src/common/framework/edge.ml
index e6f214a4c8..da47e79142 100644
--- a/src/common/framework/edge.ml
+++ b/src/common/framework/edge.ml
@@ -47,6 +47,9 @@ let pretty () = function
   | Skip -> Pretty.text "skip"
   | VDecl v -> Cil.defaultCilPrinter#pVDecl () v
 
+let show x = GobPretty.sprint pretty x
+let pp ppf x = Format.pp_print_string ppf (show x)
+
 let pretty_plain () = function
   | Assign (lv,rv) -> dprintf "Assign '%a = %a' " d_lval lv d_exp rv
   | Proc (None  ,f,ars) -> dprintf "Proc '%a(%a)'" d_exp f (d_list ", " d_exp) ars
diff --git a/src/common/framework/node.ml b/src/common/framework/node.ml
index 906f9e1d77..fcd580d059 100644
--- a/src/common/framework/node.ml
+++ b/src/common/framework/node.ml
@@ -40,6 +40,8 @@ include Printable.SimplePretty (
   )
 (* TODO: deriving to_yojson gets overridden by SimplePretty *)
 
+let pp_trace ppf x = Format.pp_print_string ppf (show x)
+
 (** Show node ID for CFG and results output. *)
 let show_id = function
   | Statement stmt   -> string_of_int stmt.sid
diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml
index 8f26ff0087..a194708b5f 100644
--- a/src/common/util/gobFormat.ml
+++ b/src/common/util/gobFormat.ml
@@ -28,3 +28,7 @@ let asprintf (fmt: ('a, Format.formatter, unit, string) format4): 'a =
   Format.asprintf ("%t" ^^ fmt) pp_set_infinite_geometry
 
 let asprint pp x = asprintf "%a" pp x (* eta-expanded to bypass value restriction *)
+
+let pp_print_opt ?(none="?") pp ppf = function
+  | None -> Format.pp_print_string ppf none
+  | Some x -> pp ppf x
diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml
index 7fe00a6708..8b8d7620ff 100644
--- a/src/common/util/messages.ml
+++ b/src/common/util/messages.ml
@@ -344,20 +344,18 @@ let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt =
 
 include Goblint_tracing
 
-open Pretty
-
 let tracel sys ?var fmt =
   let loc = !current_loc in
-  let docloc sys doc =
-    printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc);
+  let strloc sys s =
+    printtrace sys (Format.asprintf "(%a) %s" CilType.Location.pp loc s)
   in
-  gtrace true docloc sys var ~loc ignore fmt
+  gtrace true strloc sys var ~loc ignore fmt
 
 let traceli sys ?var ?(subsys=[]) fmt =
   let loc = !current_loc in
   let g () = activate sys subsys in
-  let docloc sys doc: unit =
-    printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc);
+  let strloc sys s =
+    printtrace sys (Format.asprintf "(%a) %s" CilType.Location.pp loc s);
     traceIndent ()
   in
-  gtrace true docloc sys var ~loc g fmt
+  gtrace true strloc sys var ~loc g fmt
diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml
index 92012108c3..4ed108b746 100644
--- a/src/config/gobConfig.ml
+++ b/src/config/gobConfig.ml
@@ -304,7 +304,7 @@ struct
     try
       let st = String.trim st in
       let x = get_value !json_conf (parse_path st) in
-      if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a." st GobYojson.pretty x;
+      if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a." st GobYojson.pp x;
       try f x
       with Yojson.Safe.Util.Type_error (s, _) ->
         Logs.error "The value for '%s' has the wrong type: %s" st s;
@@ -362,7 +362,7 @@ struct
       @raise Invalid_argument
       @raise Json_encoding.Cannot_destruct *)
   let set_path_string st v =
-    if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pretty v;
+    if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pp v;
     set_value v json_conf (parse_path st)
 
   let set_json st j =
@@ -417,7 +417,7 @@ struct
     | Some fn ->
       let v = In_channel.with_open_text (Fpath.to_string fn) Yojson.Safe.from_channel in
       merge v;
-      if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a." GobFpath.pretty fn GobYojson.pretty !json_conf
+      if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a." GobFpath.pp fn GobYojson.pp !json_conf
     | None -> raise (Sys_error (Printf.sprintf "%s: No such file or directory" (Fpath.to_string fn)))
 end
 
diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml
index 7857d5a543..9e4fbdbd59 100644
--- a/src/constraint/constrSys.ml
+++ b/src/constraint/constrSys.ml
@@ -13,6 +13,7 @@ sig
   include Hashtbl.HashedType
   include SysVar with type t := t
   val pretty_trace: unit -> t -> GoblintCil.Pretty.doc
+  val pp_trace: Format.formatter -> t -> unit
   val compare : t -> t -> int
 
   val printXml : 'a BatInnerIO.output -> t -> unit
@@ -37,6 +38,8 @@ struct
     | `L a -> GoblintCil.Pretty.dprintf "L:%a" LV.pretty_trace a
     | `G a -> GoblintCil.Pretty.dprintf "G:%a" GV.pretty_trace a
 
+  let pp_trace ppf x = Format.pp_print_string ppf (GobPretty.sprint pretty_trace x)
+
   let printXml f = function
     | `L a -> LV.printXml f a
     | `G a -> GV.printXml f a
diff --git a/src/domain/flagHelper.ml b/src/domain/flagHelper.ml
index c3bcb584b2..fe1eb2d18e 100644
--- a/src/domain/flagHelper.ml
+++ b/src/domain/flagHelper.ml
@@ -31,6 +31,7 @@ struct
     | _ -> failwith Msg.msg
 
   let show = unop L.show R.show
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty () = unop (L.pretty ()) (R.pretty ())
   let printXml f = unop (L.printXml f) (R.printXml f)
   let to_yojson = unop L.to_yojson R.to_yojson
diff --git a/src/domain/hoareDomain.ml b/src/domain/hoareDomain.ml
index 1bd56c0d1d..f7edc1a632 100644
--- a/src/domain/hoareDomain.ml
+++ b/src/domain/hoareDomain.ml
@@ -162,6 +162,11 @@ struct
     let content = List.fold_left (++) nil separated in
     (text "{") ++ content ++ (text "}")
 
+  let pp ppf x =
+    let pp_sep ppf () = Format.fprintf ppf ", " in
+    Format.fprintf ppf "{%a}"
+      (Format.pp_print_list ~pp_sep E.pp) (elements x)
+
   let pretty_diff () ((x:t),(y:t)): Pretty.doc =
     Pretty.dprintf "HoarePO: %a not leq %a" pretty x pretty y
   let printXml f x =
diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml
index cf563dab44..0963c05cb1 100644
--- a/src/domain/mapDomain.ml
+++ b/src/domain/mapDomain.ml
@@ -79,6 +79,17 @@ struct
 
   let show map = GobPretty.sprint pretty map
 
+  let pp ppf map =
+    let first = ref true in
+    Format.fprintf ppf "@[{";
+    M.iter (fun k v ->
+        if !first then (first := false; Format.fprintf ppf "@[<v 2>@,")
+        else Format.fprintf ppf "@,";
+        Format.fprintf ppf "@[%a ->@ @[%a@]@]" D.pp k R.pp v
+      ) map;
+    if !first then Format.fprintf ppf "}"
+    else Format.fprintf ppf "@]}@]"
+
   let printXml f map =
     BatPrintf.fprintf f "<value>\n<map>\n";
     M.iter (fun k v ->
@@ -132,6 +143,28 @@ struct
 
   let show map = GobPretty.sprint pretty map
 
+  let pp ppf mapping =
+    let groups =
+      M.fold (fun k v acc ->
+          GroupMap.update (D.to_group k) (fun kvs ->
+              let kvs = Option.value kvs ~default:[] in
+              Some ((k, v) :: kvs)
+            ) acc
+        ) mapping GroupMap.empty
+    in
+    Format.fprintf ppf "@[{";
+    let first_group = ref true in
+    GroupMap.iter (fun group kvs ->
+        if !first_group then (first_group := false; Format.fprintf ppf "@[<v 2>@,")
+        else Format.fprintf ppf "@,";
+        Format.fprintf ppf "@[%s {@ @[<v>%a@]}@]" (D.show_group group)
+          (Format.pp_print_list (fun ppf (k, v) ->
+               Format.fprintf ppf "@[%a ->@ @[%a@]@]" D.pp k R.pp v))
+          (List.rev kvs)
+      ) groups;
+    if !first_group then Format.fprintf ppf "}"
+    else Format.fprintf ppf "@]}@]"
+
   (* TODO: groups in XML, JSON? *)
 end
 
diff --git a/src/domain/partitionDomain.ml b/src/domain/partitionDomain.ml
index e97946e463..70322ba238 100644
--- a/src/domain/partitionDomain.ml
+++ b/src/domain/partitionDomain.ml
@@ -54,6 +54,7 @@ struct
   type elem = S.elt
 
   let show _ = "Partitions"
+  let pp ppf x = Format.pp_print_string ppf (show x)
 
   let leq x y =
     for_all (fun p -> exists (S.leq p) y) x
@@ -105,6 +106,7 @@ struct
   type partition = t
 
   let show _ = "Partitions"
+  let pp ppf x = Format.pp_print_string ppf (show x)
 
   (* Top and bottom are reversed:
      Bottom will be All (equations), i.e. contradiction,
diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml
index e11c8182de..dde816035a 100644
--- a/src/domain/setDomain.ml
+++ b/src/domain/setDomain.ml
@@ -152,6 +152,11 @@ struct
     let all_elems : string list = List.map E.show (S.elements x) in
     Printable.get_short_list "{" "}" all_elems
 
+  let pp ppf x =
+    let pp_sep ppf () = Format.fprintf ppf ",@ " in
+    Format.fprintf ppf "@[{%a}@]"
+      (Format.pp_print_list ~pp_sep E.pp) (S.elements x)
+
   let to_yojson x = [%to_yojson: E.t list] (S.elements x)
 
   let printXml f xs =
@@ -361,6 +366,11 @@ struct
     | `Top -> N.topname
     | `Lifted t -> S.show t
 
+  let pp ppf x =
+    match x with
+    | `Top -> Format.pp_print_string ppf N.topname
+    | `Lifted t -> S.pp ppf t
+
 
   (* Lattice implementation *)
   (* Lift separately because lattice order might be different from subset order, e.g. after Reverse *)
@@ -430,6 +440,10 @@ struct
     let content = List.fold_left (++) nil separated in
     content
 
+  let pp ppf x =
+    let pp_sep ppf () = Format.fprintf ppf ", " in
+    Format.pp_print_list ~pp_sep Base.pp ppf (elements x)
+
   let pretty_diff () ((x:t),(y:t)): Pretty.doc =
     Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
   let printXml f xs =
diff --git a/src/domains/access.ml b/src/domains/access.ml
index 823e1cd589..044ddf5f7c 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -276,7 +276,7 @@ let get_val_type e: acc_typ =
 (** Add access to {!Memo} after distributing. *)
 let add_one ~side memo: unit =
   let ignorable = is_ignorable_memo memo in
-  if M.tracing then M.trace "access" "add_one %a (ignorable = %B)" Memo.pretty memo ignorable;
+  if M.tracing then M.trace "access" "add_one %a (ignorable = %B)" Memo.pp memo ignorable;
   if not ignorable then
     side memo
 
@@ -284,7 +284,7 @@ let add_one ~side memo: unit =
     Empty access sets are needed for prefix-type_suffix race checking. *)
 let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) =
   let memo = (`Type ts, o) in
-  if M.tracing then M.tracei "access" "add_distribute_outer %a" Memo.pretty memo;
+  if M.tracing then M.tracei "access" "add_distribute_outer %a" Memo.pp memo;
   add_one ~side memo; (* Add actual access for non-recursive call, or empty access for recursive call when side is side_empty. *)
 
   (* distribute to variables of the type *)
@@ -307,11 +307,11 @@ let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) =
 let add ~side ~side_empty e voffs =
   begin match voffs with
     | Some (v, o) -> (* known variable *)
-      if M.tracing then M.traceli "access" "add var %a%a" CilType.Varinfo.pretty v CilType.Offset.pretty o;
+      if M.tracing then M.traceli "access" "add var %a%a" CilType.Varinfo.pp v CilType.Offset.pp o;
       let memo = (`Var v, Offset.Unit.of_cil o) in
       add_one ~side memo
     | None -> (* unknown variable *)
-      if M.tracing then M.traceli "access" "add type %a" CilType.Exp.pretty e;
+      if M.tracing then M.traceli "access" "add type %a" CilType.Exp.pp e;
       let ty = get_val_type e in (* extract old acc_typ from expression *)
       let (t, o) = match ty with (* convert acc_typ to type-based Memo (components) *)
         | `Struct (c, o) -> (TComp (c, []), o)
@@ -485,7 +485,7 @@ struct
 end
 
 let group_may_race (warn_accs:WarnAccs.t) =
-  if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pretty warn_accs;
+  if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pp warn_accs;
   (* BFS to traverse one component with may_race edges *)
   let rec bfs' warn_accs ~todo ~visited =
     let todo_all = WarnAccs.union_all todo in
@@ -542,7 +542,7 @@ let group_may_race (warn_accs:WarnAccs.t) =
     )
   in
   let (comps, warn_accs) = components [] warn_accs in
-  if M.tracing then M.trace "access" "components %a" WarnAccs.pretty warn_accs;
+  if M.tracing then M.trace "access" "components %a" WarnAccs.pp warn_accs;
   (* repeat BFS to find all prefix-type_suffix-only components starting from prefix accesses (symmetric) *)
   let rec components_cross comps ~prefix ~type_suffix =
     if AS.is_empty prefix then
@@ -550,7 +550,7 @@ let group_may_race (warn_accs:WarnAccs.t) =
     else (
       let prefix_acc = AS.choose prefix in
       let (warn_accs', comp) = bfs {(WarnAccs.empty ()) with prefix; type_suffix} {(WarnAccs.empty ()) with prefix=AS.singleton prefix_acc} in
-      if M.tracing then M.trace "access" "components_cross %a" WarnAccs.pretty warn_accs';
+      if M.tracing then M.trace "access" "components_cross %a" WarnAccs.pp warn_accs';
       let comps' =
         if AS.cardinal comp > 1 then
           comp :: comps
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index f655d89316..187fe7f500 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -35,6 +35,8 @@ struct
     (* if get_bool "dbg.trace.context" then dprintf "(%a, %d) on %a" Node.pretty_trace n (LD.tag c) CilType.Location.pretty (getLocation x) *)
     else dprintf "%a on %a" Node.pretty_trace n CilType.Location.pretty (getLocation x)
 
+  let pp_trace ppf x = Format.pp_print_string ppf (GobPretty.sprint pretty_trace x)
+
   let printXml f (n,c) =
     Var.printXml f n;
     BatPrintf.fprintf f "<context>\n";
@@ -63,6 +65,7 @@ struct
   let var_id = show
   let node _ = MyCFG.Function Cil.dummyFunDec
   let pretty_trace = pretty
+  let pp_trace = pp
   let is_write_only = function
     | `Left x -> V.is_write_only x
     | `Right _ -> true
@@ -79,6 +82,7 @@ struct
   let var_id = show
   let node _ = MyCFG.Function Cil.dummyFunDec
   let pretty_trace = pretty
+  let pp_trace = pp
   let is_write_only = function
     | `Left x -> V.is_write_only x
     | `Right _ -> true
diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml
index 2d9fe623c7..f894248b17 100644
--- a/src/framework/analysisResult.ml
+++ b/src/framework/analysisResult.ml
@@ -53,6 +53,7 @@ struct
   open S
   include Printable.Prod3 (C) (D) (CilType.Fundec)
   let show (es,x,f:t) = D.show x
+  let pp ppf x = Format.pp_print_string ppf (show x)
   let pretty () (_,x,_) = D.pretty () x
   let printXml f (c,d,fd) =
     BatPrintf.fprintf f "<context>\n%a</context>\n%a" C.printXml c D.printXml d
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index bb77519cbf..098a7592ba 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -188,8 +188,8 @@ struct
 
   let tf_normal_call man lv e (f:fundec) args getl sidel demandl getg sideg =
     let combine (cd, fc, fd) =
-      if M.tracing then M.traceli "combine" "local: %a" S.D.pretty cd;
-      if M.tracing then M.trace "combine" "function: %a" S.D.pretty fd;
+      if M.tracing then M.traceli "combine" "local: %a" S.D.pp cd;
+      if M.tracing then M.trace "combine" "function: %a" S.D.pp fd;
       let rec cd_man =
         { man with
           ask = (fun (type a) (q: a Queries.t) -> S.query cd_man q);
@@ -236,7 +236,7 @@ struct
           S.D.join acc (S.combine_assign combine_assign_man lv e f args fc fd1_man.local (Analyses.ask_of_man fd1_man))
         ) (S.D.bot ()) (S.paths_as_set fd_man)
       in
-      if M.tracing then M.traceu "combine" "combined local: %a" S.D.pretty r;
+      if M.tracing then M.traceu "combine" "combined local: %a" S.D.pp r;
       r
     in
     let paths = S.enter man lv f args in
@@ -249,7 +249,7 @@ struct
     if M.tracing then M.traceli "combine" "combining";
     let paths = List.map combine paths in
     let r = List.fold_left D.join (D.bot ()) paths in
-    if M.tracing then M.traceu "combine" "combined: %a" S.D.pretty r;
+    if M.tracing then M.traceu "combine" "combined: %a" S.D.pp r;
     r
 
 
diff --git a/src/framework/control.ml b/src/framework/control.ml
index f2bfffde2d..07aeef3624 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -291,7 +291,7 @@ struct
     let gh = GHT.create 13 in
     let getg v = GHT.find_default gh v (EQSys.G.bot ()) in
     let sideg v d =
-      if M.tracing then M.trace "global_inits" "sideg %a = %a" EQSys.GVar.pretty v EQSys.G.pretty d;
+      if M.tracing then M.trace "global_inits" "sideg %a = %a" EQSys.GVar.pp v EQSys.G.pp d;
       GHT.replace gh v (EQSys.G.join (getg v) d)
     in
     (* Old-style global function for context.
@@ -320,15 +320,15 @@ struct
       let funs = ref [] in
       (*let count = ref 0 in*)
       let transfer_func (st : Spec.D.t) (loc, edge) : Spec.D.t =
-        if M.tracing then M.trace "con" "Initializer %a" CilType.Location.pretty loc;
+        if M.tracing then M.trace "con" "Initializer %a" CilType.Location.pp loc;
         (*incr count;
           if (get_bool "dbg.verbose")&& (!count mod 1000 = 0)  then Printf.printf "%d %!" !count;    *)
         match edge with
         | MyCFG.Entry func        ->
-          if M.tracing then M.trace "global_inits" "Entry %a" d_lval (var func.svar);
+          if M.tracing then M.trace "global_inits" "Entry %a" CilType.Lval.pp (var func.svar);
           Spec.body {man with local = st} func
         | MyCFG.Assign (lval,exp) ->
-          if M.tracing then M.trace "global_inits" "Assign %a = %a" d_lval lval d_exp exp;
+          if M.tracing then M.trace "global_inits" "Assign %a = %a" CilType.Lval.pp lval CilType.Exp.pp exp;
           begin match lval, exp with
             | (Var v,o), (AddrOf (Var f,NoOffset))
               when v.vstorage <> Static && isFunctionType f.vtype ->
@@ -338,7 +338,7 @@ struct
           let res = Spec.assign {man with local = st} lval exp in
           (* Needed for privatizations (e.g. None) that do not side immediately *)
           let res' = Spec.sync {man with local = res} `Normal in
-          if M.tracing then M.trace "global_inits" "\t\t -> state:%a" Spec.D.pretty res;
+          if M.tracing then M.trace "global_inits" "\t\t -> state:%a" Spec.D.pp res;
           res'
         | _                       -> failwith "Unsupported global initializer edge"
       in
@@ -355,7 +355,7 @@ struct
       let with_externs = do_extern_inits man file in
       (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges);    *)
       let result : Spec.D.t = List.fold_left transfer_func with_externs edges in
-      if M.tracing then M.trace "global_inits" "startstate: %a" Spec.D.pretty result;
+      if M.tracing then M.trace "global_inits" "startstate: %a" Spec.D.pp result;
       result, !funs
     in
 
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 4d01d7e166..568baef828 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -129,7 +129,7 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b
     a, b, c, (updatedCompinfoRenames, updatedEnumRenames)
   in
 
-  if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)" d_type a d_type b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *)
+  if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)" CilType.Typ.pp a CilType.Typ.pp b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *)
   let r, updated_rename_mapping = match a, b with
     | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2
     | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp lenExp1 lenExp2 ~acc &&>>  forward_list_equal (eq_attribute ~acc) attr1 attr2
@@ -175,7 +175,7 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b
     | TFloat (fk1, attr1), TFloat (fk2, attr2) -> (fk1 = fk2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2
     | _, _ -> false, rename_mapping
   in
-  if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" d_type a d_type b;
+  if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" CilType.Typ.pp a CilType.Typ.pp b;
   (r, updated_rename_mapping)
 
 and eq_eitems (a: string * attributes * exp * location) (b: string * attributes * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
diff --git a/src/lifters/longjmpLifter.ml b/src/lifters/longjmpLifter.ml
index c392499ef6..035617d0ea 100644
--- a/src/lifters/longjmpLifter.ml
+++ b/src/lifters/longjmpLifter.ml
@@ -146,7 +146,7 @@ struct
         | Target (target_node, target_context) ->
           let target_fundec = Node.find_fundec target_node in
           if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (man.control_context ()) then (
-            if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %a" Node.pretty target_node;
+            if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %a" Node.pp target_node;
             man.sideg (V.longjmpto (target_node, man.context ())) (G.create_local (Lazy.force combined))
             (* No need to propagate this outwards here, the set of valid longjumps is part of the context, we can never have the same context setting the longjmp multiple times *)
           )
@@ -160,9 +160,9 @@ struct
       in
       JmpBufDomain.JmpBufSet.iter handle_target active_targets
     in
-    if M.tracing then M.tracel "longjmp" "longfd getg %a" CilType.Fundec.pretty f;
+    if M.tracing then M.tracel "longjmp" "longfd getg %a" CilType.Fundec.pp f;
     let longfd = G.local (man.global (V.longjmpret (f, Option.get fc))) in
-    if M.tracing then M.tracel "longjmp" "longfd %a" D.pretty longfd;
+    if M.tracing then M.tracel "longjmp" "longfd %a" D.pp longfd;
     if not (D.is_bot longfd) then
       handle_longjmp (man.local, fc, longfd);
     S.combine_env (conv_man) lv e f args fc fd f_ask
@@ -215,7 +215,7 @@ struct
         (* Eval `env` again to avoid having to construct bespoke man to ask *)
         let targets = path_man.ask (EvalJumpBuf env) in
         let valid_targets = path_man.ask ValidLongJmp in
-        if M.tracing then Messages.tracel "longjmp" "Jumping to %a" JmpBufDomain.JmpBufSet.pretty targets;
+        if M.tracing then Messages.tracel "longjmp" "Jumping to %a" JmpBufDomain.JmpBufSet.pp targets;
         let handle_target target = match target with
           | JmpBufDomain.BufferEntryOrTop.AllTargets ->
             M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env;
@@ -223,7 +223,7 @@ struct
           | Target (target_node, target_context) ->
             let target_fundec = Node.find_fundec target_node in
             if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (man.control_context ()) then (
-              if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %a" Node.pretty target_node;
+              if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %a" Node.pp target_node;
               man.sideg (V.longjmpto (target_node, man.context ())) (G.create_local (Lazy.force specialed))
             )
             else if JmpBufDomain.JmpBufSet.mem target valid_targets then (
diff --git a/src/lifters/specLifters.ml b/src/lifters/specLifters.ml
index b3fd321c15..73930cab48 100644
--- a/src/lifters/specLifters.ml
+++ b/src/lifters/specLifters.ml
@@ -722,10 +722,10 @@ struct
     assert (D.cardinal man.local = 1);
     let cd = D.choose man.local in
     let k x y =
-      if M.tracing then M.traceli "combine" "function: %a" Spec.D.pretty x;
+      if M.tracing then M.traceli "combine" "function: %a" Spec.D.pp x;
       try
         let r = Spec.combine_env (conv man cd) l fe f a fc x f_ask in
-        if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pretty r;
+        if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pp r;
         D.add r y
       with Deadcode ->
         if M.tracing then M.traceu "combine" "combined function: dead";
@@ -738,10 +738,10 @@ struct
     assert (D.cardinal man.local = 1);
     let cd = D.choose man.local in
     let k x y =
-      if M.tracing then M.traceli "combine" "function: %a" Spec.D.pretty x;
+      if M.tracing then M.traceli "combine" "function: %a" Spec.D.pp x;
       try
         let r = Spec.combine_assign (conv man cd) l fe f a fc x f_ask in
-        if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pretty r;
+        if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pp r;
         D.add r y
       with Deadcode ->
         if M.tracing then M.traceu "combine" "combined function: dead";
diff --git a/src/solver/generic.ml b/src/solver/generic.ml
index a8bf588182..6f300604f6 100644
--- a/src/solver/generic.ml
+++ b/src/solver/generic.ml
@@ -46,7 +46,7 @@ struct
   let increase (v:Var.t) =
     let set v c =
       if not full_trace && (c > start_c && c > !max_c && not (GobOption.exists (Var.equal v) !max_var)) then begin
-        if tracing then trace "sol" "Switched tracing to %a" Var.pretty_trace v;
+        if tracing then trace "sol" "Switched tracing to %a" Var.pp_trace v;
         max_c := c;
         max_var := Some v
       end
@@ -64,20 +64,20 @@ struct
 
   let new_var_event x =
     incr SolverStats.vars;
-    if tracing then trace "sol" "New %a" Var.pretty_trace x
+    if tracing then trace "sol" "New %a" Var.pp_trace x
 
   let get_var_event x =
-    if tracing && full_trace then trace "sol" "Querying %a" Var.pretty_trace x
+    if tracing && full_trace then trace "sol" "Querying %a" Var.pp_trace x
 
   let eval_rhs_event x =
-    if tracing && full_trace then trace "sol" "(Re-)evaluating %a" Var.pretty_trace x;
+    if tracing && full_trace then trace "sol" "(Re-)evaluating %a" Var.pp_trace x;
     incr SolverStats.evals;
     if (get_bool "dbg.solver-progress") then (incr stack_d; Logs.debug "%d" !stack_d)
 
   let update_var_event x o n =
     if tracing then increase x;
     if full_trace || (not (Dom.is_bot o) && GobOption.exists (Var.equal x) !max_var) then begin
-      if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pretty_trace x;
+      if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pp_trace x;
       if tracing then traceu "sol_max" "%a" Dom.pretty_diff (n, o)
     end
 
diff --git a/src/solver/postSolver.ml b/src/solver/postSolver.ml
index 449e4e5bdd..902276806c 100644
--- a/src/solver/postSolver.ml
+++ b/src/solver/postSolver.ml
@@ -192,7 +192,7 @@ struct
 
     let reachable = PS.init_reachable ~vh in
     let rec one_var x =
-      if M.tracing then M.trace "postsolver" "one_var %a reachable=%B system=%B" S.Var.pretty_trace x (VH.mem reachable x) (Option.is_some (S.system x));
+      if M.tracing then M.trace "postsolver" "one_var %a reachable=%B system=%B" S.Var.pp_trace x (VH.mem reachable x) (Option.is_some (S.system x));
       if not (VH.mem reachable x) then (
         VH.replace reachable x ();
         Option.may (one_constraint x) (S.system x)
@@ -203,13 +203,13 @@ struct
         try VH.find vh y with Not_found -> S.Dom.bot ()
       in
       let set y d =
-        if M.tracing then M.trace "postsolver" "one_side %a %a %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty d;
+        if M.tracing then M.trace "postsolver" "one_side %a %a %a" S.Var.pp_trace x S.Var.pp_trace y S.Dom.pp d;
         PS.one_side ~vh ~x ~y ~d;
         (* check before recursing *)
         one_var y
       in
       let rhs = f get set in
-      if M.tracing then M.trace "postsolver" "one_constraint %a %a" S.Var.pretty_trace x S.Dom.pretty rhs;
+      if M.tracing then M.trace "postsolver" "one_constraint %a %a" S.Var.pp_trace x S.Dom.pp rhs;
       PS.one_constraint ~vh ~x ~rhs
     in
     (Timing.wrap "postsolver_iter" (List.iter one_var)) vs;
diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml
index 968ca6879f..cab31f6b4f 100644
--- a/src/solver/sLR.ml
+++ b/src/solver/sLR.ml
@@ -62,8 +62,8 @@ module SLR3 =
           let old = HM.find rho x in
           let tmp = eq x (eval x) (side x) in
           let tmp = S.Dom.join tmp (sides x) in
-          if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-          if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
+          if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+          if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp;
           let tmp =
             if wpx then
               if HM.mem globals x then S.Dom.widen old (S.Dom.join old tmp)
@@ -72,7 +72,7 @@ module SLR3 =
           in
           if not (S.Dom.equal old tmp) then begin
             update_var_event x old tmp;
-            if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
+            if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp;
             HM.replace rho x tmp;
             let w = try HM.find infl x with Not_found -> VS.empty in
             let w = if wpx then VS.add x w else w in
@@ -401,11 +401,11 @@ module Make0 =
           let use_box = (not (V.ver>1)) || HM.mem wpoint x in
           let restart_mode_x = h_find_default restart_mode x (2*GobConfig.get_int "solvers.slr4.restart_count") in
           let rstrt = use_box && (V.ver>3) && D.leq tmp old && restart_mode_x <> 0 in
-          if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-          if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
+          if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+          if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp;
           let tmp = if use_box then box old tmp else tmp in
           if not (D.eq tmp old) then begin
-            if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
+            if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp;
             let _ = X.set_value x tmp in
             if V.ver>3 && restart_mode_x mod 2 = 1 && not (D.leq tmp old) then
               HM.replace restart_mode x (restart_mode_x - 1);
diff --git a/src/solver/sLRphased.ml b/src/solver/sLRphased.ml
index feff5514f3..5863efa89d 100644
--- a/src/solver/sLRphased.ml
+++ b/src/solver/sLRphased.ml
@@ -72,7 +72,7 @@ module Make =
         let effects = ref Set.empty in
         let side y d =
           assert (not (S.Dom.is_bot d));
-          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pp_trace y S.Dom.pp d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -83,7 +83,7 @@ module Make =
             if not (HM.mem rho y) then (
               if b then solve1 (HM.find key x - 1) ~side:true y else solve0 ~side:true y
             ) else (
-              (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pretty_trace y (HM.find key y) S.Dom.pretty d; *)
+              (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pp_trace y (HM.find key y) S.Dom.pp d; *)
               if HM.find key y < 0 then HM.replace key y (Ref.post_decr count_side)
             );
             q := H.add y !q
@@ -101,28 +101,28 @@ module Make =
         let tmp = eq x eval side in
         let tmp = S.Dom.join tmp (sides x) in
         (* if (b && not (S.Dom.leq old tmp)) then ( *)
-        (*   trace "sol" "Var: %a\nOld: %a\nTmp: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp; *)
+        (*   trace "sol" "Var: %a\nOld: %a\nTmp: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp; *)
         (*   assert false *)
         (* ); *)
         let val_new =
           if wpx then
             if b then
               let nar = narrow old tmp in
-              if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp nar;
               nar
             else
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp wid;
               wid
           else
             tmp
         in
-        if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-        if tracing then trace "sol" "Contrib:%a" S.Dom.pretty val_new;
+        if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+        if tracing then trace "sol" "Contrib:%a" S.Dom.pp val_new;
         if S.Dom.equal old val_new then ()
         else begin
           update_var_event x old val_new;
-          if tracing then trace "sol" "New Value:%a" S.Dom.pretty val_new;
+          if tracing then trace "sol" "New Value:%a" S.Dom.pp val_new;
           HM.replace rho x val_new;
           let w = try HM.find infl x with Not_found -> VS.empty in
           (* let w = if wpx then VS.add x w else w in *)
@@ -162,7 +162,7 @@ module Make =
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ())
-        in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v
+        in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pp_trace x S.Dom.pp v; v
       and eq x get set =
         eval_rhs_event x;
         match S.system x with
diff --git a/src/solver/sLRterm.ml b/src/solver/sLRterm.ml
index 7cde3e10ae..8838b3f02b 100644
--- a/src/solver/sLRterm.ml
+++ b/src/solver/sLRterm.ml
@@ -63,14 +63,14 @@ module SLR3term =
           HM.replace rho  x (S.Dom.bot ());
           HM.replace infl x (VS.add x VS.empty);
           let c = if side then count_side else count in
-          if tracing then trace "sol" "INIT: Var: %a with prio %d" S.Var.pretty_trace x !c;
+          if tracing then trace "sol" "INIT: Var: %a with prio %d" S.Var.pp_trace x !c;
           HM.replace key x !c; decr c
         end
       in
       let sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
-        if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v
+        if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pp_trace x S.Dom.pp v; v
       in
       let rec iterate b_old prio =
         if H.size !q = 0 || min_key q > prio then ()
@@ -121,7 +121,7 @@ module SLR3term =
           )
           *)
           (* if S.Dom.is_bot d then print_endline "BOT" else *)
-          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pp_trace y S.Dom.pp d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -132,7 +132,7 @@ module SLR3term =
               ignore @@ do_var false y
               (* solve ~side:true y *)
             ) else (
-              (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pretty_trace y (HM.find key y) S.Dom.pretty d; *)
+              (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pp_trace y (HM.find key y) S.Dom.pp d; *)
               if HM.find key y < 0 then (
                 HM.replace key y (Ref.post_decr count_side);
                 q := rebuild !q
@@ -155,28 +155,28 @@ module SLR3term =
           if wpx then
             if S.Dom.leq tmp old then (
               let nar = narrow old tmp in
-              if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp nar;
               nar, true
             ) else
             if b_old then (
               let nar = narrow old tmp in
-              if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp nar;
               nar, true
             )
             else (
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp wid;
               wid, false
             )
           else
             tmp, b_old
         in
-        if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-        if tracing then trace "sol" "Contrib:%a" S.Dom.pretty val_new;
+        if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+        if tracing then trace "sol" "Contrib:%a" S.Dom.pp val_new;
         if S.Dom.equal old val_new then ()
         else begin
           update_var_event x old val_new;
-          if tracing then trace "sol" "New Value:%a" S.Dom.pretty val_new;
+          if tracing then trace "sol" "New Value:%a" S.Dom.pp val_new;
           HM.replace rho x val_new;
           let w = try HM.find infl x with Not_found -> VS.empty in
           (* let w = if wpx then VS.add x w else w in *)
diff --git a/src/solver/sideWPointSelect.ml b/src/solver/sideWPointSelect.ml
index fc0fd17fa8..6f6d01a55d 100644
--- a/src/solver/sideWPointSelect.ml
+++ b/src/solver/sideWPointSelect.ml
@@ -202,7 +202,7 @@ module Cycle : S =
     let should_mark_wpoint state called old_sides x y cycle =
       match cycle with
       | Some cycle ->
-        if tracing && cycle then trace "side_widen" "cycle: should mark wpoint %a" S.Var.pretty_trace y;
+        if tracing && cycle then trace "side_widen" "cycle: should mark wpoint %a" S.Var.pp_trace y;
         cycle
       | None ->
         failwith "destabilize_vs information not provided to side_widen cycle strategy";
diff --git a/src/solver/td3.ml b/src/solver/td3.ml
index a3ecd439e9..8d64e6d7b1 100644
--- a/src/solver/td3.ml
+++ b/src/solver/td3.ml
@@ -304,7 +304,7 @@ module Base =
       let cache_sizes = ref [] in
 
       let add_infl y x =
-        if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x;
         HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty));
         if collect_dep then
           HM.replace dep x (VS.add y (HM.find_default dep x VS.empty));
@@ -326,7 +326,7 @@ module Base =
         | Some old_gas ->
           let decremented_gas = old_gas - 1 in
           if decremented_gas >= 0 then (
-            if tracing then trace "widengas" "reducing gas of %a: %d -> %d" S.Var.pretty_trace x old_gas decremented_gas;
+            if tracing then trace "widengas" "reducing gas of %a: %d -> %d" S.Var.pp_trace x old_gas decremented_gas;
             HM.replace wpoint_gas x decremented_gas
           )
         | None -> ((* Not a widening point *)) in
@@ -335,7 +335,7 @@ module Base =
 
       (* Same as destabilize, but returns true if it destabilized a called var, or a var in vs which was stable. *)
       let rec destabilize_vs x = (* TODO remove? Only used for side_widen cycle. *)
-        if tracing then trace "sol2" "destabilize_vs %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "destabilize_vs %a" S.Var.pp_trace x;
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.fold (fun y b ->
@@ -350,11 +350,11 @@ module Base =
           ) w false (* nosemgrep: fold-exists *) (* does side effects *)
       and eq_wrapper x eqx  = ((UpdateRule.get_wrapper ~solve_widen:(fun x-> solve x Widen) ~init ~stable ~data:update_rule_data ~sides ~add_sides ~rho ~destabilize ~side ~assert_can_receive_side):UpdateRule.eq_wrapper) x eqx
       and solve ?reuse_eq x phase =
-        if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %a" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) pretty_wpoint x;
+        if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %a" S.Var.pp_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) pretty_wpoint x;
         init x;
         assert (Hooks.system x <> None);
         if not (HM.mem called x || HM.mem stable x) then (
-          if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace x;
+          if tracing then trace "sol2" "stable add %a" S.Var.pp_trace x;
           HM.replace stable x ();
           HM.replace called x ();
           (* Here we cache should_widen x before eq. If during eq eval makes x wpoint (with config widen_gas = 0), then be still don't apply widening the first time, but just overwrite.
@@ -368,7 +368,7 @@ module Base =
             match reuse_eq with
             | Some d when narrow_reuse ->
               (* Do not reset deps for reuse of eq *)
-              if tracing then trace "sol2" "eq reused %a" S.Var.pretty_trace x;
+              if tracing then trace "sol2" "eq reused %a" S.Var.pp_trace x;
               incr SolverStats.narrow_reuses;
               d
             | _ ->
@@ -395,15 +395,15 @@ module Base =
             else
               box old eqd
           in
-          if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd;
+          if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a" S.Var.pp_trace x wp S.Dom.pp old S.Dom.pp eqd S.Dom.pp wpd;
           if cache then (
-            if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pretty_trace x;
+            if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pp_trace x;
             cache_sizes := HM.length l :: !cache_sizes;
           );
           if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* value changed *)
             if tracing then trace "sol" "Changed";
-            (* if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a -> %a" S.Var.pretty_trace x pretty_wpoint x S.Dom.pretty old S.Dom.pretty wpd; *)
-            if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a" S.Var.pretty_trace x pretty_wpoint x S.Dom.pretty_diff (wpd, old);
+            (* if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a -> %a" S.Var.pp_trace x pretty_wpoint x S.Dom.pp old S.Dom.pp wpd; *)
+            if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a" S.Var.pp_trace x pretty_wpoint x S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
             HM.replace rho x wpd;
             destabilize x;
@@ -411,30 +411,30 @@ module Base =
           ) else (
             (* TODO: why non-equal and non-stable checks in switched order compared to TD3 paper? *)
             if not (HM.mem stable x) then ( (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
-              if tracing then trace "sol2" "solve still unstable %a" S.Var.pretty_trace x;
+              if tracing then trace "sol2" "solve still unstable %a" S.Var.pp_trace x;
               (solve[@tailcall]) x Widen
             ) else (
               if term && phase = Widen && HM.mem wpoint_gas x then ( (* TODO: or use wp? *)
-                if tracing then trace "sol2" "solve switching to narrow %a" S.Var.pretty_trace x;
-                if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace x;
+                if tracing then trace "sol2" "solve switching to narrow %a" S.Var.pp_trace x;
+                if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace x;
                 HM.remove stable x;
                 HM.remove superstable x;
                 Hooks.stable_remove x;
                 (solve[@tailcall]) ~reuse_eq:eqd x Narrow
               ) else if remove_wpoint && not space && (not term || phase = Narrow) then ( (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *)
-                if tracing then trace "sol2" "solve removing wpoint %a (%a)" S.Var.pretty_trace x pretty_wpoint x;
+                if tracing then trace "sol2" "solve removing wpoint %a (%a)" S.Var.pp_trace x pretty_wpoint x;
                 HM.remove wpoint_gas x;
               )
             )
           )
         )
       and eq x get set demand =
-        if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "eq %a" S.Var.pp_trace x;
         match Hooks.system x with
         | None -> S.Dom.bot ()
         | Some f -> f get set demand
       and simple_solve l x y =
-        if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pretty_trace y (Hooks.system y <> None);
+        if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pp_trace y (Hooks.system y <> None);
         if Hooks.system y = None then (init y; HM.replace stable y (); HM.find rho y) else
           (* TODO: should td_space store information for widening points with remaining gas? *)
         if not space || HM.mem wpoint_gas y then (solve y Widen; HM.find rho y) else
@@ -453,7 +453,7 @@ module Base =
           else (if cache then HM.replace l y eqd; eqd)
         )
       and eval l x y =
-        if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y;
+        if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y;
         get_var_event y;
         if HM.mem called y then (
           if restart_wpoint && not (HM.mem wpoint_gas y) then (
@@ -461,30 +461,30 @@ module Base =
                The loop body might then side effect the old value, see tests/incremental/06-local-wpoint-read.
                Here we avoid this, by setting it to bottom for the loop body eval. *)
             if not (restart_once && HM.mem restarted_wpoint y) then (
-              if tracing then trace "sol2" "wpoint restart %a ## %a" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ()));
+              if tracing then trace "sol2" "wpoint restart %a ## %a" S.Var.pp_trace y S.Dom.pp (HM.find_default rho y (S.Dom.bot ()));
               HM.replace rho y (S.Dom.bot ());
               if restart_once then (* avoid populating hashtable unnecessarily *)
                 HM.replace restarted_wpoint y ();
             )
           );
-          if tracing then trace "sol2" "eval adding wpoint %a from %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+          if tracing then trace "sol2" "eval adding wpoint %a from %a" S.Var.pp_trace y S.Var.pp_trace x;
           mark_wpoint y default_widen_gas;
         );
         let tmp = simple_solve l x y in
         if HM.mem rho y then add_infl y x;
-        if tracing then trace "sol2" "eval %a ## %a -> %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty tmp;
+        if tracing then trace "sol2" "eval %a ## %a -> %a" S.Var.pp_trace x S.Var.pp_trace y S.Dom.pp tmp;
         tmp
       and side ?x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *)
-        if tracing then trace "sol2" "side to %a (wpx: %a) from %a ## value: %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d;
+        if tracing then trace "sol2" "side to %a (wpx: %a) from %a ## value: %a" S.Var.pp_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pp_trace ())) x S.Dom.pp d;
         assert_can_receive_side y;
         init y;
 
         WPS.notify_side wps_data x y;
 
         let widen a b =
-          if M.tracing then M.traceli "sol2" "side widen %a %a" S.Dom.pretty a S.Dom.pretty b;
+          if M.tracing then M.traceli "sol2" "side widen %a %a" S.Dom.pp a S.Dom.pp b;
           let r = S.Dom.widen a (S.Dom.join a b) in
-          if M.tracing then M.traceu "sol2" "-> %a" S.Dom.pretty r;
+          if M.tracing then M.traceu "sol2" "-> %a" S.Dom.pp r;
           r
         in
         let old_sides = HM.find_default sides y VS.empty in
@@ -494,11 +494,11 @@ module Base =
         in
         let old = HM.find rho y in
         let tmp = op old d in
-        if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y;
+        if tracing then trace "sol2" "stable add %a" S.Var.pp_trace y;
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
-          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %a) from %a: %a -> %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp;
-          if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %a) from %a: %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old);
+          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %a) from %a: %a -> %a" S.Var.pp_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pp_trace ())) x S.Dom.pp old S.Dom.pp tmp;
+          if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %a) from %a: %a" S.Var.pp_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pp_trace ())) x S.Dom.pretty_diff (tmp, old);
 
           (match x with
            | Some x ->
@@ -515,7 +515,7 @@ module Base =
 
           (* make y a widening point if ... This will only matter for the next side _ y.  *)
           if WPS.should_mark_wpoint wps_data called old_sides x y destabilized_vs then (
-            if tracing then trace "sol2" "side adding wpoint %a from %a" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x;
+            if tracing then trace "sol2" "side adding wpoint %a from %a" S.Var.pp_trace y (Pretty.docOpt (S.Var.pp_trace ())) x;
             mark_wpoint y default_side_widen_gas
           );
 
@@ -523,7 +523,7 @@ module Base =
           if not vetoed_widen then reduce_gas y;
         )
       and demand l x y =
-        if tracing then trace "sol2" "demand weak dep %a from %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "sol2" "demand weak dep %a from %a" S.Var.pp_trace y S.Var.pp_trace x;
         match weak_deps_handling with
         | "none" -> ignore (eval l x y)
         | "eager" ->
@@ -533,7 +533,7 @@ module Base =
           HM.replace weak_dep x (VS.add y (try HM.find weak_dep x with Not_found -> VS.empty))
         | _ -> assert false
       and init x =
-        if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "init %a" S.Var.pp_trace x;
         if not (HM.mem rho x) then (
           new_var_event x;
           HM.replace rho x (S.Dom.bot ())
@@ -541,7 +541,7 @@ module Base =
       in
 
       let set_start (x,d) =
-        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         init x;
         UpdateRule.register_start update_rule_data x d;
         HM.replace rho x d;
@@ -550,11 +550,11 @@ module Base =
       in
 
       let rec destabilize_normal x =
-        if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x;
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y ->
-            if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y;
+            if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y;
             HM.remove stable y;
             HM.remove superstable y;
             Hooks.stable_remove y;
@@ -572,7 +572,7 @@ module Base =
       if GobConfig.get_bool "incremental.load" then (
 
         let restart_leaf x =
-          if tracing then trace "sol2" "Restarting to bot %a" S.Var.pretty_trace x;
+          if tracing then trace "sol2" "Restarting to bot %a" S.Var.pp_trace x;
           Logs.debug "Restarting to bot %a" S.Var.pretty_trace x;
           HM.replace rho x (S.Dom.bot ());
           (* HM.remove rho x; *)
@@ -592,7 +592,7 @@ module Base =
         (* destabilize which restarts side-effected vars *)
         (* side_fuel specifies how many times (in recursion depth) to destabilize side_infl, None means infinite *)
         let rec destabilize_with_side ~side_fuel x =
-          if tracing then trace "sol2" "destabilize_with_side %a %a" S.Var.pretty_trace x (Pretty.docOpt (Pretty.dprintf "%d")) side_fuel;
+          if tracing then trace "sol2" "destabilize_with_side %a %a" S.Var.pp_trace x (Pretty.docOpt (Pretty.dprintf "%d")) side_fuel;
 
           (* retrieve and remove (side-effect) dependencies/influences *)
           let w_side_dep = HM.find_default side_dep x VS.empty in
@@ -620,8 +620,8 @@ module Base =
 
             (* destabilize side dep to redo side effects *)
             VS.iter (fun y ->
-                if tracing then trace "sol2" "destabilize_with_side %a side_dep %a" S.Var.pretty_trace x S.Var.pretty_trace y;
-                if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y;
+                if tracing then trace "sol2" "destabilize_with_side %a side_dep %a" S.Var.pp_trace x S.Var.pp_trace y;
+                if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y;
                 HM.remove stable y;
                 HM.remove superstable y;
                 Hooks.stable_remove y;
@@ -631,8 +631,8 @@ module Base =
 
           (* destabilize eval infl *)
           VS.iter (fun y ->
-              if tracing then trace "sol2" "destabilize_with_side %a infl %a" S.Var.pretty_trace x S.Var.pretty_trace y;
-              if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y;
+              if tracing then trace "sol2" "destabilize_with_side %a infl %a" S.Var.pp_trace x S.Var.pp_trace y;
+              if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y;
               HM.remove stable y;
               HM.remove superstable y;
               Hooks.stable_remove y;
@@ -649,8 +649,8 @@ module Base =
             in
             (* TODO: should this also be conditional on restart_only_globals? right now goes through function entry side effects, but just doesn't restart them *)
             VS.iter (fun y ->
-                if tracing then trace "sol2" "destabilize_with_side %a side_infl %a" S.Var.pretty_trace x S.Var.pretty_trace y;
-                if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y;
+                if tracing then trace "sol2" "destabilize_with_side %a side_infl %a" S.Var.pp_trace x S.Var.pp_trace y;
+                if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y;
                 HM.remove stable y;
                 HM.remove superstable y;
                 Hooks.stable_remove y;
@@ -722,8 +722,8 @@ module Base =
               HM.remove side_dep x;
               (* destabilize side dep to redo side effects *)
               VS.iter (fun y ->
-                  if tracing then trace "sol2" "destabilize_leaf %a side_dep %a" S.Var.pretty_trace x S.Var.pretty_trace y;
-                  if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y;
+                  if tracing then trace "sol2" "destabilize_leaf %a side_dep %a" S.Var.pp_trace x S.Var.pp_trace y;
+                  if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y;
                   HM.remove stable y;
                   HM.remove superstable y;
                   Hooks.stable_remove y;
@@ -900,7 +900,7 @@ module Base =
         let restore () =
           let get x =
             let d = get ~check:true x in
-            if tracing then trace "sol2" "restored var %a ## %a" S.Var.pretty_trace x S.Dom.pretty d
+            if tracing then trace "sol2" "restored var %a ## %a" S.Var.pp_trace x S.Dom.pp d
           in
           List.iter get vs;
           HM.filteri_inplace (fun x _ -> HM.mem visited x) rho
@@ -1183,7 +1183,7 @@ module DepVals(UpdateRule: Td3UpdateRule.S): DemandEqIncrSolver =
             in
             match all_deps_unchanged with
             | Some oldv ->
-              if M.tracing then M.trace "sol2" "All deps unchanged for %a, not evaluating RHS" S.Var.pretty_trace x;
+              if M.tracing then M.trace "sol2" "All deps unchanged for %a, not evaluating RHS" S.Var.pp_trace x;
               oldv
             | None ->
               (* This needs to be done here as a local wrapper around get to avoid polluting dep_vals during earlier checks *)
diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml
index 873026660c..7ae7910a49 100644
--- a/src/solver/td3UpdateRule.ml
+++ b/src/solver/td3UpdateRule.ml
@@ -124,11 +124,11 @@ module Narrow:S =
               )
             ) new_acc;
         and divided_side (phase:divided_side_mode) x y d: bool =
-          if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d;
-          if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d;
+          if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pp_trace y S.Var.pp_trace x S.Dom.pp d;
+          if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pp_trace y S.Var.pp_trace x S.Dom.pp d;
           assert_can_receive_side y;
           init y;
-          if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y;
+          if tracing then trace "sol2" "stable add %a" S.Var.pp_trace y;
           HM.replace stable y ();
 
           let sided = GobOption.exists (VS.mem x) (HM.find_option sides y) in
@@ -169,7 +169,7 @@ module Narrow:S =
             in
 
             if not (S.Dom.equal old_side new_side) then (
-              if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty old_side S.Dom.pretty new_side;
+              if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pp_trace y S.Var.pp_trace x (show_divided_side_mode phase) S.Dom.pp old_side S.Dom.pp new_side;
 
               if S.Dom.is_bot new_side && narrow_gas = None then
                 HM.remove y_sides x
@@ -192,7 +192,7 @@ module Narrow:S =
               in
               if not (S.Dom.equal y_newval y_oldval) then (
                 if tracing then trace "side" "value of %a changed by side from %a (phase: %s) Old value: %a ## New value: %a"
-                    S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty y_oldval S.Dom.pretty y_newval;
+                    S.Var.pp_trace y S.Var.pp_trace x (show_divided_side_mode phase) S.Dom.pp y_oldval S.Dom.pp y_newval;
                 HM.replace rho y y_newval;
                 destabilize y;
               );
diff --git a/src/solver/td_simplified.ml b/src/solver/td_simplified.ml
index d2e8c93241..6a07915887 100644
--- a/src/solver/td_simplified.ml
+++ b/src/solver/td_simplified.ml
@@ -34,38 +34,38 @@ module Base : GenericEqSolver =
         );
 
       let add_infl y x =
-        if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "infl" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x;
         HM.replace infl y (VS.add x (HM.find_default infl y VS.empty));
       in
 
       let init x =
         if not (HM.mem rho x) then (
           new_var_event x;
-          if tracing then trace "init" "init %a" S.Var.pretty_trace x;
+          if tracing then trace "init" "init %a" S.Var.pp_trace x;
           HM.replace rho x (S.Dom.bot ())
         )
       in
 
       let eq x get set =
-        if tracing then trace "eq" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "eq" "eq %a" S.Var.pp_trace x;
         match S.system x with
         | None -> S.Dom.bot ()
         | Some f -> f get set
       in
 
       let rec destabilize x =
-        if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x;
+        if tracing then trace "destab" "destabilize %a" S.Var.pp_trace x;
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y ->
-            if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y;
+            if tracing then trace "destab" "stable remove %a" S.Var.pp_trace y;
             HM.remove stable y;
             destabilize y
           ) w
       in
 
       let rec query x y = (* ~eval in td3 *)
-        if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (HM.mem stable y) (HM.mem called y);
+        if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pp_trace y (HM.mem stable y) (HM.mem called y);
         get_var_event y;
         if not (HM.mem called y) then (
           if S.system y = None then (
@@ -77,20 +77,20 @@ module Base : GenericEqSolver =
             iterate y;
             HM.remove called y)
         ) else (
-          if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y;
+          if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pp_trace y;
           HM.replace wpoint y ();
         );
         let tmp = HM.find rho y in
         add_infl y x;
-        if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp;
+        if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pp_trace y S.Dom.pp tmp;
         tmp
 
       and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *)
-        if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pp_trace y (HM.mem wpoint y) S.Var.pp_trace x S.Dom.pp d;
         assert (S.system y = None);
         init y;
         let widen a b =
-          if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y;
+          if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pp_trace y;
           S.Dom.widen a (S.Dom.join a b)
         in
         let op a b = if HM.mem wpoint y then widen a b else S.Dom.join a b
@@ -99,16 +99,16 @@ module Base : GenericEqSolver =
         let tmp = op old d in
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
-          if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty tmp;
+          if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pp_trace y (HM.mem wpoint y) S.Var.pp_trace x S.Dom.pp tmp;
           HM.replace rho y tmp;
           destabilize y;
           (* make y a widening point. This will only matter for the next side _ y.  *)
-          if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y;
+          if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pp_trace y;
           HM.replace wpoint y ()
         )
 
       and iterate x = (* ~(inner) solve in td3*)
-        if tracing then trace "iter" "begin iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x);
+        if tracing then trace "iter" "begin iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x);
         init x;
         assert (S.system x <> None);
         if not (HM.mem stable x) then (
@@ -119,26 +119,26 @@ module Base : GenericEqSolver =
           let wpd = (* d after widen/narrow (if wp) *)
             if not wp then eqd
             else (
-              if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
+              if M.tracing then M.trace "wpoint" "widen %a" S.Var.pp_trace x;
               box old eqd)
           in
           if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
             (* old != wpd *)
-            if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old);
+            if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pp_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
             HM.replace  rho x wpd;
             destabilize x;
-            if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x;
+            if tracing then trace "iter" "iterate changed %a" S.Var.pp_trace x;
             (iterate[@tailcall]) x
           ) else (
             (* old == wpd *)
             if not (HM.mem stable x) then (
               (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
-              if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
+              if tracing then trace "iter" "iterate still unstable %a" S.Var.pp_trace x;
               (iterate[@tailcall]) x
             ) else (
               (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *)
-              if tracing && (HM.mem wpoint x) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x;
+              if tracing && (HM.mem wpoint x) then trace "wpoint" "iterate removing wpoint %a" S.Var.pp_trace x;
               HM.remove wpoint x
             )
           )
@@ -171,7 +171,7 @@ module Base : GenericEqSolver =
             flush_all ();
           );
           List.iter (fun x -> HM.replace called x ();
-                      if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
+                      if tracing then trace "multivar" "solving for %a" S.Var.pp_trace x;
                       iterate x;
                       HM.remove called x
                     ) unstable_vs;
diff --git a/src/solver/td_simplified_ref.ml b/src/solver/td_simplified_ref.ml
index 2968dc1b84..57ebe9b637 100644
--- a/src/solver/td_simplified_ref.ml
+++ b/src/solver/td_simplified_ref.ml
@@ -33,7 +33,7 @@ module Base : GenericEqSolver =
         );
 
       let add_infl y x =
-        if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "infl" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x;
         let y_ref = HM.find data y in
         y_ref := { !y_ref with infl = VS.add x !y_ref.infl }
       in
@@ -45,7 +45,7 @@ module Base : GenericEqSolver =
         | None ->
           begin
             new_var_event x;
-            if tracing then trace "init" "init %a" S.Var.pretty_trace x;
+            if tracing then trace "init" "init %a" S.Var.pp_trace x;
             let data_x = ref {
                 infl = VS.empty;
                 value = S.Dom.bot ();
@@ -59,19 +59,19 @@ module Base : GenericEqSolver =
       in
 
       let eq x get set =
-        if tracing then trace "eq" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "eq" "eq %a" S.Var.pp_trace x;
         match S.system x with
         | None -> S.Dom.bot ()
         | Some f -> f get set
       in
 
       let rec destabilize x =
-        if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x;
+        if tracing then trace "destab" "destabilize %a" S.Var.pp_trace x;
         let x_ref = HM.find data x in
         let w = !x_ref.infl in
         x_ref := { !x_ref with infl = VS.empty };
         VS.iter (fun y ->
-            if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y;
+            if tracing then trace "destab" "stable remove %a" S.Var.pp_trace y;
             let y_ref = HM.find data y in
             y_ref := { !y_ref with stable = false };
             destabilize y
@@ -80,7 +80,7 @@ module Base : GenericEqSolver =
 
       let rec query x y =
         let y_ref = init y in
-        if tracing then trace "sol_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (!y_ref.stable) (!y_ref.called);
+        if tracing then trace "sol_query" "entering query for %a; stable %b; called %b" S.Var.pp_trace y (!y_ref.stable) (!y_ref.called);
         get_var_event y;
         if not (!y_ref.called) then (
           if S.system y = None then (
@@ -91,20 +91,20 @@ module Base : GenericEqSolver =
             iterate y;
             y_ref := { !y_ref with called = false };)
         ) else (
-          if tracing && not (!y_ref.wpoint) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y;
+          if tracing && not (!y_ref.wpoint) then trace "wpoint" "query adding wpoint %a" S.Var.pp_trace y;
           y_ref := { !y_ref with wpoint = true };
         );
         let tmp = !y_ref.value in
         add_infl y x;
-        if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp;
+        if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pp_trace y S.Dom.pp tmp;
         tmp
 
       and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *)
         assert (S.system y = None);
         let y_ref = init y in
-        if tracing then trace "side" "side to %a (wpx: %b) from %a ## value: %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "side" "side to %a (wpx: %b) from %a ## value: %a" S.Var.pp_trace y (!y_ref.wpoint) S.Var.pp_trace x S.Dom.pp d;
         let widen a b =
-          if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y;
+          if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pp_trace y;
           S.Dom.widen a (S.Dom.join a b)
         in
         let op a b = if !y_ref.wpoint then widen a b else S.Dom.join a b
@@ -113,11 +113,11 @@ module Base : GenericEqSolver =
         let tmp = op old d in
         y_ref := { !y_ref with stable = true };
         if not (S.Dom.leq tmp old) then (
-          if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a: %a -> %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp;
+          if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a: %a -> %a" S.Var.pp_trace y (!y_ref.wpoint) S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp;
           y_ref := { !y_ref with value = tmp };
           destabilize y;
           (* make y a widening point. This will only matter for the next side _ y.  *)
-          if tracing && not (!y_ref.wpoint) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y;
+          if tracing && not (!y_ref.wpoint) then trace "wpoint" "side adding wpoint %a" S.Var.pp_trace y;
           y_ref := { !y_ref with wpoint = true };
         )
 
@@ -125,7 +125,7 @@ module Base : GenericEqSolver =
 
         (* beginning of iterate*)
         let x_ref = init x in
-        if tracing then trace "iter" "iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (!x_ref.called) (!x_ref.stable) (!x_ref.wpoint);
+        if tracing then trace "iter" "iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pp_trace x (!x_ref.called) (!x_ref.stable) (!x_ref.wpoint);
         assert (S.system x <> None);
         if not (!x_ref.stable) then (
           x_ref := { !x_ref with stable = true };
@@ -135,26 +135,26 @@ module Base : GenericEqSolver =
           let wpd = (* d after widen/narrow (if wp) *)
             if not wp then eqd
             else (
-              if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
+              if M.tracing then M.trace "wpoint" "widen %a" S.Var.pp_trace x;
               box old eqd)
           in
           if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
             (* old != wpd *)
-            if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old);
+            if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pp_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
             x_ref := { !x_ref with value = wpd };
             destabilize x;
-            if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x;
+            if tracing then trace "iter" "iterate changed %a" S.Var.pp_trace x;
             (iterate[@tailcall]) x
           ) else (
             (* old == wpd *)
             if not (!x_ref.stable) then (
               (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
-              if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
+              if tracing then trace "iter" "iterate still unstable %a" S.Var.pp_trace x;
               (iterate[@tailcall]) x
             ) else (
               (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *)
-              if tracing && (!x_ref.wpoint) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x;
+              if tracing && (!x_ref.wpoint) then trace "wpoint" "iterate removing wpoint %a" S.Var.pp_trace x;
               x_ref := { !x_ref with wpoint = false };
             )
           )
@@ -188,7 +188,7 @@ module Base : GenericEqSolver =
           List.iter (fun x ->
               let x_ref = HM.find data x in
               x_ref := { !x_ref with called = true };
-              if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
+              if tracing then trace "multivar" "solving for %a" S.Var.pp_trace x;
               iterate x;
               x_ref := { !x_ref with called = false }
             ) unstable_vs;
diff --git a/src/solver/topDown.ml b/src/solver/topDown.ml
index f71481ff40..00da73ae34 100644
--- a/src/solver/topDown.ml
+++ b/src/solver/topDown.ml
@@ -32,7 +32,7 @@ module WP =
       let wpoint = HM.create  10 in
 
       let add_infl y x =
-        if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x;
         HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty))
       in
       let add_set x y d =
@@ -42,15 +42,15 @@ module WP =
       in
       let is_side x = HM.mem set x in
       let rec destabilize x =
-        (* if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x; *)
+        (* if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x; *)
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y ->
           HM.remove stable y;
-          if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace y;
+          if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace y;
           if not (HM.mem called y) then destabilize y) w
       and solve x =
-        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x);
+        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x);
         if not (HM.mem called x || HM.mem stable x) then (
           HM.replace stable x ();
           HM.replace called x ();
@@ -59,22 +59,22 @@ module WP =
           let old = HM.find rho x in
           let tmp' = eq x (eval x) (side x) in
           let tmp = S.Dom.join tmp' (sides x) in
-          if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-          if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
+          if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+          if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp;
           let tmp = if is_side x then S.Dom.widen old (S.Dom.join old tmp) else if wpx then box old tmp else tmp in
           HM.remove called x;
           if not (S.Dom.equal old tmp) then (
-            if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty (S.Dom.widen old (S.Dom.join old tmp));
+            if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pp old S.Dom.pp tmp S.Dom.pp (S.Dom.widen old (S.Dom.join old tmp));
             update_var_event x old tmp;
-            if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
-            if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x (HM.mem rho x) (is_side x) S.Dom.pretty tmp S.Dom.pretty old;
+            if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp;
+            if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x (HM.mem rho x) (is_side x) S.Dom.pp tmp S.Dom.pp old;
             HM.replace rho x tmp;
             destabilize x;
           );
           (solve[@tailcall]) x
         )
       and eq x get set =
-        if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "eq %a" S.Var.pp_trace x;
         eval_rhs_event x;
         match S.system x with
         | None -> S.Dom.bot ()
@@ -89,7 +89,7 @@ module WP =
           in
           f get sidef
       and eval x y =
-        if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y;
+        if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y;
         get_var_event y;
         if HM.mem called y || S.system y = None then HM.replace wpoint y ();
         solve y;
@@ -97,11 +97,11 @@ module WP =
         HM.find rho y
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
-        let d = VS.fold (fun y d -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty r; r) w (S.Dom.bot ()) in
-        if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        let d = VS.fold (fun y d -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pp_trace x S.Var.pp_trace y S.Dom.pp r; r) w (S.Dom.bot ()) in
+        if tracing then trace "sol2" "sides %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         d
       and side x y d =
-        if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pretty_trace x S.Var.pretty_trace y (HM.mem rho y) S.Dom.pretty d;
+        if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pp_trace x S.Var.pp_trace y (HM.mem rho y) S.Dom.pp d;
         let old = try HPM.find rho' (x,y) with Not_found -> S.Dom.bot () in
         if not (S.Dom.equal old d) then (
           add_set x y (S.Dom.join old d);
@@ -109,7 +109,7 @@ module WP =
           solve y;
         )
       and init x =
-        if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "init %a" S.Var.pp_trace x;
         if not (HM.mem rho x) then (
           new_var_event x;
           HM.replace rho  x (S.Dom.bot ())
@@ -117,7 +117,7 @@ module WP =
       in
 
       let set_start (x,d) =
-        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         init x;
         add_set x x d;
         solve x
diff --git a/src/solver/topDown_deprecated.ml b/src/solver/topDown_deprecated.ml
index 8d7ad781b2..61f270959c 100644
--- a/src/solver/topDown_deprecated.ml
+++ b/src/solver/topDown_deprecated.ml
@@ -36,16 +36,16 @@ module TD3 =
       let add_set x y d = HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty)); HPM.add rho' (x,y) d; HM.add sidevs y () in
       let is_side x = HM.mem set x in
       let make_wpoint x =
-        if tracing then trace "sol2" "make_wpoint %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "make_wpoint %a" S.Var.pp_trace x;
         HM.replace wpoint x ()
       in
       let rec destabilize x =
-        if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x;
         let t = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y -> HM.remove stable y; if not (HM.mem called y) then destabilize y) t
       and solve x =
-        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x);
+        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x);
         if not (HM.mem called x || HM.mem stable x) then begin
           HM.replace called x ();
           let wpx = HM.mem wpoint x in
@@ -54,21 +54,21 @@ module TD3 =
           let old = HM.find rho x in
           let tmp = eq x (eval x) (side x) in
           let tmp = S.Dom.join tmp (sides x) in
-          if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-          if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
+          if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+          if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp;
           let tmp = if is_side x then S.Dom.widen old (S.Dom.join old tmp) else if wpx then box old tmp else tmp in
           HM.remove called x;
           if not (S.Dom.equal old tmp) then begin
             update_var_event x old tmp;
-            if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
-            if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x wpx (is_side x) S.Dom.pretty tmp S.Dom.pretty old;
+            if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp;
+            if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x wpx (is_side x) S.Dom.pp tmp S.Dom.pp old;
             HM.replace rho x tmp;
             destabilize x;
             (solve[@tailcall]) x;
           end;
         end;
       and eq x get set =
-        if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "eq %a" S.Var.pp_trace x;
         eval_rhs_event x;
         match S.system x with
         | None -> S.Dom.bot ()
@@ -83,7 +83,7 @@ module TD3 =
           in
           f get sidef
       and eval x y =
-        if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y;
+        if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y;
         get_var_event y;
         if not (HM.mem rho y) then init y;
         if HM.mem called y then make_wpoint y else if neg is_side y then solve y;
@@ -92,11 +92,11 @@ module TD3 =
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let d = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
-        if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "sol2" "sides %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         d
       and side x y d =
         if S.Dom.is_bot d then () else
-        if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pretty_trace x S.Var.pretty_trace y (HM.mem wpoint y) S.Dom.pretty d;
+        if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pp_trace x S.Var.pp_trace y (HM.mem wpoint y) S.Dom.pp d;
         if not (HM.mem rho y) then begin
           init y;
           add_set x y d;
@@ -113,7 +113,7 @@ module TD3 =
           end
         end
       and init x =
-        if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "init %a" S.Var.pp_trace x;
         if not (HM.mem rho x) then begin
           new_var_event x;
           HM.replace rho  x (S.Dom.bot ());
@@ -122,7 +122,7 @@ module TD3 =
       in
 
       let set_start (x,d) =
-        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         init x;
         add_set x x d;
         solve x
diff --git a/src/solver/topDown_space_cache_term.ml b/src/solver/topDown_space_cache_term.ml
index 56f089156c..313519ad7f 100644
--- a/src/solver/topDown_space_cache_term.ml
+++ b/src/solver/topDown_space_cache_term.ml
@@ -29,16 +29,16 @@ module WP =
       let cache_sizes = ref [] in
 
       let add_infl y x =
-        if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x;
         HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty))
       in
       let rec destabilize x =
-        if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x;
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y -> HM.remove stable y; if not (HM.mem called y) then destabilize y) w
       and solve x phase =
-        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x);
+        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x);
         if not (HM.mem called x || HM.mem stable x) then (
           HM.replace stable x ();
           HM.replace called x ();
@@ -46,17 +46,17 @@ module WP =
           let l = HM.create 10 in
           let tmp = eq x (eval l x) (side l) in
           let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> S.Dom.bot ()) in
-          if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-          if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
+          if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+          if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp;
           HM.remove called x;
           let tmp = match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow -> S.Dom.narrow old tmp in
-          if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pretty_trace x;
+          if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pp_trace x;
           cache_sizes := HM.length l :: !cache_sizes;
           if not (S.Dom.equal old tmp) then (
-            (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty (S.Dom.widen old (S.Dom.join old tmp)); *)
+            (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pp old S.Dom.pp tmp S.Dom.pp (S.Dom.widen old (S.Dom.join old tmp)); *)
             update_var_event x old tmp;
-            if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
-            (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x (HM.mem rho x) (is_side x) S.Dom.pretty tmp S.Dom.pretty old; *)
+            if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp;
+            (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x (HM.mem rho x) (is_side x) S.Dom.pp tmp S.Dom.pp old; *)
             HM.replace rho x tmp;
             destabilize x;
             (solve[@tailcall]) x phase;
@@ -68,13 +68,13 @@ module WP =
           );
         )
       and eq x get set =
-        if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "eq %a" S.Var.pp_trace x;
         eval_rhs_event x;
         match S.system x with
         | None -> S.Dom.bot ()
         | Some f -> f get set
       and simple_solve l x y =
-        if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pretty_trace y (S.system y <> None);
+        if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pp_trace y (S.system y <> None);
         if S.system y = None then init y;
         if HM.mem rho y then (solve y Widen; HM.find rho y) else
         if HM.mem called y then (init y; HM.remove l y; HM.find rho y) else
@@ -87,13 +87,13 @@ module WP =
           else (HM.replace l y tmp; tmp)
         )
       and eval l x y =
-        if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y;
+        if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y;
         get_var_event y;
         let tmp = simple_solve l x y in
         if HM.mem rho y then add_infl y x;
         tmp
       and side l y d =
-        if tracing then trace "sol2" "side to %a (wpx: %b) ## value: %a" S.Var.pretty_trace y (HM.mem rho y) S.Dom.pretty d;
+        if tracing then trace "sol2" "side to %a (wpx: %b) ## value: %a" S.Var.pp_trace y (HM.mem rho y) S.Dom.pp d;
         let old = try HM.find rho' y with Not_found -> S.Dom.bot () in
         if not (S.Dom.leq d old) then (
           HM.replace rho' y (S.Dom.join old d);
@@ -103,7 +103,7 @@ module WP =
           solve y Widen;
         )
       and init x =
-        if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "init %a" S.Var.pp_trace x;
         if not (HM.mem rho x) then (
           new_var_event x;
           HM.replace rho  x (S.Dom.bot ())
@@ -111,7 +111,7 @@ module WP =
       in
 
       let set_start (x,d) =
-        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         init x;
         HM.replace rho x d;
         HM.replace rho' x d;
@@ -175,7 +175,7 @@ module WP =
         let restore () =
           let get x =
             let d = get x in
-            if tracing then trace "sol2" "restored var %a ## %a" S.Var.pretty_trace x S.Dom.pretty d
+            if tracing then trace "sol2" "restored var %a ## %a" S.Var.pp_trace x S.Dom.pp d
           in
           List.iter get vs
         in
diff --git a/src/solver/topDown_term.ml b/src/solver/topDown_term.ml
index 3a67cda982..82b87dfd3e 100644
--- a/src/solver/topDown_term.ml
+++ b/src/solver/topDown_term.ml
@@ -29,19 +29,19 @@ module WP =
       let wpoint = HM.create  10 in
 
       let add_infl y x =
-        if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+        if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x;
         HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty))
       in
       let rec destabilize x =
-        if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x;
         let w = HM.find_default infl x VS.empty in
         HM.replace infl x VS.empty;
         VS.iter (fun y ->
           HM.remove stable y;
-          (* if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace y; *)
+          (* if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace y; *)
           if not (HM.mem called y) then destabilize y) w
       and solve x phase =
-        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x);
+        if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x);
         if not (HM.mem called x || HM.mem stable x) then (
           HM.replace stable x ();
           HM.replace called x ();
@@ -50,15 +50,15 @@ module WP =
           let old = HM.find rho x in
           let tmp = eq x (eval x) side in
           let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> S.Dom.bot ()) in
-          if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
-          if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
+          if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ;
+          if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp;
           HM.remove called x;
           let tmp = if wpx then match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow -> S.Dom.narrow old tmp else tmp in
           if not (S.Dom.equal old tmp) then (
-            (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty (S.Dom.widen old (S.Dom.join old tmp)); *)
+            (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pp old S.Dom.pp tmp S.Dom.pp (S.Dom.widen old (S.Dom.join old tmp)); *)
             update_var_event x old tmp;
-            if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
-            (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x (HM.mem rho x) (is_side x) S.Dom.pretty tmp S.Dom.pretty old; *)
+            if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp;
+            (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x (HM.mem rho x) (is_side x) S.Dom.pp tmp S.Dom.pp old; *)
             HM.replace rho x tmp;
             destabilize x;
             (solve[@tailcall]) x phase;
@@ -70,13 +70,13 @@ module WP =
           );
         )
       and eq x get set =
-        if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "eq %a" S.Var.pp_trace x;
         eval_rhs_event x;
         match S.system x with
         | None -> S.Dom.bot ()
         | Some f -> f get set
       and eval x y =
-        if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y;
+        if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y;
         get_var_event y;
         if HM.mem called y then HM.replace wpoint y ();
         solve y Widen;
@@ -91,7 +91,7 @@ module WP =
           solve y Widen;
         )
       and init x =
-        if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
+        if tracing then trace "sol2" "init %a" S.Var.pp_trace x;
         if not (HM.mem rho x) then (
           new_var_event x;
           HM.replace rho  x (S.Dom.bot ())
@@ -99,7 +99,7 @@ module WP =
       in
 
       let set_start (x,d) =
-        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
+        if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d;
         init x;
         HM.replace rho' x d;
         solve x Widen
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 4dee3a62c8..86f807eb8a 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -408,7 +408,7 @@ class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object
       (* this makes new physical copy*)
       let new_s = {sn with labels = new_labels} in
       CopyOfHashTable.replace copyof new_s s;
-      if M.tracing then M.trace "cfg" "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s;
+      if M.tracing then M.trace "cfg" "Marking %a as copy of %a" CilType.Stmt.pp new_s CilType.Stmt.pp s;
       if new_s.labels <> [] then
         (* Use original s, ns might be temporay e.g. if the type of statement changed *)
         (* record that goto s; appearing in the current fragment should later be patched to goto new_s *)
diff --git a/src/util/std/gobFpath.ml b/src/util/std/gobFpath.ml
index 9b6523030c..93b62e3ab8 100644
--- a/src/util/std/gobFpath.ml
+++ b/src/util/std/gobFpath.ml
@@ -4,6 +4,8 @@ let hash p = Hashtbl.hash (Fpath.to_string p)
 
 let pretty () p = GoblintCil.Pretty.text (Fpath.to_string p)
 
+let pp ppf p = Format.pp_print_string ppf (Fpath.to_string p)
+
 let to_yojson p = `String (Fpath.to_string p)
 
 let of_yojson = function
diff --git a/src/util/std/gobYojson.ml b/src/util/std/gobYojson.ml
index 72d5f0b0e2..2def7dd61c 100644
--- a/src/util/std/gobYojson.ml
+++ b/src/util/std/gobYojson.ml
@@ -30,3 +30,5 @@ let print (ch: 'a BatIO.output) json =
 
 let pretty () json =
   GoblintCil.Pretty.text (Yojson.Safe.to_string json)
+
+let pp ppf json = Format.pp_print_string ppf (Yojson.Safe.to_string json)
diff --git a/src/util/tracing/goblint_tracing.ml b/src/util/tracing/goblint_tracing.ml
index f62ec3ee38..52c4ba6b75 100644
--- a/src/util/tracing/goblint_tracing.ml
+++ b/src/util/tracing/goblint_tracing.ml
@@ -7,7 +7,6 @@
 open Goblint_std
 open Goblint_parallel
 open GoblintCil
-open Pretty
 
 module Strs = Set.Make (String)
 
@@ -35,16 +34,15 @@ let indent_level = ref 0
 let traceIndent () = indent_level := !indent_level + 2
 let traceOutdent () = indent_level := !indent_level - 2
 
-let traceTag (sys : string) : Pretty.doc =
+let traceTag (sys : string) : string =
   let rec ind (i : int) : string = if (i <= 0) then "" else " " ^ (ind (i-1)) in
-  (text ((ind !indent_level) ^ "%%% " ^ sys ^ ": "))
+  (ind !indent_level) ^ "%%% " ^ sys ^ ": "
 
 let trace_mutex = GobMutex.create ()
 
-let printtrace sys d: unit =
+let printtrace sys (s: string): unit =
   GobMutex.lock trace_mutex;
-  fprint stderr ~width:max_int ((traceTag sys) ++ d ++ line);
-  flush stderr;
+  Printf.eprintf "%s%s\n%!" (traceTag sys) s;
   GobMutex.unlock trace_mutex
 
 let gtrace always f sys var ?loc do_subsys fmt =
@@ -60,9 +58,14 @@ let gtrace always f sys var ?loc do_subsys fmt =
   in
   if cond then begin
     do_subsys ();
-    gprintf (f sys) fmt
+    let buf = Buffer.create 64 in
+    let ppf = Format.formatter_of_buffer buf in
+    Format.kfprintf (fun ppf ->
+        Format.pp_print_flush ppf ();
+        f sys (Buffer.contents buf)
+      ) ppf fmt
   end else
-    GobPretty.igprintf () fmt
+    Format.ifprintf Format.err_formatter fmt
 
 let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt
 
@@ -74,13 +77,13 @@ let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt
 *)
 
 let tracei (sys:string) ?var ?(subsys=[]) fmt =
-  let f sys d = printtrace sys d; traceIndent () in
+  let f sys s = printtrace sys s; traceIndent () in
   let g () = activate sys subsys in
   gtrace true f sys var g fmt
 
 let tracec sys fmt = gtrace false printtrace sys None ignore fmt
 
 let traceu sys fmt =
-  let f sys d = printtrace sys d; traceOutdent () in
+  let f sys s = printtrace sys s; traceOutdent () in
   let g () = deactivate sys in
   gtrace true f sys None g fmt