diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index 30c71fb3ca..fc34241ef2 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -444,7 +444,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
           (* If we have reached an unknown state, we can return it right
              away. *)
           match SAT.get_unknown_reason env.sat_env with
-          | Some (Step_limit _) -> raise SAT.I_dont_know
+          | Some (Step_limit _ | Timeout _)  -> raise SAT.I_dont_know
           | Some _ ->
             (* For now, only the step limit is an unknown step reachable
                here. We could raise SAT.I_dont_know as in the previous case,
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 7d89862bcf..40d274ec0a 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1030,7 +1030,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
             env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *)
         with
         (* We raised an exception. This can come from four sources:
-           - we raised I_dont_know
+           - we raised I_dont_know (legit)
            - we raised Unsat -> maybe unsound, returning I_dont_know
            - we broke an invaraiant because the timeout happened during a
            critical instruction and now the environment is invalid. *)