# HG changeset patch
# User wenzelm
# Date 1601500137 -7200
# Node ID 7d3a96acae287ea0f9c3d90e6196a1ce38b5b1bd
# Parent  478b7599a1a0a953ad24ed6a55155ffb84546511# Parent  e18e15b9e2ab2a8d4c2083377c4af656228b7180
merged

diff -r e18e15b9e2ab -r 7d3a96acae28 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Sep 30 22:59:33 2020 +0200
+++ b/src/HOL/SMT.thy	Wed Sep 30 23:08:57 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
diff -r e18e15b9e2ab -r 7d3a96acae28 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Sep 30 22:59:33 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Sep 30 23:08:57 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)