diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index a2cabcf08f2293cd6615a88e3bb1ff3e730624e4..76151e6abe7084bb6bf864089de7a7e390d7af6c 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -164,13 +164,38 @@ let propagateSatMu () =
   *)
 
   let rec fixpointstep setStates setCores =
-    let allowedStates = setFinishingStates in
-    let allowedCores = setFinishingCores in
+    let allowedStates = setEmptyState () in
+    let allowedCores = setEmptyCore () in
+    let initialStates = setEmptyState () in
+    let initialCores = setEmptyCore () in
+
+    let checkFinishingState (state : state) =
+      let ruleiter (dependencies, corelist) : bool =
+        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
+      in
+      if not (List.exists ruleiter (stateGetRules state)) then begin
+        setAddState allowedStates state;
+        setAddState initialStates state
+      end
+    in
+    let checkFinishingCore (core : core) =
+      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
+                (coreGetChildren core)) then begin
+        setAddCore allowedCores core;
+        setAddCore initialCores core
+      end
+    in
+    setIterState checkFinishingState setFinishingStates;
+    setIterCore checkFinishingCore setFinishingCores;
 
     let rec visitParentStates (core : core) : unit =
-      if setMemCore allowedCores core then () else begin
+      if not (setMemCore setCores core) then ()
+      else begin
         let children = coreGetChildren core in
-        let acceptable = List.exists (fun (state) -> setMemState allowedStates state) children in
+        let acceptable =
+          List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
+            children
+        in
         if acceptable then begin
           print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
           setAddCore allowedCores core;
@@ -180,23 +205,25 @@ let propagateSatMu () =
       end
 
     and visitParentCores (state : state) : unit =
-      if setMemState allowedStates state then () else begin
+      if not (setMemState setStates state) then ()
+      else begin
         let rules = stateGetRules state in
         let ruleiter (dependencies, corelist) =
-          List.exists (fun (core) -> setMemCore allowedCores core) corelist
+          List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
+            corelist
         in
         let acceptable = List.for_all ruleiter rules in
         if acceptable then begin
           print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
           setAddState allowedStates state;
-          List.iter (fun core -> visitParentStates core)
+          List.iter (fun core -> if not (setMemCore allowedCores core) then visitParentStates core)
             (stateGetParents state)
         end
       end
     in
 
-    setIterState visitParentCores setFinishingStates;
-    setIterCore visitParentStates setFinishingCores;
+    setIterState visitParentCores initialStates;
+    setIterCore visitParentStates initialCores;
 
     if (setLengthState setStates) = (setLengthState allowedStates) &&
       (setLengthCore setCores) = (setLengthCore allowedCores)