Fix assertions ; fix environment equality test ; fix varialbe removal.HEADmaster

1 files changed, 5 insertions, 5 deletions

diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
index 926d2a9..4541b0e 100644
--- a/abstract/relational_apron.ml
+++ b/abstract/relational_apron.ml
@@ -59,9 +59,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
         let env2 = Environment.add env [| Var.of_string id |] [||] in
         Abstract1.change_environment manager x env2 false
     let rmvar x id =
+        let v = [| Var.of_string id |] in
         let env = Abstract1.env x in
-        let env2 = Environment.remove env [| Var.of_string id |] in
-        Abstract1.change_environment manager x env2 false
+        let env2 = Environment.remove env v in
+        let y = Abstract1.forget_array manager x v false in
+        Abstract1.change_environment manager y env2 false
     let vars x =
         List.map Var.to_string @@
         Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
@@ -98,13 +100,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
     let widen = Abstract1.widening manager
 
     let subset = Abstract1.is_leq manager
+    let eq = Abstract1.is_eq manager
 
     let var_str x idl = 
         let prevars = vars x in
         let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in
-        (* print_list "prevars" prevars;
-        print_list "idl" idl;
-        print_list "rm_vars_l" rm_vars_l; *)
         let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in
         let xx = Abstract1.forget_array manager x rm_vars false in
         let b = Buffer.create 80 in