1 files changed, 33 insertions, 25 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 722dc1a..cdf3c7e 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -259,30 +259,37 @@ end = struct
     *)
     let edd_of_cons ve (op, vid, r) =
         let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
-
-        let leaves = Hashtbl.create 1 in
-
-        let root = match r with
-        | EItem x ->
-          DChoice(0, vid,
-              List.map (fun v -> if op v x then v, DTop else v, DBot)
-                (List.assoc vid ve.evars))      
-        | EIdent vid2 ->
-            let a, b =
-                if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2
-                  then vid, vid2
-                  else vid2, vid
-            in
-            let nc = ref 0 in
-            let nb x =
-              incr nc;
-              DChoice(!nc, b,
-                    List.map (fun v -> if op v x then v, DTop else v, DBot)
-                      (List.assoc b ve.evars))
+        if not (List.mem vid ve.d_vars) 
+          then edd_top ve
+          else
+            let leaves = Hashtbl.create 1 in
+            let root = match r with
+            | EItem x ->
+              DChoice(0, vid,
+                  List.map (fun v -> if op v x then v, DTop else v, DBot)
+                    (List.assoc vid ve.evars))      
+            | EIdent vid2 ->
+                if not (List.mem vid2 ve.d_vars)
+                  then DTop
+                  else
+                    let a, b =
+                        if Hashtbl.find ve.ev_order vid
+                            < Hashtbl.find ve.ev_order vid2
+                          then vid, vid2
+                          else vid2, vid
+                    in
+                    let nc = ref 0 in
+                    let nb x =
+                      incr nc;
+                      DChoice(!nc, b,
+                            List.map (fun v -> if op v x then v, DTop else v, DBot)
+                              (List.assoc b ve.evars))
+                    in
+                    DChoice(0, a, List.map
+                      (fun x -> x, nb x)
+                      (List.assoc a ve.evars))
             in
-            DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
-        in
-        { ve; root; leaves }
+            { ve; root; leaves }
 
     (*
       edd_join : edd_v -> edd_v -> edd_v
@@ -570,7 +577,8 @@ end = struct
             all_vars = [];
             cycle = [];
             forget = [];
-            forget_inv = []; } in
+            forget_inv = [];
+            d_vars = ["x"; "y"; "z"] } in
         Hashtbl.add ve.ev_order "x" 0;
         Hashtbl.add ve.ev_order "y" 1;
         Hashtbl.add ve.ev_order "z" 2;
@@ -856,7 +864,7 @@ end = struct
           guarantees;
         Format.printf "@.";
         
-        let ve = mk_varenv rp f cl in
+        let ve = mk_varenv rp opt.disjunct f cl in
 
         { rp; opt; ve; init_cl; cl; guarantees; }