diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index d2d437024..c730a88d5 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -523,6 +523,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
          or to increase your timeouts. \
          Returned unknown reason = %a@]"
         Sat_solver_sig.pp_ae_unknown_reason_opt ur;
+      Fmt.pf ppf "()"
 
     | Some model ->
       Models.pp ppf model
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 2200a8e0a..c0b448983 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1165,6 +1165,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     with
     | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
     | Util.Timeout -> i_dont_know env (Timeout ProofSearch)
+    | Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
     | Satml.Sat ->
       try
         do_case_split env Util.BeforeMatching;
@@ -1205,6 +1206,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
       with
       | Util.Timeout -> i_dont_know env (Timeout ProofSearch)
+      | Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
       | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
       | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*)
         begin
@@ -1214,6 +1216,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           with
           | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
           | Util.Timeout -> i_dont_know env (Timeout ProofSearch)
+          | Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
         end
 
   let rec unsat_rec_prem env ~first_call : unit =