diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 35bdbfb..8ea0012 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -936,6 +936,14 @@ end = struct let init_cl = Formula.conslist_of_f init_f in Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; + let guarantees = Transform.guarantees_of_prog rp in + Format.printf "Guarantees:@."; + List.iter (fun (id, f) -> + Format.printf " %s: %a@." id Formula_printer.print_expr f) + guarantees; + Format.printf "@."; + + (* add variables from LASTs *) let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in let last_vars = List.map (fun id -> @@ -955,12 +963,6 @@ end = struct | TReal -> (id, true)::nv, ev) ([], []) all_vars in - let guarantees = Transform.guarantees_of_prog rp in - Format.printf "Guarantees:@."; - List.iter (fun (id, f) -> - Format.printf " %s: %a@." id Formula_printer.print_expr f) - guarantees; - Format.printf "@."; (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in |