| 1234567891011121314151617181920212223 |
- --- Isabelle2016-1-orig/src/HOL/SMT.thy 2016-12-13 01:03:38.000000000 +1100
- +++ Isabelle2016-1/src/HOL/SMT.thy 2016-12-30 14:11:09.379863215 +1100
- @@ -201,7 +201,7 @@
- (given in seconds) to restrict their runtime.
- \<close>
-
- -declare [[smt_timeout = 20]]
- +declare [[smt_timeout = 300]]
-
- text \<open>
- SMT solvers apply randomized heuristics. In case a problem is not
- --- Isabelle2016-1-orig/src/HOL/Tools/SMT/smt_config.ML 2016-12-13 01:03:42.000000000 +1100
- +++ Isabelle2016-1/src/HOL/Tools/SMT/smt_config.ML 2016-12-30 14:11:27.186904132 +1100
- @@ -170,7 +170,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 300.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)
|
