diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index ffe5cb104f..d15884e697 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -312,10 +312,19 @@ module SmtlibCounterExample = struct
     | [Ty.Trecord _r, _arg] -> begin
         match xs_values with
         | [record_name,_] ->
+          (* HOTFIX: this fix is temporary. The current implementation of
+             model generation for records relies on string representants,
+             which means the printer for access symbols has to agree with
+             the name of the field in the type trecord. As the printer
+             [Symbols.print] will always output AE native format, this
+             doesn't agree when the output format is SMT-LIB. But the
+             printer of expression will output the right string if we don't
+             give the arguments of the field. *)
+          let access = Fmt.str "%a" Expr.print (Expr.mk_term f [] ty) in
           add_records_destr
             records
             (asprintf "%a" Expr.print record_name)
-            (Sy.to_string f)
+            access
             rep
         | [] | _ -> records
       end
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 74cecdd1ca..cdf6deecea 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -311,393 +311,374 @@ module F_Htbl : Hashtbl.S with type key = t =
 
 (** pretty printing *)
 
-let print_binders =
-  let print_one fmt (sy, (ty, _)) =
-    Format.fprintf fmt "%a:%a" Sy.print sy Ty.print ty
-  in fun fmt b ->
-    match SMap.bindings b with
-    | [] ->
-      (* can happen when quantifying only on type variables *)
-      Format.fprintf fmt "(no term variables)"
-    | e::l ->
-      print_one fmt e;
-      List.iter (fun e -> Format.fprintf fmt ", %a" print_one e) l
-
-(* let print_list_sep sep pp fmt =
- *   Format.pp_print_list ~pp_sep:(fun fmt _ -> Format.fprintf fmt sep) pp fmt
- *
- * let print_list pp fmt = print_list_sep "," pp fmt *)
-
 module SmtPrinter = struct
+  let pp_binder ppf (var, (ty, _)) =
+    let var =
+      match var with
+      | Sy.Var v -> v
+      | _ -> assert false
+    in
+    Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty
 
-  let rec print_formula fmt form xs bind =
-    let open Format in
+  let pp_binders = Fmt.(iter_bindings ~sep:sp SMap.iter pp_binder)
+
+  let rec pp_formula ppf form xs bind =
     match form, xs, bind with
     | Sy.F_Unit _, [f1; f2], _ ->
-      Format.fprintf fmt "@[(and %a %a)@]" print_silent f1 print_silent f2
+      Fmt.pf ppf "@[(and %a %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Iff, [f1; f2], _ ->
-      fprintf fmt "@[(= %a %a)@]" print_silent f1 print_silent f2
+      Fmt.pf ppf "@[(= %a %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Xor, [f1; f2], _ ->
-      fprintf fmt "@[(not (= %a %a))@]" print_silent f1 print_silent f2
+      Fmt.pf ppf "@[(xor %a %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Clause _, [f1; f2], _ ->
-      fprintf fmt "@[(or %a %a)@]" print_silent f1 print_silent f2
+      Fmt.pf ppf "@[(or %a %a)@]" pp_silent f1 pp_silent f2
 
-    | Sy.F_Lemma, [], B_lemma { user_trs ; main ; name ; binders; _ } ->
-      if Options.get_verbose () then
-        fprintf fmt "(lemma: %s forall %a[%a].@  %a)"
-          name
-          print_binders binders
-          print_triggers user_trs
-          print_silent main
-      else
-        fprintf fmt "(lem %s)" name
+    | Sy.F_Lemma, [], B_lemma { main; name; binders; _ } ->
+      Fmt.pf ppf "(! (forall (%a) %a) :named %s)"
+        pp_binders binders pp_silent main name
 
-    | Sy.F_Skolem, [], B_skolem { main; binders; _ } ->
-      fprintf fmt "(<sko exists %a.> %a)"
-        print_binders binders print_silent main
+    | Sy.F_Skolem, [], B_skolem { main; name; binders; _ } ->
+      Fmt.pf ppf "(! (exists (%a) %a) :named %s)"
+        pp_binders binders pp_silent main name
 
     | _ -> assert false
 
-  and print_lit fmt lit xs =
-    let open Format in
+  and pp_lit ppf lit xs =
     match lit, xs with
     | Sy.L_eq, a::l ->
-      fprintf fmt "(= %a%a)"
-        print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l
+      Fmt.pf ppf "(= %a %a)"
+        pp a (fun ppf -> List.iter (Fmt.pf ppf " %a" pp)) l
+
     | Sy.L_neg_eq, [a; b] ->
-      fprintf fmt "(not (= %a %a))" print a print b
+      Fmt.pf ppf "(not (= %a %a))" pp a pp b
 
-    | Sy.L_neg_eq, a::l ->
-      fprintf fmt "(distinct %a%a)"
-        print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l
+    | Sy.L_neg_eq, _ :: _ ->
+      Fmt.pf ppf "(distinct %a)" Fmt.(list ~sep:sp pp) xs
 
     | Sy.L_built Sy.LE, [a;b] ->
-      fprintf fmt "(<= %a %a)" print a print b
+      Fmt.pf ppf "(<= %a %a)" pp a pp b
 
     | Sy.L_built Sy.LT, [a;b] ->
-      fprintf fmt "(< %a %a)" print a print b
+      Fmt.pf ppf "(< %a %a)" pp a pp b
 
     | Sy.L_neg_built Sy.LE, [a; b] ->
-      fprintf fmt "(> %a %a)" print a print b
+      Fmt.pf ppf "(> %a %a)" pp a pp b
 
     | Sy.L_neg_built Sy.LT, [a; b] ->
-      fprintf fmt "(>= %a %a)" print a print b
+      Fmt.pf ppf "(>= %a %a)" pp a pp b
 
     | Sy.L_neg_pred, [a] ->
-      fprintf fmt "(not %a)" print a
+      Fmt.pf ppf "(not %a)" pp a
 
     | Sy.L_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "((_ is %a) %a)" Hstring.print hs print e
+      Fmt.pf ppf "((_ is %a) %a)" Hstring.print hs pp e
 
     | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e
+      Fmt.pf ppf "(not ((_ is %a) %a))" Hstring.print hs pp e
 
     | (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
       | Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
       | Sy.L_built (Sy.IsConstr _)
-      | Sy.L_neg_built (Sy.IsConstr _)) , _ ->
+      | Sy.L_neg_built (Sy.IsConstr _)), _ ->
       assert false
 
-  and print_silent fmt t =
-    let open Format in
+  and pp_operator = Symbols.pp_operator ~format:`Smtlib
+
+  and pp_silent ppf t =
     let { f ; xs ; ty; bind; _ } = t in
     match f, xs with
-    (* Formulas *)
-    | Sy.Form form, xs -> print_formula fmt form xs bind
+    | Sy.Form form, xs -> pp_formula ppf form xs bind
+
+    | Sy.Lit lit, xs -> pp_lit ppf lit xs
 
     | Sy.Let, [] ->
       let x = match bind with B_let x -> x | _ -> assert false in
-      fprintf fmt
-        "(let%a %a =@ %a in@ %a)"
-        (fun fmt x -> if Options.get_verbose () then
-            fprintf fmt
-              " [sko = %a]" print x.let_sko) x
-        Sy.print x.let_v print x.let_e print_silent x.in_e
+      Fmt.pf ppf "(let ((%a %a)) %a)"
+        Symbols.print x.let_v
+        pp x.let_e
+        pp_silent x.in_e
 
-    (* Literals *)
-    | Sy.Lit lit, xs -> print_lit fmt lit xs
+    | Sy.(Op Record), _ ->
+      begin
+        match ty with
+        | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } ->
+          assert (List.compare_lengths xs lbs = 0);
+          Fmt.pf ppf "(%a %a)"
+            Hstring.print record_constr
+            Fmt.(list ~sep:sp pp) xs
 
-    | Sy.Op Sy.Get, [e1; e2] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(select %a %a)" print e1 print e2
-      else
-        fprintf fmt "%a[%a]" print e1 print e2
-
-    | Sy.Op Sy.Set, [e1; e2; e3] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(store %a %a %a)"
-          print e1
-          print e2
-          print e3
-      else
-        fprintf fmt "%a[%a<-%a]" print e1 print e2 print e3
+        | _ ->
+          (* Exclude by the typechecker. *)
+          assert false
+      end
 
-    | Sy.Op Sy.Concat, [e1; e2] ->
-      fprintf fmt "%a@@%a" print e1 print e2
+    | Sy.Op op, [] -> Fmt.pf ppf "%a" pp_operator op
 
-    | Sy.Op Sy.Extract (i, j), [e] ->
-      fprintf fmt "%a^{%d,%d}" print e i j
+    | Sy.Op op, _ :: _ ->
+      Fmt.pf ppf "(%a %a)" pp_operator op Fmt.(list ~sep:sp pp) xs
 
-    | Sy.Op (Sy.Access field), [e] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(%s %a)" (Hstring.view field) print e
-      else
-        fprintf fmt "%a.%s" print e (Hstring.view field)
+    | Sy.True, [] -> Fmt.pf ppf "true"
 
-    | Sy.Op (Sy.Record), _ ->
-      begin match ty with
-        | Ty.Trecord { Ty.lbs = lbs; _ } ->
-          assert (List.length xs = List.length lbs);
-          fprintf fmt "{";
-          ignore (List.fold_left2 (fun first (field,_) e ->
-              fprintf fmt "%s%s = %a"  (if first then "" else "; ")
-                (Hstring.view field) print e;
-              false
-            ) true lbs xs);
-          fprintf fmt "}";
-        | _ -> assert false
-      end
+    | Sy.False, [] -> Fmt.pf ppf "false"
 
-    (* TODO: introduce PrefixOp in the future to simplify this ? *)
-    | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round ||
-                              op == Sy.Max_real || op == Sy.Max_int ||
-                              op == Sy.Min_real || op == Sy.Min_int ->
-      fprintf fmt "%a(%a,%a)" Sy.print f print e1 print e2
+    | Sy.Name (n, _, _), [] -> Symbols.pp_name ppf (Hstring.view n)
 
-    (* TODO: introduce PrefixOp in the future to simplify this ? *)
-    | Sy.Op (Sy.Constr hs), ((_::_) as l) ->
-      fprintf fmt
-        "%a(%a)" Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l
+    | Sy.Name (n, _, _), _ :: _ ->
+      Fmt.pf ppf "(%a %a)"
+        Symbols.pp_name (Hstring.view n)
+        Fmt.(list ~sep:sp pp) xs
 
-    | Sy.Op _, [e1; e2] ->
-      fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2
+    | Sy.Var v, [] -> Var.print ppf v
+
+    | Sy.Int i, [] ->
+      if Z.sign i = -1 then
+        Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i)
+      else
+        Fmt.pf ppf "%a" Z.pp_print i
+
+    | Sy.Real q, [] ->
+      if Z.equal (Q.den q) Z.one then
+        Fmt.pf ppf "%a.0" Z.pp_print (Q.num q)
+      else if Q.sign q = -1 then
+        Fmt.pf ppf "(/ (- %a) %a)"
+          Z.pp_print (Z.abs (Q.num q))
+          Z.pp_print (Q.den q)
+      else
+        Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q)
 
-    | Sy.Op Sy.Destruct (hs, grded), [e] ->
-      fprintf fmt "%a#%s%a"
-        print e (if grded then "" else "!") Hstring.print hs
+    | Sy.Bitv (n, s), [] ->
+      Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s)
 
+    | Sy.MapsTo v, [t] ->
+      Fmt.pf ppf "(ae.mapsto %a %a)" Var.print v pp t
 
-    | Sy.In(lb, rb), [t] ->
-      fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb
+    | Sy.In (_lb, _rb), [_t] ->
+      (* WARNING: we don't print the content of this semantic trigger as
+         it requires to write a SMT-LIB compliant printer for bounds. *)
+      Fmt.pf ppf "ae.in"
 
-    | _, [] ->
-      fprintf fmt "%a" Sy.print f
+    | Sy.Void, [] ->
+      (* The void type doesn't exist in SMT-LIB standard. *)
+      Fmt.pf ppf "ae.void"
 
-    | _, _ ->
-      Format.fprintf fmt "(%a %a)" Sy.print f
-        (Util.print_list ~sep:"," ~pp:print) xs
+    | Sy.(True | False | Let | Void | Var _ | Int _ | Real _ | Bitv _
+         | MapsTo _ | In _), _ ->
+      (* All the cases have been excluded by the parser. *)
+      assert false
 
-  and print_triggers fmt trs =
-    List.iter (fun { content = l; _ } ->
-        Format.fprintf fmt "| %a@,"  (Util.print_list ~sep:"," ~pp:print) l;
-      ) trs
+  and pp_trigger ppf { content; _ } =
+    Fmt.pf ppf "@[<hv 2>(and %a)@]" Fmt.(list ~sep:sp pp) content
+
+  and pp_triggers ppf trs =
+    Fmt.pf ppf "@[<hv 2>(or %a)@]" Fmt.(list ~sep:sp pp_trigger) trs
 
-  and print_verbose fmt t = print_silent fmt t
   (* Not displaying types when int SMT format *)
+  and pp_verbose ppf t = pp_silent ppf t
 
-  and print fmt t =
-    if Options.get_debug () then print_verbose fmt t
-    else print_silent fmt t
+  and pp ppf t =
+    if Options.get_debug () then pp_verbose ppf t
+    else pp_silent ppf t
 
 end
 
 module AEPrinter = struct
+  let pp_binder ppf (var, (ty, _)) =
+    let var =
+      match var with
+      | Sy.Var v -> v
+      | _ -> assert false
+    in
+    Fmt.pf ppf "%a:%a" Var.print var Ty.pp_smtlib ty
 
-  (* Same as SmtPrinter.print_formula *)
-  let rec print_formula fmt form xs bind =
+  let pp_binders ppf binders =
+    if SMap.is_empty binders then
+      (* Can happen when quantifying only on type variables. *)
+      Fmt.pf ppf "(no term variables)"
+    else
+      Fmt.(iter_bindings ~sep:sp SMap.iter pp_binder) ppf binders
+
+  let rec pp_formula fmt form xs bind =
     let open Format in
     match form, xs, bind with
     | Sy.F_Unit _, [f1; f2], _ ->
-      fprintf fmt "@[(%a /\\@ %a)@]" print_silent f1 print_silent f2
+      fprintf fmt "@[(%a /\\@ %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Iff, [f1; f2], _ ->
-      fprintf fmt "@[(%a <->@ %a)@]" print_silent f1 print_silent f2
+      fprintf fmt "@[(%a <->@ %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Xor, [f1; f2], _ ->
-      fprintf fmt "@[(%a xor@ %a)@]" print_silent f1 print_silent f2
+      fprintf fmt "@[(%a xor@ %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Clause _, [f1; f2], _ ->
-      fprintf fmt "@[(%a \\/@ %a)@]" print_silent f1 print_silent f2
+      fprintf fmt "@[(%a \\/@ %a)@]" pp_silent f1 pp_silent f2
 
     | Sy.F_Lemma, [], B_lemma { user_trs ; main ; name ; binders; _ } ->
       if Options.get_verbose () then
         fprintf fmt "(lemma: %s forall %a[%a].@  %a)"
           name
-          print_binders binders
-          print_triggers user_trs
-          print_silent main
+          pp_binders binders
+          pp_triggers user_trs
+          pp_silent main
       else
         fprintf fmt "(lem %s)" name
 
     | Sy.F_Skolem, [], B_skolem { main; binders; _ } ->
       fprintf fmt "(<sko exists %a.> %a)"
-        print_binders binders print_silent main
+        pp_binders binders pp_silent main
 
     | _ -> assert false
 
-  and print_lit fmt lit xs =
-    let open Format in
+  and pp_lit ppf lit xs =
     match lit, xs with
-    | Sy.L_eq, a::l ->
-      fprintf fmt "(%a%a)"
-        print a (fun fmt -> List.iter (fprintf fmt " = %a" print)) l
+    | Sy.L_eq, _ :: _ ->
+      Fmt.pf ppf "@[<hv 2>(%a)@]"
+        Fmt.(list ~sep:(fun ppf () -> Fmt.pf ppf " =@, ") pp) xs
 
     | Sy.L_neg_eq, [a; b] ->
-      fprintf fmt "(%a <> %a)" print a print b
+      Fmt.pf ppf "(%a <> %a)" pp a pp b
 
-    | Sy.L_neg_eq, a::l ->
-      fprintf fmt "distinct(%a%a)"
-        print a (fun fmt -> List.iter (fprintf fmt ", %a" print)) l
+    | Sy.L_neg_eq, _ :: _ ->
+      Fmt.pf ppf "@[<hv 2>distinct(%a)@]" Fmt.(list ~sep:comma pp) xs
 
     | Sy.L_built Sy.LE, [a;b] ->
-      fprintf fmt "(%a <= %a)" print a print b
+      Fmt.pf ppf "(%a <= %a)" pp a pp b
 
     | Sy.L_built Sy.LT, [a;b] ->
-      fprintf fmt "(%a < %a)" print a print b
+      Fmt.pf ppf "(%a < %a)" pp a pp b
 
     | Sy.L_neg_built Sy.LE, [a; b] ->
-      fprintf fmt "(%a > %a)" print a print b
+      Fmt.pf ppf "(%a > %a)" pp a pp b
 
     | Sy.L_neg_built Sy.LT, [a; b] ->
-      fprintf fmt "(%a >= %a)" print a print b
+      Fmt.pf ppf "(%a >= %a)" pp a pp b
 
     | Sy.L_neg_pred, [a] ->
-      fprintf fmt "(not %a)" print a
+      Fmt.pf ppf "(not %a)" pp a
 
     | Sy.L_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "(%a ? %a)" print e Hstring.print hs
+      Fmt.pf ppf "(%a ? %a)" pp e Hstring.print hs
 
     | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "not (%a ? %a)" print e Hstring.print hs
+      Fmt.pf ppf "not (%a ? %a)" pp e Hstring.print hs
 
     | (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
       | Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
       | Sy.L_built (Sy.IsConstr _)
-      | Sy.L_neg_built (Sy.IsConstr _)) , _ ->
+      | Sy.L_neg_built (Sy.IsConstr _)), _ ->
       assert false
 
-  and print_silent fmt t =
-    let open Format in
+  and pp_operator = Sy.pp_operator ~format:`Ae
+
+  and pp_silent ppf t =
     let { f ; xs ; ty; bind; _ } = t in
     match f, xs with
-    (* Formulas *)
-    | Sy.Form form, xs -> print_formula fmt form xs bind
+    | Sy.Form form, xs -> pp_formula ppf form xs bind
+
+    | Sy.Lit lit, xs -> pp_lit ppf lit xs
 
     | Sy.Let, [] ->
       let x = match bind with B_let x -> x | _ -> assert false in
-      fprintf fmt
+      Fmt.pf ppf
         "(let%a %a =@ %a in@ %a)"
-        (fun fmt x -> if Options.get_verbose () then
-            fprintf fmt
-              " [sko = %a]" print x.let_sko) x
-        Sy.print x.let_v print x.let_e print_silent x.in_e
+        (fun ppf x -> if Options.get_verbose () then
+            Fmt.pf ppf
+              " [sko = %a]" pp x.let_sko) x
+        Symbols.print x.let_v pp x.let_e pp_silent x.in_e
 
-    (* Literals *)
-    | Sy.Lit lit, xs -> print_lit fmt lit xs
+    | Sy.(Op Get), [e1; e2] ->
+      Fmt.pf ppf "%a[%a]" pp e1 pp e2
 
-    | Sy.Op Sy.Get, [e1; e2] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(select %a %a)" print e1 print e2
-      else
-        fprintf fmt "%a[%a]" print e1 print e2
-
-    | Sy.Op Sy.Set, [e1; e2; e3] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(store %a %a %a)"
-          print e1
-          print e2
-          print e3
-      else
-        fprintf fmt "%a[%a<-%a]" print e1 print e2 print e3
+    | Sy.(Op Set), [e1; e2; e3] ->
+      Fmt.pf ppf "%a[%a<-%a]" pp e1 pp e2 pp e3
 
-    | Sy.Op Sy.Concat, [e1; e2] ->
-      fprintf fmt "%a@@%a" print e1 print e2
+    | Sy.(Op Concat), [e1; e2] ->
+      Fmt.pf ppf "%a@@%a" pp e1 pp e2
 
-    | Sy.Op Sy.Extract (i, j), [e] ->
-      fprintf fmt "%a^{%d, %d}" print e i j
+    | Sy.(Op Extract (i, j)), [e] ->
+      Fmt.pf ppf "%a^{%d, %d}" pp e i j
 
-    | Sy.Op (Sy.Access field), [e] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(%s %a)" (Hstring.view field) print e
-      else
-        fprintf fmt "%a.%s" print e (Hstring.view field)
+    | Sy.(Op (Access field)), [e] ->
+      Fmt.pf ppf "%a.%s" pp e (Hstring.view field)
 
-    | Sy.Op (Sy.Record), _ ->
+    | Sy.(Op Record), _ ->
       begin match ty with
         | Ty.Trecord { Ty.lbs = lbs; _ } ->
-          assert (List.length xs = List.length lbs);
-          fprintf fmt "{";
+          assert (List.compare_lengths xs lbs = 0);
+          Fmt.pf ppf "{";
           ignore (List.fold_left2 (fun first (field,_) e ->
-              fprintf fmt "%s%s = %a"  (if first then "" else "; ")
-                (Hstring.view field) print e;
+              Fmt.pf ppf "%s%s = %a"  (if first then "" else "; ")
+                (Hstring.view field) pp e;
               false
             ) true lbs xs);
-          fprintf fmt "}";
-        | _ -> assert false
+          Fmt.pf ppf "}";
+        | _ ->
+          (* Exclude by the typechecker. *)
+          assert false
       end
 
-    (* TODO: introduce PrefixOp in the future to simplify this ? *)
-    | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round ||
-                              op == Sy.Max_real || op == Sy.Max_int ||
-                              op == Sy.Min_real || op == Sy.Min_int ->
-      fprintf fmt "%a(%a,%a)" Sy.print f print e1 print e2
+    | Sy.(Op ((Pow | Integer_round | Max_real | Min_real | Max_int
+              | Min_int) as op)), [e1; e2] ->
+      Fmt.pf ppf "%a(%a, %a)" pp_operator op pp e1 pp e2
 
-    (* TODO: introduce PrefixOp in the future to simplify this ? *)
-    | Sy.Op (Sy.Constr hs), ((_::_) as l) ->
-      fprintf fmt "%a(%a)"
-        Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l
+    | Sy.(Op (Constr _ as op)), _::_ ->
+      Fmt.pf ppf "%a(%a)" pp_operator op Fmt.(list ~sep:comma pp) xs
 
-    | Sy.Op _, [e1; e2] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2
-      else
-        fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2
-
-    | Sy.Op Sy.Destruct (hs, grded), [e] ->
-      fprintf fmt "%a#%s%a"
-        print e (if grded then "" else "!") Hstring.print hs
+    | Sy.(Op Destruct (hs, grded)), [e] ->
+      Fmt.pf ppf "%a#%s%a"
+        pp e (if grded then "" else "!") Hstring.print hs
 
+    | Sy.Op op, [e1; e2] ->
+      Fmt.pf ppf "(%a %a %a)" pp e1 pp_operator op pp e2
 
-    | Sy.In(lb, rb), [t] ->
-      fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb
-
+    | Sy.In (lb, rb), [t] ->
+      Fmt.pf ppf "(%a in %a, %a)" pp t Sy.print_bound lb Sy.print_bound rb
 
     | _, [] ->
-      fprintf fmt "%a" Sy.print f
+      Fmt.pf ppf "%a" Sy.print f
 
     | _, _ ->
-      fprintf fmt "%a(%a)" Sy.print f (Util.print_list ~sep:"," ~pp:print) xs
+      Fmt.pf ppf "%a(%a)" Sy.print f Fmt.(list ~sep:comma pp) xs
+
+  and pp_trigger ppf { content; _ } =
+    Fmt.list ~sep:Fmt.comma pp ppf content
 
-  and print_triggers fmt trs =
-    List.iter (fun { content = l; _ } ->
-        Format.fprintf fmt "| %a@," (Util.print_list ~sep:"," ~pp:print) l;
-      ) trs
+  and pp_triggers ppf trs =
+    Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "|@,") pp_trigger ppf trs
 
-  and print_verbose fmt t =
-    Format.fprintf fmt "(%a : %a)" print_silent t Ty.print t.ty
+  and print_verbose ppf t =
+    Fmt.pf ppf "(%a : %a)" pp_silent t Ty.print t.ty
 
-  and print fmt t =
+  and pp fmt t =
     if Options.get_debug () then print_verbose fmt t
-    else print_silent fmt t
+    else pp_silent fmt t
 
 end
 
-let print fmt =
+let print ppf =
   if Options.get_output_smtlib ()
-  then SmtPrinter.print fmt
-  else AEPrinter.print fmt
+  then SmtPrinter.pp ppf
+  else AEPrinter.pp ppf
 
-let print_triggers fmt =
+let print_triggers ppf =
   if Options.get_output_smtlib ()
-  then SmtPrinter.print_triggers fmt
-  else AEPrinter.print_triggers fmt
+  then SmtPrinter.pp_triggers ppf
+  else AEPrinter.pp_triggers ppf
 
-let print_list_sep sep = Util.print_list ~sep ~pp:print
+let print_list_sep sep =
+  if Options.get_output_smtlib () then
+    Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "%s" sep) SmtPrinter.pp
+  else
+    Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "%s" sep) AEPrinter.pp
+
+let print_list ppf = print_list_sep "," ppf
 
-let print_list fmt = print_list_sep "," fmt
+let pp_binders ppf =
+  if Options.get_output_smtlib ()
+  then SmtPrinter.pp_binders ppf
+  else AEPrinter.pp_binders ppf
 
 (** different views of an expression *)
 
@@ -1254,8 +1235,8 @@ let no_capture_issue s_t binders =
       Printer.print_wrn
         "captures between@,%aand%a!@,(captured = %a)"
         (SMap.print print) s_t
-        print_binders binders
-        print_binders capt_bind;
+        pp_binders binders
+        pp_binders capt_bind;
       false
     end
 
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 2f443c8c54..45863cc149 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -278,28 +278,7 @@ let string_of_bound b =
 
 let print_bound fmt b = Format.fprintf fmt "%s" (string_of_bound b)
 
-let string_of_lit lit = match lit with
-  | L_eq -> "="
-  | L_neg_eq -> "<>"
-  | L_neg_pred -> "not "
-  | L_built LE -> "<="
-  | L_built LT -> "<"
-  | L_neg_built LE -> ">"
-  | L_neg_built LT -> ">="
-  | L_built (IsConstr h) ->
-    Format.sprintf "? %s" (Hstring.view h)
-  | L_neg_built (IsConstr h) ->
-    Format.sprintf "?not? %s" (Hstring.view h)
-
-let string_of_form f = match f with
-  | F_Unit _ -> "/\\"
-  | F_Clause _ -> "\\/"
-  | F_Lemma -> "Lemma"
-  | F_Skolem -> "Skolem"
-  | F_Iff -> "<->"
-  | F_Xor -> "xor"
-
-let name_to_string =
+let pp_name ppf =
   let no_need_to_quote s =
     String.length s > 0 &&
     (match s.[0] with | '0'..'9' -> false | _ -> true) &&
@@ -317,82 +296,209 @@ let name_to_string =
       true
     with Exit -> false
   in
-  fun s -> if no_need_to_quote s then s else Format.sprintf "|%s|" s
-
-let to_string ?(show_vars=true) x = match x with
-  | Name (n, _, _) -> name_to_string @@ Hstring.view n
-  | Var v when show_vars -> Format.sprintf "'%s'" (Var.to_string v)
-  | Var v -> Var.to_string v
-  | Int n -> Z.to_string n
-  | Real n -> Q.to_string n
-  | Bitv (n, s) -> Fmt.str "[|%s|]" (Z.format (Fmt.str "%%0%db" n) s)
-  | Op Plus -> "+"
-  | Op Minus -> "-"
-  | Op Mult -> "*"
-  | Op Div -> "/"
-  | Op Modulo -> "%"
-  | Op (Access s) ->
-    if Options.get_output_smtlib () then
-      (Hstring.view s)
+  fun s ->
+    if no_need_to_quote s then
+      Fmt.string ppf s
     else
-      "@Access_"^(Hstring.view s)
-  | Op (Constr s) -> (Hstring.view s)
-  | Op (Destruct (s,g)) ->
-    Format.sprintf "%s%s" (if g then "" else "!") (Hstring.view s)
-
-  | Op Record -> "@Record"
-  | Op Get -> "get"
-  | Op Set -> "set"
-  | Op Float -> "float"
-  | Op Fixed -> "fixed"
-  | Op Abs_int -> "abs_int"
-  | Op Abs_real -> "abs_real"
-  | Op Sqrt_real -> "sqrt_real"
-  | Op Sqrt_real_default -> "sqrt_real_default"
-  | Op Sqrt_real_excess -> "sqrt_real_excess"
-  | Op Real_of_int -> "real_of_int"
-  | Op Real_is_int -> "real_is_int"
-  | Op Int_floor -> "int_floor"
-  | Op Int_ceil -> "int_ceil"
-  | Op Max_real -> "max_real"
-  | Op Max_int -> "max_int"
-  | Op Min_real -> "min_real"
-  | Op Min_int -> "min_int"
-  | Op Integer_log2 -> "integer_log2"
-  | Op Pow -> "**"
-  | Op Integer_round -> "integer_round"
-  | Op Not_theory_constant -> "not_theory_constant"
-  | Op Is_theory_constant -> "is_theory_constant"
-  | Op Linear_dependency -> "linear_dependency"
-  | Op Concat -> "@"
-  | Op Extract (i, j) -> Format.sprintf "^{%d; %d}" i j
-  | Op BVnot -> "bvnot"
-  | Op BVand -> "bvand"
-  | Op BVor -> "bvor"
-  | Op Int2BV n -> Format.sprintf "int2bv[%d]" n
-  | Op BV2Nat -> "bv2nat"
-  | Op Tite -> "ite"
-  | Op Reach -> assert false
-  | True -> "true"
-  | False -> "false"
-  | Void -> "void"
-  | In (lb, rb) ->
-    Format.sprintf "%s , %s" (string_of_bound lb) (string_of_bound rb)
-
-  | MapsTo x ->  Format.sprintf "%s |->" (Var.to_string x)
-
-  | Lit lit -> string_of_lit lit
-  | Form form -> string_of_form form
-  | Let -> "let"
-
-  | Op (Optimize {order; is_max=true}) -> Format.sprintf "maximize(-,%d)" order
-  | Op (Optimize {order; is_max=false}) -> Format.sprintf "minimize(-,%d)" order
-
-let to_string_clean s = to_string ~show_vars:false s
-let to_string s = to_string ~show_vars:true s
-
-let print_clean fmt s = Format.fprintf fmt "%s" (to_string_clean s)
-let print fmt s = Format.fprintf fmt "%s" (to_string s)
+      Fmt.pf ppf "|%s|" s
+
+module AEPrinter = struct
+  let pp_operator ppf op =
+    match op with
+    (* Core theory *)
+    | Tite -> Fmt.pf ppf "ite"
+
+    (* Reals and Ints theories *)
+    | Plus -> Fmt.pf ppf "+"
+    | Minus -> Fmt.pf ppf "-"
+    | Mult -> Fmt.pf ppf "*"
+    | Div -> Fmt.pf ppf "/"
+    | Modulo -> Fmt.pf ppf "%%"
+    | Pow -> Fmt.pf ppf "**"
+    | Sqrt_real -> Fmt.pf ppf "sqrt_real"
+    | Sqrt_real_default -> Fmt.pf ppf "sqrt_real_default"
+    | Sqrt_real_excess -> Fmt.pf ppf "sqrt_real_excess"
+    | Int_floor -> Fmt.pf ppf "int_floor"
+    | Int_ceil -> Fmt.pf ppf "int_ceil"
+    | Max_real -> Fmt.pf ppf "max_real"
+    | Max_int -> Fmt.pf ppf "max_int"
+    | Min_real -> Fmt.pf ppf "min_real"
+    | Min_int -> Fmt.pf ppf "min_int"
+    | Integer_log2 -> Fmt.pf ppf "integer_log2"
+    | Integer_round -> Fmt.pf ppf "integer_round"
+
+    (* Reals_Ints theory *)
+    | Abs_int -> Fmt.pf ppf "abs_int"
+    | Abs_real -> Fmt.pf ppf "abs_real"
+    | Real_of_int -> Fmt.pf ppf "real_of_int"
+    | Real_is_int -> Fmt.pf ppf "real_is_int"
+
+    (* FixedSizedBitVectors theory *)
+    | Extract (i, j) -> Fmt.pf ppf "^{%d; %d}" i j
+    | Concat -> Fmt.pf ppf "@"
+    | BV2Nat -> Fmt.pf ppf "bv2nat"
+    | Int2BV n -> Fmt.pf ppf "int2bv[%d]" n
+    | BVnot -> Fmt.pf ppf "bvnot"
+    | BVand -> Fmt.pf ppf "bvand"
+    | BVor -> Fmt.pf ppf "bvor"
+
+    (* ArraysEx theory *)
+    | Get -> Fmt.pf ppf "get"
+    | Set -> Fmt.pf ppf "set"
+
+    (* DT theory *)
+    | Record -> Fmt.pf ppf "@Record"
+    | Access s -> Fmt.pf ppf "@Access_%a" Hstring.print s
+    | Constr s -> Hstring.print ppf s
+    | Destruct (s, g) ->
+      Fmt.pf ppf "%s%a" (if g then "" else "!") Hstring.print s
+
+    (* Float theory *)
+    | Float -> Fmt.pf ppf "float"
+    | Fixed -> Fmt.pf ppf "fixed"
+
+    | Not_theory_constant -> Fmt.pf ppf "not_theory_constant"
+    | Is_theory_constant -> Fmt.pf ppf "is_theory_constant"
+    | Linear_dependency -> Fmt.pf ppf "linear_dependency"
+
+    | Optimize {order; is_max=true} ->
+      Fmt.pf ppf "maximize(-,%d)" order
+    | Optimize {order; is_max=false} ->
+      Fmt.pf ppf "minimize(-,%d)" order
+    | Reach -> assert false
+
+  let pp_lit ppf lit =
+    match lit with
+    | L_eq -> Fmt.pf ppf "="
+    | L_neg_eq -> Fmt.pf ppf "distinct"
+    | L_built LE -> Fmt.pf ppf "<="
+    | L_built LT -> Fmt.pf ppf "<"
+    | L_neg_built LE -> Fmt.pf ppf ">"
+    | L_neg_built LT -> Fmt.pf ppf ">="
+    | L_neg_pred -> Fmt.pf ppf "not "
+    | L_built (IsConstr h) ->
+      Fmt.pf ppf "? %a" Hstring.print h
+    | L_neg_built (IsConstr h) ->
+      Fmt.pf ppf "?not? %a" Hstring.print h
+
+  let pp_form ppf f =
+    match f with
+    | F_Unit _ -> Fmt.pf ppf "/\\"
+    | F_Clause _ -> Fmt.pf ppf "\\/"
+    | F_Lemma -> Fmt.pf ppf "Lemma"
+    | F_Skolem -> Fmt.pf ppf "Skolem"
+    | F_Iff -> Fmt.pf ppf "<->"
+    | F_Xor -> Fmt.pf ppf "xor"
+
+  let pp ?(show_vars = true) ppf sy =
+    match sy with
+    | Lit lit -> pp_lit ppf lit
+    | Form form -> pp_form ppf form
+    | Let -> Fmt.pf ppf "let"
+    | Op op -> pp_operator ppf op
+
+    (* Core theory *)
+    | True -> Fmt.pf ppf "true"
+    | False -> Fmt.pf ppf "false"
+    | Void -> Fmt.pf ppf "void"
+    | Name (n, _, _) -> pp_name ppf (Hstring.view n)
+    | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.to_string v)
+    | Var v -> Fmt.string ppf (Var.to_string v)
+
+    (* Reals and Ints theories *)
+    | Int i -> Z.pp_print ppf i
+    | Real q -> Q.pp_print ppf q
+
+    (* FixedSizedBitVectors theory *)
+    | Bitv (n, s) ->
+      Fmt.pf ppf "[|%s|]" (Z.format (Fmt.str "%%0%db" n) s)
+
+    (* Symbols used in semantic triggers *)
+    | In (lb, rb) ->
+      Fmt.pf ppf "%s, %s" (string_of_bound lb) (string_of_bound rb)
+    | MapsTo v -> Fmt.pf ppf "%a |->" Var.print v
+end
+
+module SmtPrinter = struct
+  let pp_operator ppf op =
+    match op with
+    (* Core theory *)
+    |Tite -> Fmt.pf ppf "ite"
+
+    (* Reals and Ints theories *)
+    | Plus -> Fmt.pf ppf "+"
+    | Minus -> Fmt.pf ppf "-"
+    | Mult -> Fmt.pf ppf "*"
+    | Div -> Fmt.pf ppf "/"
+    | Modulo -> Fmt.pf ppf "%%"
+
+    (* Reals_Ints theory *)
+    | Abs_int | Abs_real -> Fmt.pf ppf "abs"
+    | Real_of_int -> Fmt.pf ppf "to_real"
+    | Real_is_int -> Fmt.pf ppf "is_int"
+    | Integer_round -> Fmt.pf ppf "to_int"
+
+    (* FixedSizedBitVectors theory *)
+    | Extract (i, j) ->
+      Fmt.pf ppf "(_ extract %d %d)" i j
+    | Concat -> Fmt.pf ppf "concat"
+    | BV2Nat -> Fmt.pf ppf "bv2nat"
+    | BVnot -> Fmt.pf ppf "bvnot"
+    | BVand -> Fmt.pf ppf "bvand"
+    | BVor -> Fmt.pf ppf "bvor"
+
+    (* ArraysEx theory *)
+    | Get -> Fmt.pf ppf "select"
+    | Set -> Fmt.pf ppf "store"
+
+    (* DT theory *)
+    | Record -> ()
+    | Access s | Constr s | Destruct (s, _) -> Hstring.print ppf s
+
+    (* Float theory *)
+    | Float -> Fmt.pf ppf "ae.round"
+
+    (* Not in the SMT-LIB standard *)
+    | Int2BV _ -> Fmt.pf ppf "(_ int2bv)"
+    | Not_theory_constant -> Fmt.pf ppf "ae.not_theory_constant"
+    | Is_theory_constant -> Fmt.pf ppf "ae.is_theory_constant"
+    | Linear_dependency -> Fmt.pf ppf "ae.linear_dependency"
+    | Sqrt_real -> Fmt.pf ppf "ae.sqrt_real"
+    | Sqrt_real_default -> Fmt.pf ppf "ae.sqrt_real_default"
+    | Sqrt_real_excess -> Fmt.pf ppf "ae.sqrt_real_excess"
+    | Int_floor -> Fmt.pf ppf "ae.int_floor"
+    | Int_ceil -> Fmt.pf ppf "ae.int_ceil"
+    | Max_real -> Fmt.pf ppf "ae.max_real"
+    | Max_int -> Fmt.pf ppf "ae.max_int"
+    | Min_real -> Fmt.pf ppf "ae.min_real"
+    | Min_int -> Fmt.pf ppf "ae.min_int"
+    | Integer_log2 -> Fmt.pf ppf "ae.integer_log2"
+    | Pow -> Fmt.pf ppf "ae.pow"
+
+    | Optimize _ ->
+      (* TODO: this case will be removed in the PR #921. *)
+      assert false
+
+    | Fixed | Reach ->
+      (* Unused symbols *)
+      assert false
+
+end
+
+let[@inline always] pp_operator ~(format:[`Ae | `Smtlib]) ppf op =
+  match format with
+  | `Ae -> AEPrinter.pp_operator ppf op
+  | `Smtlib -> SmtPrinter.pp_operator ppf op
+
+let print_clean = AEPrinter.pp ~show_vars:false
+let print = AEPrinter.pp ~show_vars:true
+
+let to_string_clean sy =
+  Fmt.str "%a" (AEPrinter.pp ~show_vars:false) sy
+
+let to_string sy =
+  Fmt.str "%a"(AEPrinter.pp ~show_vars:true) sy
+
 
 module type Id = sig
   val fresh : ?base:string -> unit -> string
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index 59078b83ff..a620669e5b 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -122,10 +122,16 @@ val compare_operators : operator -> operator -> int
 val hash : t -> int
 
 val to_string : t -> string
-val print : Format.formatter -> t -> unit
+val print : t Fmt.t
+(* Printer used by debugging messages. *)
 
 val to_string_clean : t -> string
-val print_clean : Format.formatter -> t -> unit
+val print_clean : t Fmt.t
+
+val pp_name : string Fmt.t
+
+val pp_operator : format:[`Ae | `Smtlib] -> operator Fmt.t
+(* [pp_smtlib ppf sy] prints the symbol [sy] on the formatter [ppf]. *)
 
 (*val dummy : t*)