From 215ad4d7ae4231ca91d6f8855008ee5d6969ecc0 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 8 Apr 2016 20:09:30 +0200
Subject: [PATCH] Mark `True` only node as 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 255dd9d..20f0a57 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -129,7 +129,7 @@ let propagateSatMu () =
setAddState setSatStates state
| Expandable -> ()
| Open ->
- if stateGetStatus state == Open && List.length (stateGetRules state) == 0
+ if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
then begin
setAddState setSatStates state;
stateSetStatus state Sat
--
GitLab