From 2fba43c0aff0f4c8644a5cc1090e5b2fcd495910 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 8 Apr 2016 02:28:55 +0200
Subject: [PATCH] Make Sat children actually propagate their state to the
parents
---
src/lib/CoAlgReasoner.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index cf35e05..0035ba3 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -178,7 +178,7 @@ let propagateSatMu () =
let allowedCores = setEmptyCore () in
let rec visitParentStates (core : core) : unit =
- if not (setMemCore setCores core) then ()
+ if not (setMemCore setCores core || setMemCore setSatCores core) then ()
else begin
let children = coreGetChildren core in
let acceptable =
@@ -194,7 +194,7 @@ let propagateSatMu () =
end
and visitParentCores (state : state) : unit =
- if not (setMemState setStates state) then ()
+ if not (setMemState setStates state || setMemState setSatStates state) then ()
else begin
let rules = stateGetRules state in
let ruleiter (dependencies, corelist) =
--
GitLab