diff -r 86a1f61d260e -r f643399acab3 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Nov 22 14:19:03 2010 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Nov 22 14:27:42 2010 +0100 @@ -50,8 +50,8 @@ lemma "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample] -quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample] +quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60] +quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60] oops