diff --git a/src/arith/lra/Sidekick_arith_lra.ml b/src/arith/lra/Sidekick_arith_lra.ml
index 543e9383..98d69326 100644
--- a/src/arith/lra/Sidekick_arith_lra.ml
+++ b/src/arith/lra/Sidekick_arith_lra.ml
@@ -69,6 +69,7 @@ module Make(A : ARG) : S with module A = A = struct
   module FM_A = FM.Make(struct
       module T = T
       type tag = Lit.t
+      let pp_tag = Lit.pp
     end)
 
   (* linear expressions *)
@@ -142,6 +143,9 @@ module Make(A : ARG) : S with module A = A = struct
     let t = fresh_term ~pre self Ty.bool in
     mk_lit t
 
+  let pp_pred_def out (p,l1,l2) : unit =
+    Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" FM.Pred.pp p LE.pp l1 LE.pp l2
+
   (* turn the term into a linear expression. Apply [f] on leaves. *)
   let rec as_linexp ~f (t:T.t) : LE.t =
     let open LE.Infix in
@@ -175,13 +179,15 @@ module Make(A : ARG) : S with module A = A = struct
       let l2 = as_linexp ~f:recurse t2 in
       let proxy = fresh_term self ~pre:"_pred_lra_" Ty.bool in
       T.Tbl.add self.pred_defs proxy (pred, l1, l2);
-      Log.debugf 5 (fun k->k"lra.preprocess.step %a :into %a" T.pp t T.pp proxy);
+      Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
+                       T.pp t T.pp proxy pp_pred_def (pred,l1,l2));
       Some proxy
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp ~f:recurse t in
       let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
       self.t_defs <- (proxy, le) :: self.t_defs;
-      Log.debugf 5 (fun k->k"lra.preprocess.step %a :into %a" T.pp t T.pp proxy);
+      Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
+                       T.pp t T.pp proxy LE.pp le);
       Some proxy
     | LRA_const _ | LRA_other _ -> None
 
diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
index 3efb5ba7..ab695cb5 100644
--- a/src/arith/lra/fourier_motzkin.ml
+++ b/src/arith/lra/fourier_motzkin.ml
@@ -12,6 +12,7 @@ module type ARG = sig
   end
 
   type tag
+  val pp_tag : tag Fmt.printer
 end
 
 module Pred : sig
@@ -173,10 +174,17 @@ module Make(A : ARG)
         if Q.equal Q.one q then T.pp out e
         else Fmt.fprintf out "%a * %a" Q.pp_print q T.pp e
       in
-      Fmt.fprintf out "(@[%a@ + %a@])"
-        Q.pp_print self.const (Util.pp_iter ~sep:" + " pp_pair) (M.to_iter self.le)
+      let pp_sum out le =
+        (Util.pp_iter ~sep:" + " pp_pair) out (M.to_iter le)
+      in
+      if Q.sign self.const = 0 then (
+        Fmt.fprintf out "(@[%a@])" pp_sum self.le
+      ) else (
+        Fmt.fprintf out "(@[%a@ + %a@])" Q.pp_print self.const pp_sum self.le
+      )
   end
 
+  (** {2 Constraints} *)
   module Constr = struct
     type t = {
       pred: Pred.t;
@@ -271,7 +279,8 @@ module Make(A : ARG)
     )
 
   let assert_c (self:t) c0 : unit =
-    Log.debugf 10 (fun k->k "(@[FM.add-constr@ %a@])" Constr.pp c0);
+    Log.debugf 10 (fun k->k "(@[FM.add-constr@ %a@ :tags %a@])"
+                      Constr.pp c0 (Fmt.Dump.list A.pp_tag) c0.tag);
     let c = Constr.normalize c0 in
     if c.pred <> c0.pred then (
       Log.debugf 30 (fun k->k "(@[FM.normalized %a@])" Constr.pp c);