merged
authorblanchet
Thu, 23 Jun 2011 16:31:20 +0200
changeset 43530 f05a707fdf91
parent 43529 359fa511662c (diff)
parent 43527 1aacef7471c2 (current diff)
child 43531 cc46a678faaf
merged
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jun 23 12:02:54 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jun 23 16:31:20 2011 +0200
@@ -406,7 +406,7 @@
                (K (750, ["mangled_tags?"]) (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-               (K (150, ["mangled_preds?"]) (* FUDGE *))
+               (K (200, ["mangled_preds?"]) (* FUDGE *))
 val remote_z3_atp =
   remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *))
 val remote_leo2 =
@@ -418,7 +418,7 @@
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
              Axiom Conjecture [FOF]
-             (K (500, ["poly_tags_heavy"]) (* FUDGE *))
+             (K (500, ["mangled_preds?"]) (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jun 23 12:02:54 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jun 23 16:31:20 2011 +0200
@@ -94,7 +94,7 @@
 $Agent->env_proxy;
 if (exists($Options{'t'})) {
   # give server more time to respond
-  $Agent->timeout($Options{'t'} + 10);
+  $Agent->timeout($Options{'t'} + 15);
 }
 my $Request = POST($SystemOnTPTPFormReplyURL,
 	Content_Type => 'form-data',Content => \%URLParameters);