--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 06 17:58:03 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 06 17:19:34 2011 +0100
@@ -326,7 +326,10 @@
formats = [FOF],
best_slices =
(* FUDGE (FIXME) *)
- K [(1.0, (false, (250, "mangled_preds?", "")))]}
+ K [(0.5, (false, (250, "mangled_preds?", ""))),
+ (0.25, (false, (125, "mangled_preds?", ""))),
+ (0.125, (false, (62, "mangled_preds?", ""))),
+ (0.125, (false, (31, "mangled_preds?", "")))]}
val z3_atp = (z3_atpN, z3_atp_config)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 06 17:58:03 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 06 17:19:34 2011 +0100
@@ -529,7 +529,7 @@
(* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
Linux appears to be the only ATP that does not honor its time limit. *)
-val atp_timeout_slack = seconds 5.0
+val atp_timeout_slack = seconds 1.0
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,