--- 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]
*)
--- 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>
--- 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
--- 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
--- 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" |
--- 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]
--- 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>
--- 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>
--- 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)"
--- 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
--- 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)
--- 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
--- 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}"