From 803b61c7dc8646071034d4d8dd7e233f0d00a67e Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 29 Jan 2015 15:39:48 +0100
Subject: [PATCH] Removed an error that was raised for tautological conflict
 clauses

---
 solver/mcproof.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/solver/mcproof.ml b/solver/mcproof.ml
index bd440a50..f9e620db 100644
--- a/solver/mcproof.ml
+++ b/solver/mcproof.ml
@@ -78,10 +78,7 @@ module Make(St : Mcsolver_types.S) = struct
     for i = 0 to Vec.size v - 1 do
       l := (Vec.get v i) :: !l
     done;
-    let l, res = resolve (List.sort_uniq compare_atoms !l) in
-    if l <> [] then
-      raise (Resolution_error "Input cause is a tautology");
-    res
+    List.sort_uniq compare_atoms !l
 
   (* Adding hyptoheses *)
   let is_unit_hyp = function