From 25dae83c6e3058e5e157681ebb1bc5f3144f1d28 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sun, 15 Mar 2015 22:12:21 +0100
Subject: [PATCH] Still working...

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

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 0c85e99b..f9ab63ba 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -572,6 +572,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         done;
         (* no watch lit found *)
         if first.neg.is_true || (th_eval first = Some false) then begin
+            L.debug 100 "clause is false";
           (* clause is false *)
           env.qhead <- Vec.size env.trail;
           for k = i to Vec.size watched - 1 do
@@ -580,8 +581,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
           done;
           L.debug 3 "Conflict found : %a" St.pp_clause c;
           raise (Conflict c)
-        end
-        else begin
+        end else begin
+          L.debug 100 "clause is unit";
           (* clause is unit *)
           Vec.set watched !new_sz c;
           incr new_sz;