diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 690814e58f08f4259b1db8ae66e7afe037c0e895..f24844e9fec7a23036dd9d8e22da51c2a2997282 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -1080,6 +1080,7 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
   let sat =
     try
       buildGraphLoop ();
+      propagateUnsatMu ();
       (* get whether the root is satisfiable *)
       (* we know that the reasoner finished, so the value is there, *)
       (* i.e. isRootSat() will give a "Some x" and not "None" *)