# HG changeset patch
# User blanchet
# Date 1657544644 -7200
# Node ID 707748d3d1866c38ec3821360a808ecb6225b292
# Parent  a65c4539dedbf77efa13780e104c2f7bbd4059a5
prefer non-JNI SAT solvers by default in Nitpick

diff -r a65c4539dedb -r 707748d3d186 NEWS
--- a/NEWS	Mon Jul 11 15:03:42 2022 +0200
+++ b/NEWS	Mon Jul 11 15:04:04 2022 +0200
@@ -126,6 +126,9 @@
 * Theory "HOL-Library.Sublist":
   - Added lemma map_mono_strict_suffix.
 
+* Nitpick: To avoid technical issues, prefer non-JNI solvers to JNI solvers by
+  default. Minor INCOMPATIBILITY.
+
 * Sledgehammer:
   - Redesigned multithreading to provide more fine grained prover schedules.
     The binary option 'slice' has been replaced by a numeric value 'slices'
diff -r a65c4539dedb -r 707748d3d186 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Jul 11 15:03:42 2022 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Jul 11 15:04:04 2022 +0200
@@ -30,11 +30,8 @@
 val berkmin_exec = getenv "BERKMIN_EXE"
 
 val static_list =
-  [("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
-   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
-   ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
+  [("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")),
-   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
@@ -47,7 +44,10 @@
                            "solution =", "UNSATISFIABLE          !!")),
    ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
-   ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
+   ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"])),
+   ("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
+   ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
+   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"]))]
 
 fun dynamic_entry_for_external name dev home exec args markers =
   let