package z3 to Z3 when using z3 github repo.

configure.ac

@@ -79,15 +79,15 @@ AS_IF([test "x$seal" = "xyes"], [
 
 # z3
 AC_MSG_CHECKING(z3 library (optional))
-#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
-define([z3path], esyscmd([opam config var z3:lib | tr -d '\n']))
+define([z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
+#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
 
-AS_IF([ocamlfind query z3 >/dev/null 2>&1],
+AS_IF([ocamlfind query Z3 >/dev/null 2>&1],
     [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
 )
 AS_IF([test "x$z3" = "xyes"], [
    AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
-   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)")
+   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(Z3)")
    AC_SUBST(Z3LIBPATH, "z3path")
 ])
 

src/tools/zustre/zustre_analyze.ml

@@ -203,10 +203,14 @@ let check machines node =
   match res_status with
   | Z3.Solver.SATISFIABLE -> (
      (*Zustre_cex.build_cex decl_err*)
-     let expr_opt = Z3.Fixedpoint.get_answer !fp in
-       match expr_opt with
-	 None -> Format.eprintf "Sat No feedback@."
-       | Some e -> Format.eprintf "Sat Result: %s@." (Z3.Expr.to_string e)
+    let expr1_opt = Z3.Fixedpoint.get_answer !fp in
+    let expr2_opt = Z3.Fixedpoint.get_ground_sat_answer !fp in 
+       match expr1_opt, expr2_opt with
+	 None, None -> Format.eprintf "Sat No feedback@."
+       | Some e, Some e2 -> Format.eprintf "Sat Result: %s, %s@."
+					   (Z3.Expr.to_string e)
+					   (Z3.Expr.to_string e2)
+       | _ -> assert false
   )
   | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
        let expr_opt = Z3.Fixedpoint.get_answer !fp in