diff -r 65cd285f6b9c -r 45d3d43abee7 src/HOL/Nunchaku/Tools/nunchaku.ML
--- a/src/HOL/Nunchaku/Tools/nunchaku.ML	Thu Jun 22 10:50:18 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML	Thu Jun 22 16:59:14 2017 +0200
@@ -12,7 +12,8 @@
   datatype mode = Auto_Try | Try | Normal
 
   type mode_of_operation_params =
-    {falsify: bool,
+    {solvers: string list,
+     falsify: bool,
      assms: bool,
      spy: bool,
      overlord: bool,
@@ -74,7 +75,8 @@
 datatype mode = Auto_Try | Try | Normal;
 
 type mode_of_operation_params =
-  {falsify: bool,
+  {solvers: string list,
+   falsify: bool,
    assms: bool,
    spy: bool,
    overlord: bool,
@@ -138,7 +140,7 @@
 val timeout_slack = seconds 1.0;
 
 fun run_chaku_on_prop state
-    ({mode_of_operation_params = {falsify, assms, spy, overlord, expect},
+    ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect},
       scope_of_search_params = {wfs, whacks, cards, monos},
       output_format_params = {verbose, debug, evals, atomss, ...},
       optimization_params = {specialize, ...},
@@ -157,8 +159,9 @@
     val das_wort_Model = if falsify then "Countermodel" else "Model";
     val das_wort_model = if falsify then "countermodel" else "model";
 
-    val tool_params = {overlord = overlord, debug = debug, specialize = specialize,
-      timeout = timeout};
+    val tool_params =
+      {solvers = solvers, overlord = overlord, debug = debug, specialize = specialize,
+       timeout = timeout};
 
     fun run () =
       let