From 88eaa03968345cc0e856d17dd089eca0ce0c4107 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 30 Mar 2017 19:29:53 +0200
Subject: [PATCH] Internal check also checks for undecided lits

---
 src/core/internal.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 1846ff75..ef91c71d 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -1237,7 +1237,11 @@ module Make
 
   (* Check satisfiability *)
   let check_clause c =
-    let res = Array_util.exists (fun a -> a.is_true) c.atoms in
+    let tmp = Array.map (fun a ->
+        if a.is_true then true
+        else if a.neg.is_true then false
+        else raise UndecidedLit) c.atoms in
+    let res = Array_util.exists (fun x -> x) tmp in
     if not res then begin
       Log.debugf debug "Clause not satisfied: @[<hov>%a@]"
         (fun k -> k St.pp_clause c);