Project

General

Profile

Revision 3d3718ae

View differences:

configure.ac
79 79

  
80 80
# z3
81 81
AC_MSG_CHECKING(z3 library (optional))
82
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
83
define([z3path], esyscmd([opam config var z3:lib | tr -d '\n']))
82
define([z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
83
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
84 84

  
85
AS_IF([ocamlfind query z3 >/dev/null 2>&1],
85
AS_IF([ocamlfind query Z3 >/dev/null 2>&1],
86 86
    [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
87 87
)
88 88
AS_IF([test "x$z3" = "xyes"], [
89 89
   AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
90
   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)")
90
   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(Z3)")
91 91
   AC_SUBST(Z3LIBPATH, "z3path")
92 92
])
93 93

  
src/tools/zustre/zustre_analyze.ml
203 203
  match res_status with
204 204
  | Z3.Solver.SATISFIABLE -> (
205 205
     (*Zustre_cex.build_cex decl_err*)
206
     let expr_opt = Z3.Fixedpoint.get_answer !fp in
207
       match expr_opt with
208
	 None -> Format.eprintf "Sat No feedback@."
209
       | Some e -> Format.eprintf "Sat Result: %s@." (Z3.Expr.to_string e)
206
    let expr1_opt = Z3.Fixedpoint.get_answer !fp in
207
    let expr2_opt = Z3.Fixedpoint.get_ground_sat_answer !fp in 
208
       match expr1_opt, expr2_opt with
209
	 None, None -> Format.eprintf "Sat No feedback@."
210
       | Some e, Some e2 -> Format.eprintf "Sat Result: %s, %s@."
211
					   (Z3.Expr.to_string e)
212
					   (Z3.Expr.to_string e2)
213
       | _ -> assert false
210 214
  )
211 215
  | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
212 216
       let expr_opt = Z3.Fixedpoint.get_answer !fp in

Also available in: Unified diff