# HG changeset patch
# User blanchet
# Date 1260784786 -3600
# Node ID 652719832159057a9d973f7c07def35bef111632
# Parent  61b7aa37f4b75610b2210e196b46d81aba5735c0
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits

diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [sat_solver = MiniSatJNI]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
 
 subsection {* Curry in a Hurry *}
 
diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,6 +11,8 @@
 imports Main
 begin
 
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
 primrec rot where
 "rot Nibble0 = Nibble1" |
 "rot Nibble1 = Nibble2" |
diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [show_all]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,7 +11,8 @@
 imports Main
 begin
 
-nitpick_params [card = 14]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+                card = 14]
 
 lemma "x = (case u of () \<Rightarrow> y)"
 nitpick [expect = genuine]
diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,6 +11,8 @@
 imports Main
 begin
 
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
 record point2d =
   xc :: int
   yc :: int
diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,6 +11,8 @@
 imports Main
 begin
 
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
 lemma "P \<and> Q"
 apply (rule conjI)
 nitpick [expect = genuine] 1
diff -r 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -11,7 +11,8 @@
 imports Main
 begin
 
-nitpick_params [card = 4, debug, show_consts, timeout = 10 s]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+                card = 4]
 
 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 61b7aa37f4b7 -r 652719832159 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Dec 14 10:31:35 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Dec 14 10:59:46 2009 +0100
@@ -137,7 +137,7 @@
 by (rule Inl_Rep_not_Inr_Rep)
 
 lemma "Abs_Sum (Rep_Sum a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
+nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
 by (rule Rep_Sum_inverse)
 
 lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
@@ -157,15 +157,15 @@
 by (rule Rep_Nat_inverse)
 
 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
+nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
 by (rule Zero_int_def_raw)
 
 lemma "Abs_Integ (Rep_Integ a) = a"
-nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
+nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
 by (rule Rep_Integ_inverse)
 
 lemma "Abs_list (Rep_list a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
+nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
 by (rule Rep_list_inverse)
 
 record point =