diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 20f0a57fec77c73a6f745ce51529481d96555126..f24d02fe8026478e16fec68d45e131a54d7fede5 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -178,36 +178,40 @@ let propagateSatMu () =
     let allowedCores = setEmptyCore () in
 
     let rec visitParentStates (core : core) : unit =
-      if not (setMemCore setCores core || setMemCore setSatCores core) then ()
-      else begin
-        let children = coreGetChildren core in
-        let acceptable =
-          List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
-            children
+      print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core)));
+      if not (setMemCore allowedCores core)
+      then begin
+        setAddCore allowedCores core;
+        print_endline ("Adding Core " ^ (string_of_int (coreGetIdx core)));
+        let verifyParent (state,_) =
+          let rules = stateGetRules state in
+          let ruleiter (dependencies, corelist) =
+            List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
+              corelist
+          in
+          if List.for_all ruleiter rules
+          then visitParentCores state
+          else print_endline ("Not considering state "^(string_of_int (stateGetIdx state)))
         in
-        if acceptable then begin
-          print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
-          setAddCore allowedCores core;
-          List.iter (fun (state, _) -> visitParentCores state)
-            (coreGetParents core)
-        end
+        List.iter verifyParent (coreGetParents core)
       end
 
     and visitParentCores (state : state) : unit =
-      if not (setMemState setStates state || setMemState setSatStates state) then ()
-      else begin
-        let rules = stateGetRules state in
-        let ruleiter (dependencies, corelist) =
-          List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
-            corelist
+      print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state)));
+      if not (setMemState allowedStates state)
+      then begin
+        setAddState allowedStates state;
+        print_endline ("Adding State " ^ (string_of_int (stateGetIdx state)));
+        let verifyParent core =
+          let acceptable =
+            List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
+              (coreGetChildren core)
+          in
+          if acceptable
+          then visitParentStates core
+          else print_endline ("Not considering state "^(string_of_int (coreGetIdx core)))
         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 -> if not (setMemCore allowedCores core) then visitParentStates core)
-            (stateGetParents state)
-        end
+        List.iter verifyParent (stateGetParents state)
       end
     in
 
@@ -219,7 +223,7 @@ let propagateSatMu () =
         List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
       in
       if not (List.exists ruleiter (stateGetRules state)) then begin
-        setAddState allowedStates state;
+        print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node");
         visitParentCores state
       end
 
@@ -230,7 +234,7 @@ let propagateSatMu () =
       if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
                            (coreGetChildren core))
       then begin
-        setAddCore allowedCores core;
+        print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node");
         visitParentStates core
       end
     in