diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index c51625a2f91707e4bb529c05644341be1a019b78..b2366bdeb2f791fe76cabc46531e98b509a88af8 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -52,9 +52,11 @@ let doStep args =
     let action() =
         if Reasoner.reasonerFinished ()
         then print_endline "Reasoner already finished!"
-        else try
-                Reasoner.runReasonerStep ()
-             with CoAlgMisc.CoAlg_finished _ -> printResult()
+        else
+          try
+            Reasoner.runReasonerStep ();
+            if (Reasoner.reasonerFinished ()) then printResult();
+          with CoAlgMisc.CoAlg_finished _ -> printResult()
     in
     let steps = match args with
                 | (str::_) -> (int_of_string str)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 93d7761cf373917a2f9d15ab37a04a9ae56ce3d1..fca69aaf78c08132e7c8dc9bff98cc8815e9c440 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -1035,6 +1035,7 @@ let expandNodesLoop (recursiveAction: unit -> unit) =
 let runReasonerStep () =
   let void () = () in
   expandNodesLoop void; (* expand at most one node *)
+  propagateUnsatMu ();
   (* if this emptied the queue *)
   if queueIsEmpty () then begin
     (* then check whether the nominals would add further queue elements *)
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index b63083dbd7d80584bc21f14a08eafd227f040394..a30ed9311bc0cbcc59cb4a063b88390c998a932e 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/src/lib/CoAlgReasoner.mli
@@ -20,7 +20,13 @@ val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) -
 val initReasoner : sortTable -> (string -> CoAlgFormula.sort option) ->
   CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> unit
 
+(** Run a single step of the reasoner. That is: Expand one node and perform sat
+  * propagation.
+  *
+  * This is used in the debugger.
+  *)
 val runReasonerStep : unit -> unit
+
 val reasonerFinished : unit -> bool
 val isRootSat : unit -> bool option