diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index aebf4247e85095d6b316d8f44cd6c9b6136c96e9..91e04c792b00bfef8d45c198d30674a548e6e88b 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -120,15 +120,25 @@ let propagateSatMu () =
   let setCores = setEmptyCore () in
   let emptySet = bsetMakeRealEmpty () in
 
+  (* Collect two sets of nodes. All nodes that may be satisfiable
+   * after this iteration are collected into setStates/setCores.
+   *
+   * As every cycle containing a node with empty focus or an
+   * satisfiable node should be considered satisfiable, collect these
+   * decisive nodes into setFinishingStates/setFinishingCores
+   *
+   * This also marks in trivial cases nodes as satisfiable.
+   *)
   let stateCollector state =
     match stateGetStatus state with
     | Unsat -> ()
     | Sat ->
        setAddState setStates state;
-       setAddState setFinishingStates state
+      setAddState setFinishingStates state
     | Expandable -> ()
     | Open ->
-       if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
+       if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *)
+         bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *)
        then begin
          setAddState setFinishingStates state;
          stateSetStatus state Sat
@@ -141,8 +151,11 @@ let propagateSatMu () =
          end
          else ()
        end
-  in
-  let coreCollector core =
+
+  (* As it is enough for a core to have one successfull child, we can
+   * also handle (some) expandable cores.
+   *)
+  and coreCollector core =
     match coreGetStatus core with
     | Unsat -> ()
     | Sat ->
@@ -151,28 +164,27 @@ let propagateSatMu () =
     | Expandable
     | Open ->
        setAddCore setCores core;
-       if bsetCompare (coreGetDeferral core) emptySet == 0
-       then begin
-           print_endline (coreToString core);
-           setAddCore setFinishingCores core
-         end
-       else ()
+      if bsetCompare (coreGetDeferral core) emptySet == 0
+      then begin
+        print_endline (coreToString core);
+        setAddCore setFinishingCores core
+      end
+      else ()
   in
   graphIterStates stateCollector;
   graphIterCores coreCollector;
 
-  (*
-    In a fixpoint the set called setStates / setCores is narrowed down.
-
-    In each step only those states and cores are retained in setStates
-    / setCores which reach one of setFinishing{States,Cores} in
-    finitely many steps. This new set of States / Cores is collected
-    as allowed{States,Cores} during each fixpoint iteration.
-
-    Only those finishing nodes are retained that have allowed or
-    Successfull Children.
-  *)
-
+  (* In a fixpoint the set called setStates / setCores is narrowed
+   * down.
+   *
+   * In each step only those states and cores are retained in setStates
+   * / setCores which reach one of setFinishing{States,Cores} in
+   * finitely many steps. This new set of States / Cores is collected
+   * as allowed{States,Cores} during each fixpoint iteration.
+   *
+   * Only those finishing nodes are retained that have allowed or
+   * Successfull Children.
+   *)
   let rec fixpointstep setStates setCores =
     let allowedStates = setEmptyState () in
     let allowedCores = setEmptyCore () in