# 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. \ -declare [[smt_timeout = 20]] +declare [[smt_timeout = 1000000]] text \ 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>\smt_oracle\ (K true) -val timeout = Attrib.setup_config_real \<^binding>\smt_timeout\ (K 30.0) +val timeout = Attrib.setup_config_real \<^binding>\smt_timeout\ (K 1000000.0) val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\smt_reconstruction_step_timeout\ (K 10.0) val random_seed = Attrib.setup_config_int \<^binding>\smt_random_seed\ (K 1) val read_only_certificates = Attrib.setup_config_bool \<^binding>\smt_read_only_certificates\ (K false)