diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml
index 4ec01a55..53aca04d 100644
--- a/src/lra/sidekick_arith_lra.ml
+++ b/src/lra/sidekick_arith_lra.ml
@@ -563,13 +563,15 @@ module Make(A : ARG) : S with module A = A = struct
 
   (** Check satisfiability of simplex, and sets [self.last_res] *)
   let check_simplex_ self si acts : SimpSolver.Subst.t =
-    Log.debug 5 "(lra.check-simplex)";
+    Log.debugf 5
+      (fun k->k "(@[lra.check-simplex@ :n-vars %d :n-rows %d@])"
+          (SimpSolver.n_vars self.simplex) (SimpSolver.n_rows self.simplex));
     let res =
-      Profile.with_ "lra.simplex.solve"
-        (fun () ->
-           SimpSolver.check self.simplex
-             ~on_propagate:(on_propagate_ si acts))
+      Profile.with_ "lra.simplex.solve" @@ fun () ->
+      SimpSolver.check self.simplex
+        ~on_propagate:(on_propagate_ si acts)
     in
+    Log.debug 5 "(lra.check-simplex.done)";
     self.last_res <- Some res;
     begin match res with
       | SimpSolver.Sat m -> m
diff --git a/src/simplex/sidekick_simplex.ml b/src/simplex/sidekick_simplex.ml
index 1d751525..df8caac2 100644
--- a/src/simplex/sidekick_simplex.ml
+++ b/src/simplex/sidekick_simplex.ml
@@ -152,6 +152,9 @@ module type S = sig
     t -> result option
   (** Try to solve and respect the integer constraints. *)
 
+  val n_vars: t -> int
+  val n_rows: t -> int
+
   (**/**)
   val _check_invariants : t -> unit
   (* check internal invariants *)
@@ -470,6 +473,9 @@ module Make(Arg: ARG)
       ~f:(fun f -> f());
     ()
 
+  let n_vars self = Vec.size self.vars
+  let n_rows self = Matrix.n_rows self.matrix
+
   let pp_stats out (self:t) : unit =
     Fmt.fprintf out "(@[simplex@ :n-vars %d@ :n-rows %d@])"
       (Vec.size self.vars) (Matrix.n_rows self.matrix)