# HG changeset patch
# User blanchet
# Date 1504826073 -7200
# Node ID 809d40cfa4deaa15fc6255f68060ec96e6da7da4
# Parent  6585669c33dc39dea07747e5b78061c8835944d1
correctly locate SMBC from Nunchaku

diff -r 6585669c33dc -r 809d40cfa4de src/HOL/Nunchaku.thy
--- 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
diff -r 6585669c33dc -r 809d40cfa4de src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- 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) ^ "\" " ^