Revision 3d3718ae src/tools/zustre/zustre_analyze.ml
| 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