Project

General

Profile

Revision 3d3718ae src/tools/zustre/zustre_analyze.ml

View differences:

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