Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning options to avoid spurious isabelle test failures
authorbulwahn
Wed, 06 Jul 2011 13:52:42 +0200
changeset 43686 bc7d63c7fd6f
parent 43656 9ece73262746
child 43687 2882832b8d89
tuning options to avoid spurious isabelle test failures
src/HOL/Predicate_Compile_Examples/IMP_1.thy file | annotate | diff | comparison | revisions
src/HOL/Predicate_Compile_Examples/IMP_2.thy file | annotate | diff | comparison | revisions
src/HOL/Predicate_Compile_Examples/IMP_3.thy file | annotate | diff | comparison | revisions
src/HOL/Predicate_Compile_Examples/IMP_4.thy file | annotate | diff | comparison | revisions
src/HOL/ex/SML_Quickcheck_Examples.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Sun Jul 03 09:59:25 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Wed Jul 06 13:52:42 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, timeout = 600.0, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Sun Jul 03 09:59:25 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Wed Jul 06 13:52:42 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, timeout = 600.0, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Sun Jul 03 09:59:25 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Wed Jul 06 13:52:42 2011 +0200
@@ -29,8 +29,8 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-  quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
+  quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=100, quiet = false, expect = counterexample]
 oops
 
 
-end
\ No newline at end of file
+end
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Sun Jul 03 09:59:25 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Wed Jul 06 13:52:42 2011 +0200
@@ -30,7 +30,7 @@
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
   nitpick (* nitpick fails here! *)
-  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
+  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=100, expect=counterexample]
 oops
 
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/SML_Quickcheck_Examples.thy	Sun Jul 03 09:59:25 2011 +0200
+++ b/src/HOL/ex/SML_Quickcheck_Examples.thy	Wed Jul 06 13:52:42 2011 +0200
@@ -16,6 +16,7 @@
 *}
 
 declare [[quickcheck_finite_types = false]]
+declare [[quickcheck_timeout = 600.0]]
 
 subsection {* Lists *}
 
@@ -139,4 +140,4 @@
   --{* Wrong! *} 
   oops
 
-end
\ No newline at end of file
+end
isabelle