# HG changeset patch
# User krauss
# Date 1301902370 -7200
# Node ID 02513eb26eb70da3cb54daa4d960e0b1bcc2062c
# Parent  2bda5eddadf3895507cec0c72c7c18ff777ad9e2
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.

diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 subsection {* Curry in a Hurry *}
 
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 primrec rot where
 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -13,7 +13,7 @@
 begin
 
 nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
-                max_threads = 1, timeout = 120]
+                max_threads = 1, timeout = 240]
 
 typedecl guest
 typedecl key
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "Suc x = x + 1"
 nitpick [unary_ints, expect = none]
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -18,7 +18,7 @@
 chapter {* 3. First Steps *}
 
 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60]
+                timeout = 240]
 
 subsection {* 3.1. Propositional Logic *}
 
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
-                max_threads = 1, timeout = 60]
+                max_threads = 1, timeout = 240]
 
 lemma "x = (case u of () \<Rightarrow> y)"
 nitpick [expect = genuine]
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 record point2d =
   xc :: int
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "P \<and> Q"
 apply (rule conjI)
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60]
+                timeout = 240]
 
 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
 "f1 a b c d e = a + b + c + d + e"
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60]
+                timeout = 240]
 
 typedef three = "{0\<Colon>nat, 1, 2}"
 by blast
@@ -159,7 +159,7 @@
 by (rule Rep_Nat_inverse)
 
 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, timeout = 240, expect = none]
+nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
 by (rule Zero_int_def_raw)
 
 lemma "Abs_list (Rep_list a) = a"
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -2,7 +2,7 @@
 imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
 
 section {* Formal Languages *}
 
diff -r 2bda5eddadf3 -r 02513eb26eb7 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Apr 04 09:32:50 2011 +0200
@@ -2,7 +2,7 @@
 imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
 
 subsection {* Basic predicates *}