From c4142480db1c22347982b8da4d67fa0b7336dad1 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 13 Apr 2016 21:31:55 +0200
Subject: [PATCH] If root is Sat, formula is unconditionally Sat

---
 src/lib/CoAlgReasoner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index ab63f46..efb958d 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -1049,7 +1049,7 @@ let isRootSat () =
   match coreGetStatus (graphGetRoot ()) with
   | Expandable -> None
   | Unsat -> Some false
-  | Sat -> if (queueIsEmpty()) then Some true else None
+  | Sat -> Some true
   | Open -> if (queueIsEmpty()) then Some false else None
 
 let reasonerFinished () =
-- 
GitLab