1 files changed, 18 insertions, 22 deletions

diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index b83edc1..3cdcc31 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -69,20 +69,26 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
         | Env env -> V.to_itv (get_var env id)
 
     (* Set-theoretic operations *)
+    let f_in_merge f _ a b = match a, b with
+      | Some a, None -> Some a
+      | None, Some b -> Some b
+      | Some a, Some b -> Some (f a b)
+      | _ -> assert false
+
     let join a b = match a, b with
         | Bot, x | x, Bot -> x
         | Env m, Env n ->
-            strict (VarMap.map2z (fun _ a b -> V.join a b) m n)
+            strict (VarMap.merge (f_in_merge V.join) m n)
     
     let meet a b = match a, b with
         | Bot, _ | _, Bot -> Bot
         | Env m, Env n ->
-            strict (VarMap.map2z (fun _ a b -> V.meet a b) m n)
+            strict (VarMap.merge (f_in_merge V.meet) m n)
 
     let widen a b = match a, b with
         | Bot, x | x, Bot -> x
         | Env m, Env n ->
-            strict (VarMap.map2z (fun _ a b -> V.widen a b) m n)
+            strict (VarMap.merge (f_in_merge V.widen) m n)
 
     (* Inclusion and equality *)
     let subset a b = match a, b with
@@ -161,27 +167,17 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
         List.fold_left restrict_var env
           (extract_var (expr, zop, NIntConst 0))
 
-    let rec apply_cl x (cons, rest) =
-        let apply_cl_l x = List.fold_left apply_cons x cons in
-
-        let y = fix eq apply_cl_l x in
-        if debug then Format.printf "-[@.";
-        let z = apply_cl_r y rest in
-        if debug then Format.printf "-]@.";
-        fix eq apply_cl_l z
-
-    and apply_cl_r x = function
-        | CLTrue -> x
+    let rec apply_cl x (cons, rest) = match rest with
+        | CLTrue ->
+          let apply_cl_l x = List.fold_left apply_cons x cons in
+          fix eq apply_cl_l x
         | CLFalse -> vbottom x
         | CLAnd(a, b) ->
-          let y = apply_cl_r x a in
-          apply_cl_r y b
-        | CLOr(a, b) ->
-          if debug then Format.printf "<<@.";
-          let y = apply_cl x a in
-          if debug then Format.printf "\\/@.";
-          let z = apply_cl x b in
-          if debug then Format.printf ">>@.";
+          let y = apply_cl x (cons, a) in
+          apply_cl y (cons, b)
+        | CLOr((ca, ra), (cb, rb)) ->
+          let y = apply_cl x (cons@ca, ra) in
+          let z = apply_cl x (cons@cb, rb) in
           join y z
 
     let apply_f x f = apply_cl x (conslist_of_f f)