# HG changeset patch
# User krauss
# Date 1303139267 -7200
# Node ID 13798dcbdca53f7d967f68d2e7d6159e8af33758
# Parent  0869ce2006eb6822027780fc06e5e00d406da162
raised timeouts further, for SML/NJ!

diff -r 0869ce2006eb -r 13798dcbdca5 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Apr 18 16:33:45 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Apr 18 17:07:47 2011 +0200
@@ -51,7 +51,7 @@
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
 (*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*)
-quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = counterexample]
+quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample]
 oops
 
 
diff -r 0869ce2006eb -r 13798dcbdca5 src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Mon Apr 18 16:33:45 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Mon Apr 18 17:07:47 2011 +0200
@@ -26,7 +26,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample]
 oops
 
 
diff -r 0869ce2006eb -r 13798dcbdca5 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Mon Apr 18 16:33:45 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Mon Apr 18 17:07:47 2011 +0200
@@ -29,7 +29,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample]
 oops