diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 08b5b310c0b34598b1fb917ea2139d41dd26839c..c2fda8b7d888e94ee1c910cc1c6bd0190bc208a2 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -357,6 +357,7 @@ let rec propagateUnsat = function
                 in
                 coreSetBs core mbs;
                 coreSetStatus core Unsat;
+                coreDeallocateSolver core;
                 if core == graphGetRoot () then raise (CoAlg_finished false) else ();
                 let prop acc (state, idx) =
                   let turnsUnsat =
@@ -527,7 +528,7 @@ let propagateUnsatMu () =
       (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;
+        setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
       end else
       fixpointstep setUnsatStates setUnsatCores
   in
@@ -902,9 +903,11 @@ let expandCore core =
       queueInsertCore core
   | None ->
       let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
-      if isUnsat then propagateUnsat [UCore (core, false)]
-      else coreSetStatus core Open;
-      coreDeallocateSolver core
+      if isUnsat
+      then
+          propagateUnsat [UCore (core, false)]
+      else
+          coreSetStatus core Open
 
 
 let insertCore sort bs defer =