diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml
index 9fb56d1f..9c9e6145 100644
--- a/src/smt/Congruence_closure.ml
+++ b/src/smt/Congruence_closure.ml
@@ -606,15 +606,15 @@ let mk_model (cc:t) (m:Model.t) : Model.t =
   Model.add_funs funs m
 
 let pp_full out (cc:t) : unit =
+  let pp_next out n =
+    if n==n.n_root then Fmt.string out " :is-root"
+    else Fmt.fprintf out "@ :next %a" N.pp n.n_root in
+  let pp_root out n =
+    let u = find cc n in if n==u||n.n_root==u then () else Fmt.fprintf out "@ :root %a" N.pp u in
   let pp_n out n =
-    let pp_next out n =
-      if n==n.n_root then Fmt.string out " :is-root"
-      else Fmt.fprintf out "@ :next %a" N.pp n.n_root in
-    let pp_root out n =
-      let u = find cc n in if n==u||n.n_root==u then () else Fmt.fprintf out "@ :root %a" N.pp u in
     Fmt.fprintf out "(@[%a%a%a@])" Term.pp n.n_term pp_next n pp_root n
   and pp_sig_e out (s,n) =
-    Fmt.fprintf out "(@[<1>%a@ -> %a@])" Signature.pp s N.pp n
+    Fmt.fprintf out "(@[<1>%a@ -> %a%a%a@])" Signature.pp s N.pp n pp_next n pp_root n
   in
   Fmt.fprintf out
     "(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])"