diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 1a878489be056ea368555978c3b95aaede8467b7..facbe456e79da3a73da02dbf47c5c56c685bd562 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -118,20 +118,18 @@ let propagateSatMu () =
   let setFinishingCores = setEmptyCore () in
   let setStates = setEmptyState () in
   let setCores = setEmptyCore () in
-  let setSatStates = setEmptyState () in
-  let setSatCores = setEmptyCore () in
   let emptySet = bsetMakeRealEmpty () in
 
   let stateCollector state =
     match stateGetStatus state with
     | Unsat -> ()
     | Sat ->
-       setAddState setSatStates state
+       setAddState setFinishingStates state
     | Expandable -> ()
     | Open ->
        if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
        then begin
-         setAddState setSatStates state;
+         setAddState setFinishingStates state;
          stateSetStatus state Sat
        end else begin
          setAddState setStates state;
@@ -147,7 +145,7 @@ let propagateSatMu () =
     match coreGetStatus core with
     | Unsat -> ()
     | Sat ->
-       setAddCore setSatCores core
+       setAddCore setFinishingCores core
     | Expandable
     | Open ->
        setAddCore setCores core;
@@ -240,8 +238,6 @@ let propagateSatMu () =
     in
     setIterState checkFinishingState setFinishingStates;
     setIterCore checkFinishingCore setFinishingCores;
-    setIterState visitParentCores setSatStates;
-    setIterCore visitParentStates setSatCores;
 
 
     if (setLengthState setStates) = (setLengthState allowedStates) &&