src/HOL/Tools/Sledgehammer/sledgehammer.ML

           | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
           | SOME (SMT_Failure.Solver_Crashed code) =>
             (if verbose then
                "The SMT solver invoked with " ^ string_of_int num_facts ^
                " fact" ^ plural_s num_facts ^ " terminated abnormally with \
-               \exit code " ^ string_of_int code
+               \exit code " ^ string_of_int code ^ "."
                |> (if debug then error else warning)
              else
                ();
              true (* kind of *))
           | SOME SMT_Failure.Out_Of_Memory => true