From f604401e4712a93821dcca4254dfb5b4437511c6 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 16 Mar 2015 15:29:12 +0100
Subject: [PATCH] More log messages

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

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index e55551e0..ae0d13ab 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -792,6 +792,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     let conflictC = ref 0 in
     env.starts <- env.starts + 1;
     while (true) do
+      L.debug 100 "searching %d/%d (%d)" !conflictC n_of_conflicts n_of_learnts;
       match propagate () with
       | Some confl -> (* Conflict *)
         incr conflictC;
@@ -799,13 +800,12 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
 
       | None -> (* No Conflict *)
         if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat;
-        if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then
-          begin
+        if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then begin
             L.debug 1 "Restarting...";
             env.progress_estimate <- progress_estimate();
             cancel_until 0;
             raise Restart
-          end;
+        end;
         if decision_level() = 0 then simplify ();
 
         if n_of_learnts >= 0 &&