diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index c2cbb91b..e55551e0 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -846,14 +846,14 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         begin try
             search (to_int !n_of_conflicts) (to_int !n_of_learnts)
           with
-          | Restart ->
-            n_of_conflicts := !n_of_conflicts *. env.restart_inc;
-            n_of_learnts   := !n_of_learnts *. env.learntsize_inc
+          | Restart -> ()
           | Sat ->
             let tag = ref false in
             Th.if_sat (full_slice tag);
             if not !tag then raise Sat
-        end
+        end;
+        n_of_conflicts := !n_of_conflicts *. env.restart_inc;
+        n_of_learnts   := !n_of_learnts *. env.learntsize_inc
       done
     with
     | Sat -> ()