--- a/src/HOL/SMT.thy Tue Sep 08 11:32:57 2020 +0200
+++ b/src/HOL/SMT.thy Wed Sep 30 18:37:22 2020 +0200
@@ -346,7 +346,7 @@
(given in seconds) to restrict their runtime.
\<close>
-declare [[smt_timeout = 20]]
+declare [[smt_timeout = 1000000]]
text \<open>
SMT solvers apply randomized heuristics. In case a problem is not
--- a/src/HOL/Tools/SMT/smt_config.ML Tue Sep 08 11:32:57 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Sep 30 18:37:22 2020 +0200
@@ -174,7 +174,7 @@
(* options *)
val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
-val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 30.0)
+val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 1000000.0)
val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)