Adapt domain with non-EDD disjunctions ; it doesn't work very well !

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