From a362505d86b4100d1f8ac538b80704da590165a9 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 16 Mar 2015 15:22:18 +0100
Subject: [PATCH] Little test

---
 solver/mcsolver.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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 -> ()