# HG changeset patch
# User wenzelm
# Date 1635615669 -7200
# Node ID 6f801e1073fa8f995362df2e12d48aba0057476e
# Parent  85d8d9eeb4e180ece1e78b6f4220dadb677cdc30
prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms;

diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -23,7 +23,7 @@
 quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
 
 (*
-nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
+nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
 refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
 *)
 
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1-6, unary_ints, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 subsection \<open>Curry in a Hurry\<close>
 
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1-8, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3
   | Nibble4 | Nibble5 | Nibble6 | Nibble7
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -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 = MiniSat,
                 max_threads = 1, timeout = 240]
 
 typedecl guest
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1-8, unary_ints,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1-5, bits = 1,2,3,4,6,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 lemma "Suc x = x + 1"
 nitpick [unary_ints, expect = none]
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -17,7 +17,7 @@
 
 section \<open>2. First Steps\<close>
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+nitpick_params [sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 
 subsection \<open>2.1. Propositional Logic\<close>
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -13,8 +13,7 @@
 
 ML_file \<open>minipick.ML\<close>
 
-nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
-  total_consts = smart]
+nitpick_params [verbose, sat_solver = MiniSat, max_threads = 1, total_consts = smart]
 
 ML \<open>
 val check = Minipick.minipick \<^context>
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -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 = MiniSat,
                 max_threads = 1, timeout = 240]
 
 lemma "x = (case u of () \<Rightarrow> y)"
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1-6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 record point2d =
   xc :: int
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -12,7 +12,7 @@
 begin
 
 nitpick_params [verbose, card = 1-6, max_potential = 0,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+                sat_solver = MiniSat, max_threads = 1, timeout = 240]
 
 lemma "P \<and> Q"
 apply (rule conjI)
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -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 = MiniSat, max_threads = 1,
                 timeout = 240]
 
 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
diff -r 85d8d9eeb4e1 -r 6f801e1073fa src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Oct 30 19:23:01 2021 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Oct 30 19:41:09 2021 +0200
@@ -11,7 +11,7 @@
 imports Complex_Main
 begin
 
-nitpick_params [verbose, card = 1-4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 1-4, sat_solver = MiniSat, max_threads = 1,
                 timeout = 240]
 
 definition "three = {0::nat, 1, 2}"