Issues with linking Z3 on OSX

configure.ac

@@ -108,7 +108,7 @@ AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
 )
 AS_IF([test "x$z3" = "xyes"], [
    AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
-   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package($z3name)")
+   AC_SUBST(LUSTREV_Z3_TAG, "<**/*verifier.native> or <tools/zustre/*.ml> or <tools/zustre/*.mli>: package($z3name)")
    AS_IF([test "x$z3name" = "xZ3"],
    	       [define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
 	        AC_SUBST(Z3LIBPATH, "Z3path")],
@@ -118,8 +118,6 @@ AS_IF([test "x$z3" = "xyes"], [
 ])
 
 
-
-
 # Tiny
 AC_MSG_CHECKING(tiny library (optional))
 AS_IF([ocamlfind query tiny >/dev/null 2>&1],
@@ -270,7 +268,7 @@ AC_MSG_NOTICE(********   Verifiers    ********)
 
   if (test "x$z3" = xyes); then
       AC_MSG_NOTICE([Zustre enabled])
-      AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH.)
+      AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH in OSX).)
       dnl AC_MSG_WARN(It is currently located in "z3path")
       AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
       AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)

include/z3librc.in

 export LD_LIBRARY_PATH=@Z3LIBPATH@:$LD_LIBRARY_PATH
+export DYLD_LIBRARY_PATH=@Z3LIBPATH@:$DYLD_LIBRARY_PATH

src/_tags.in

@@ -29,27 +29,29 @@ true: bin_annot, color(always)
 <**/.svn>: not_hygienic
 
 # packages
-<**/*.native>                   : package(ocamlgraph)
+<**/*.native> or <**/*.ml{,i}>         : package(num)
+<**/*.native> or <**/*.ml{,i}>         : package(ocamlgraph)
+<**/*verifier.native> or <**/*.ml{,i}> : package(yojson)
+
 <**/*.native>                   : use_str
 <**/*.native>                   : use_unix
-<utils.*>                       : use_unix
-<**/*.native>                   : package(num)
-<**/*.ml>                       : package(logs)
-<**/*.native>                   : package(logs)
-<**/*.native>                   : package(yojson)
-<tools/zustre/zustre_cex.*>                   : package(yojson)
-<**/json_parser.ml>             : package(yojson)
-<**/main_parse_json_file.*>     : package(cmdliner)
-<**/main_parse_json_file.*>     : package(fmt.tty)
-<**/main_parse_json_file.*>     : package(fmt.cli)
-<**/main_parse_json_file.*>     : package(logs.fmt)
-<**/main_parse_json_file.*>     : package(logs.cli)
-<**/main_parse_json_file.*>     : package(yojson)
-<**/test_*.*>                   : package(oUnit)
-<**/test_json*.*>               : package(yojson)
 
-# Required for ocamldoc. Otherwise failed to build
-<**/*.ml{,i}>: package(ocamlgraph)
+# <**/*.ml>                       : package(logs)
+# <**/*.native>                   : package(logs)
+# <**/*.native>                   : package(yojson)
+# <tools/zustre/zustre_cex.*>                   : package(yojson)
+# <**/json_parser.ml>             : package(yojson)
+# <**/main_parse_json_file.*>     : package(cmdliner)
+# <**/main_parse_json_file.*>     : package(fmt.tty)
+# <**/main_parse_json_file.*>     : package(fmt.cli)
+# <**/main_parse_json_file.*>     : package(logs.fmt)
+# <**/main_parse_json_file.*>     : package(logs.cli)
+# <**/main_parse_json_file.*>     : package(yojson)
+# <**/test_*.*>                   : package(oUnit)
+# <**/test_json*.*>               : package(yojson)
+
+# # Required for ocamldoc. Otherwise failed to build
+# <**/*.ml{,i}>: package(ocamlgraph)
 
 # Plugin dependencies
 @SALSA_TAG@