diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 0035ba3a9304d61fb56696addfd46a4ef0f626de..6a54b71fdf7213bb37ba1cd9a570333c51ea9500 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -216,7 +216,7 @@ let propagateSatMu () =
      *)
     let checkFinishingState (state : state) =
       let ruleiter (dependencies, corelist) : bool =
-        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
+        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;
@@ -227,7 +227,7 @@ let propagateSatMu () =
      * to be considered for the fixpoint
      *)
     and checkFinishingCore (core : core) =
-      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
+      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;