diff --git a/configure.ac b/configure.ac
index aaef572656d5e249dc8b1e5b50e284cc9c63ca33..04d6ac0ca3a0d0722451f77f4231112db6ef4a6f 100644
--- a/configure.ac
+++ b/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)
diff --git a/include/z3librc.in b/include/z3librc.in
index ee0b231e187db683387ea17e12de9f001d194983..26843ee971ef971b916b28ddb99d6878ebb4299a 100644
--- a/include/z3librc.in
+++ b/include/z3librc.in
@@ -1 +1,2 @@
 export LD_LIBRARY_PATH=@Z3LIBPATH@:$LD_LIBRARY_PATH
+export DYLD_LIBRARY_PATH=@Z3LIBPATH@:$DYLD_LIBRARY_PATH
diff --git a/src/_tags.in b/src/_tags.in
index 235bf5681bfd00b37c307248f2a25b01040081bc..98c554d9d1de4f7ff8cbf2bcb477fe6f509a65e7 100644
--- a/src/_tags.in
+++ b/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@