1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 09:28:03 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 15:32:30 2012 +0200
1.3 @@ -226,7 +226,7 @@
1.4 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
1.5 timeout, it makes sense to put E first. *)
1.6 fun default_provers_param_value ctxt =
1.7 - [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
1.8 + [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
1.9 |> map_filter (remotify_prover_if_not_installed ctxt)
1.10 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
1.11 max_default_remote_threads)
1.12 @@ -404,11 +404,11 @@
1.13 else
1.14 ();
1.15 mash_learn ctxt (get_params Normal ctxt
1.16 - (("timeout",
1.17 - [string_of_real default_learn_atp_timeout]) ::
1.18 + ([("timeout",
1.19 + [string_of_real default_learn_atp_timeout]),
1.20 + ("slice", ["false"])] @
1.21 override_params @
1.22 - [("slice", ["false"]),
1.23 - ("minimize", ["true"]),
1.24 + [("minimize", ["true"]),
1.25 ("preplay_timeout", ["0"])]))
1.26 fact_override (#facts (Proof.goal state))
1.27 (subcommand = learn_atpN orelse subcommand = relearn_atpN))