# HG changeset patch
# User blanchet
# Date 1386247100 -3600
# Node ID 86e0b402994c4239acb0109ecf5d53157a4bca80
# Parent  7a14f831d02d35cde346bd7e36efab09f4c0762b
experiment

diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<emdash>6, unary_ints, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 subsection {* Curry in a Hurry *}
 
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<emdash>8, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 primrec rot where
 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
+nitpick_params [verbose, max_potential = 0, sat_solver = Riss3g,
                 max_threads = 1, timeout = 240]
 
 typedecl guest
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 lemma "Suc x = x + 1"
 nitpick [unary_ints, expect = none]
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -17,7 +17,7 @@
 
 chapter {* 2. First Steps *}
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+nitpick_params [sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 subsection {* 2.1. Propositional Logic *}
 
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -13,7 +13,7 @@
 
 ML_file "minipick.ML"
 
-nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
+nitpick_params [verbose, sat_solver = Riss3g, max_threads = 1]
 
 nitpick_params [total_consts = smart]
 
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = MiniSat_JNI,
+nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = Riss3g,
                 max_threads = 1, timeout = 240]
 
 lemma "x = (case u of () \<Rightarrow> y)"
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 record point2d =
   xc :: int
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = Riss3g, max_threads = 1, timeout = 240]
 
 lemma "P \<and> Q"
 apply (rule conjI)
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 4, sat_solver = Riss3g, max_threads = 1,
                 timeout = 240]
 
 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
diff -r 7a14f831d02d -r 86e0b402994c src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Dec 05 13:22:00 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Dec 05 13:38:20 2013 +0100
@@ -11,7 +11,7 @@
 imports Complex_Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 1\<emdash>4, sat_solver = Riss3g, max_threads = 1,
                 timeout = 240]
 
 definition "three = {0\<Colon>nat, 1, 2}"