--- a/src/HOL/Nunchaku.thy Fri Sep 08 00:58:08 2017 +0200
+++ b/src/HOL/Nunchaku.thy Fri Sep 08 01:14:33 2017 +0200
@@ -11,7 +11,7 @@
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4 and Kodkodi are necessary to use these backend solvers.
+for CVC4, Kodkodi, and SMBC are necessary to use these backend solvers.
*)
theory Nunchaku
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Sep 08 00:58:08 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Sep 08 01:14:33 2017 +0200
@@ -95,7 +95,7 @@
else
let
val bash_cmd =
- "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
+ "PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
"--solvers \"" ^ space_implode "," (map Bash_Syntax.string solvers) ^ "\" " ^