diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index ed0d2dec09b06b3199dbf3d71ecc2b5c6cf44f5b..3358f6c48ce55bac98779ca49b682d7894b69566 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -578,6 +578,8 @@ let coreAddConstraintParent core cset =
 
 let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
 let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
+let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
+let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
 let setEmptyCnstr () = GHtS.create 128
 let setAddState set state =
   GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 9c25e6c892a3880c11d8d26a5988728c98edfda7..80a0eb85b23df3de98271c189802a4ddbf54a3f8 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -267,6 +267,8 @@ val coreToDot : core -> string
 
 val setEmptyState : unit -> setState
 val setEmptyCore : unit -> setCore
+val setCopyState : setState -> setState
+val setCopyCore : setCore -> setCore
 val setEmptyCnstr : unit -> setCnstr
 val setAddState : setState -> state -> unit
 val setAddCore : setCore -> core -> unit
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 91e04c792b00bfef8d45c198d30674a548e6e88b..ab63f46c81f10ccb5e4f8eaced297e205edc7304 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -411,6 +411,133 @@ let rec propagateUnsat = function
       in
       propagateUnsat tl1
 
+let propateUnsatMu () =
+  let setFinishingStates = setEmptyState () in
+  let setFinishingCores = setEmptyCore () in
+  let setStates = setEmptyState () in
+  let setCores = setEmptyCore () in
+  let emptySet = bsetMakeRealEmpty () in
+
+  (* Collect two sets of nodes. All nodes that may be unsatisfiable
+   * after this iteration are collected into setStates/setCores.
+   *
+   * Nodes reaching Points with empty focus as well as Expandable nodes
+   * (if not Unsat) can not be declared Unsat so we collect these into
+   * setFinishingStates/setFinishingCores.
+   *)
+  let stateCollector state =
+    match stateGetStatus state with
+    | Unsat -> ()
+    | Sat
+    | Expandable ->
+       setAddState setStates state;
+      setAddState setFinishingStates state
+    | Open ->
+       setAddState setStates state;
+      if bsetCompare (stateGetDeferral state) emptySet == 0
+      then begin
+        setAddState setFinishingStates state
+      end
+      else ()
+
+  and coreCollector core =
+    match coreGetStatus core with
+    | Unsat -> ()
+    | Expandable
+    | Sat ->
+       setAddCore setCores core;
+      setAddCore setFinishingCores core
+    | Open ->
+       setAddCore setCores core;
+      if bsetCompare (coreGetDeferral core) emptySet == 0
+      then begin
+        setAddCore setFinishingCores core
+      end
+      else ()
+  in
+  graphIterStates stateCollector;
+  graphIterCores coreCollector;
+
+  (* In a fixpoint the set called setFinishingStates/setFinishingCores
+   * is narrowed down
+   *
+   * In each iteration we start with all Nodes and remove all that can
+   * reach a finishing Node. We then remove all finishing Nodes from the
+   * respective set which are becoming Unsat and start with the next
+   * iteration until the fixpoint is reached
+   *
+   *
+   *)
+  let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
+    let setUnsatStates = setCopyState setStates in
+    let setUnsatCores = setCopyCore setCores in
+
+    let rec visitParentStates (core : core) : unit =
+      if setMemCore setUnsatCores core
+      then begin
+        setRemoveCore setUnsatCores core;
+        let verifyParent (state,_) =
+          let rules = stateGetRules state in
+          let ruleiter (dependencies, corelist) =
+            List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat)
+              corelist
+          in
+          if List.for_all ruleiter rules
+          then visitParentCores state
+        in
+        List.iter verifyParent (coreGetParents core)
+      end
+
+    and visitParentCores (state : state) : unit =
+      if setMemState setUnsatStates state
+      then begin
+        setRemoveState setUnsatStates state;
+        let verifyParent core =
+          let acceptable =
+            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat)
+              (coreGetChildren core)
+          in
+          if acceptable
+          then visitParentStates core
+        in
+        List.iter verifyParent (stateGetParents state)
+      end
+    in
+
+    (* All rule applications need to still be potentially Sat for a
+     * finishing State to be a valid startingpoint for this fixpoint.
+     *)
+    let checkFinishingState (state : state) =
+      let ruleiter (dependencies, corelist) : bool =
+        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist
+      in
+      if not (List.exists ruleiter (stateGetRules state)) then begin
+        visitParentCores state
+      end
+
+    (* There needs to be a State still potentially Sat for this core
+     * to be considered for the fixpoint
+     *)
+    and checkFinishingCore (core : core) =
+      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state)
+                           (coreGetChildren core))
+      then begin
+        visitParentStates core
+      end
+    in
+    setIterState checkFinishingState setFinishingStates;
+    setIterCore checkFinishingCore setFinishingCores;
+
+    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
+      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
+    then begin
+        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
+        setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot () then raise (CoAlg_finished false) else ()) setUnsatCores;
+      end else
+      fixpointstep setUnsatStates setUnsatCores
+  in
+  fixpointstep (setEmptyState ()) (setEmptyCore ())
+
 
 (*****************************************************************************)
 (*                   Propagation of Nominal Constraints                      *)