raised timeouts further, for SML/NJ!
authorkrauss
Mon Apr 18 17:07:47 2011 +0200 (2011-04-18)
changeset 4239713798dcbdca5
parent 42396 0869ce2006eb
child 42398 919e17c0358e
child 42412 4a929b0630c3
raised timeouts further, for SML/NJ!
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
src/HOL/Predicate_Compile_Examples/IMP_1.thy
src/HOL/Predicate_Compile_Examples/IMP_2.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Apr 18 16:33:45 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Apr 18 17:07:47 2011 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  lemma
     1.5    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
     1.6  (*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*)
     1.7 -quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = counterexample]
     1.8 +quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample]
     1.9  oops
    1.10  
    1.11  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Mon Apr 18 16:33:45 2011 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Mon Apr 18 17:07:47 2011 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  
     2.5  lemma
     2.6    "exec c s s' ==> exec (Seq c c) s s'"
     2.7 -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
     2.8 +quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample]
     2.9  oops
    2.10  
    2.11  
     3.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Mon Apr 18 16:33:45 2011 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Mon Apr 18 17:07:47 2011 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  lemma
     3.6    "exec c s s' ==> exec (Seq c c) s s'"
     3.7 -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10]
     3.8 +quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample]
     3.9  oops
    3.10  
    3.11