From 436dc491117208dd623c3013f80d938159caaac4 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 29 Jan 2015 15:44:54 +0100
Subject: [PATCH] Better error message

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

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index d2368cd7..9df6cd9f 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -370,7 +370,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
                                     var_bump_activity a.var;
                                     history := d :: !history;
                                     c := res
-                            | _ -> assert false
+                            | _ ->
+                                L.debug 0 "Found %d resolution lits" (List.length tmp);
+                                List.iter (fun c -> L.debug 0 " |- %a" St.pp_atom c) tmp;
+                                assert false
                             end
                     | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a
                     | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)