# HG changeset patch
# User wenzelm
# Date 1598282381 -7200
# Node ID 8dc2e4d9deaa7990befe9a2c1f183ed934e93994
# Parent  7ffa26f05c723631c1c8e9cb90e5b9e88a36c190
proper default for max_threads;
proper warmup example;

diff -r 7ffa26f05c72 -r 8dc2e4d9deaa src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Mon Aug 24 13:39:09 2020 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Mon Aug 24 17:19:41 2020 +0200
@@ -35,9 +35,10 @@
     max_solutions: Int = Integer.MAX_VALUE,
     cleanup_inst: Boolean = false,
     timeout: Time = Time.zero,
-    max_threads: Int = 1): Result =
+    max_threads: Int = 0): Result =
   {
-    val executor = Executors.newFixedThreadPool(max_threads)
+    val executor =
+      Executors.newFixedThreadPool(if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads)
 
     def executor_kill(): Unit =
       if (!executor.isShutdown) Isabelle_Thread.fork() { executor.shutdownNow() }
@@ -105,7 +106,7 @@
 
   def warmup(): String =
     execute(
-      """solver: "MiniSat\n"""" +
+      "solver: \"MiniSat\"\n" +
       File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check