Catch Step_limit_reached consistently with Timeout

This is a partial fix for OCamlPro#1244 that only addresses the fatal error
issue, but not incrementality.

Author: bclement-ocp

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

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 =