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