# HG changeset patch
# User wenzelm
# Date 1316613869 -7200
# Node ID 33a1af99b3a2e4d5aadf4b24f4dbaa9a25f94ce1
# Parent  77c3e74bd954a8d6ea3d35fbbbfc6cff2284b64d
more hints on Z3 configuration;

diff -r 77c3e74bd954 -r 33a1af99b3a2 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Sep 21 15:08:15 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Sep 21 16:04:29 2011 +0200
@@ -125,9 +125,10 @@
       error ("The SMT solver Z3 may only be used for non-commercial " ^
         "applications.")
   | Z3_Non_Commercial_Unknown =>
-      error ("The SMT solver Z3 is not activated. To activate it, set " ^
-        "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
-        "."))
+      error ("The SMT solver Z3 is not activated. To activate it, set\n" ^
+        "the environment variable " ^ quote flagN ^ " to " ^ quote "yes" ^ "." ^
+        (if getenv "Z3_COMPONENT" = "" then ""
+         else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings")))))
 
 end