Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Fri, 12 Sep 2025 22:42:03 +0200
changeset 83145 c3c278374b5b
parent 83137 4b9311a5b7e3 (diff)
parent 83144 de5f468de460 (current diff)
child 83146 87c96d455992
merged
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 12 21:58:41 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 12 22:42:03 2025 +0200
@@ -318,10 +318,9 @@
       SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
         (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
     | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) =>
-        (SMT_Config.verbose_msg ctxt (K ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^
+        error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^
           SMT_Failure.string_of_failure fail ^ " (setting the " ^
-          "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")) ();
-         NONE)
+          "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")
     | SMT_Failure.SMT fail => error (str_of ctxt fail)
 
   fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
isabelle