From 9b41aab1b1d62351f05c913d10353fceb0f96ebc Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 10 Mar 2015 18:02:31 +0100
Subject: [PATCH] Tautological input clauses are now accepted

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

diff --git a/solver/mcproof.ml b/solver/mcproof.ml
index 93ae47b5..5da67828 100644
--- a/solver/mcproof.ml
+++ b/solver/mcproof.ml
@@ -77,9 +77,10 @@ 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
+    let res = List.sort_uniq compare_atoms !l in
+    let l, _ = resolve res in
     if l <> [] then
-      raise (Resolution_error "Input clause is a tautology");
+      Log.debug 3 "Input clause is a tautology";
     res
 
   (* Adding hyptoheses *)