diff --git a/src/main/main.ml b/src/main/main.ml
index fc67c4d7..8bcc75c5 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -152,9 +152,10 @@ let main_cnf () : _ result =
   S.Dimacs.parse_file solver !file >>= fun () ->
   let r = S.solve solver in
   if !p_stat then (
-    Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d n-atoms: %d@."
+    Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d@. \
+                ; n-restarts: %d n-atoms: %d@."
       (S.SAT.n_conflicts solver) (S.SAT.n_decisions solver)
-      (S.SAT.n_propagations solver) !n_atoms;
+      (S.SAT.n_propagations solver) (S.SAT.n_restarts solver) !n_atoms;
   );
   r
 
diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml
index c8dc6686..c5926442 100644
--- a/src/sat/Solver_intf.ml
+++ b/src/sat/Solver_intf.ml
@@ -379,6 +379,8 @@ module type S = sig
     ?on_conflict:(atom array -> unit) ->
     ?on_decision:(atom -> unit) ->
     ?on_new_atom:(atom -> unit) ->
+    ?on_learnt:(atom array -> unit) ->
+    ?on_gc:(atom array -> unit) ->
     ?store_proof:bool ->
     ?size:[`Tiny|`Small|`Big] ->
     theory ->
@@ -444,5 +446,6 @@ module type S = sig
   val n_propagations : t -> int
   val n_decisions : t -> int
   val n_conflicts : t -> int
+  val n_restarts : t -> int
 end