diff --git a/dune-project b/dune-project
index aec7520e1c..21831e0b9e 100644
--- a/dune-project
+++ b/dune-project
@@ -39,6 +39,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (ocaml (>= 4.14))
     (goblint-cil (>= 2.0.9)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.9.0))
+    (patricia-tree (>= 0.13.0))
     (zarith (>= 1.12))
     (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
     (qcheck-core (>= 0.19))
diff --git a/goblint.opam b/goblint.opam
index 5907626172..1b0e6b2879 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -41,6 +41,7 @@ depends: [
   "ocaml" {>= "4.14"}
   "goblint-cil" {>= "2.0.9"}
   "batteries" {>= "3.9.0"}
+  "patricia-tree" {>= "0.13.0"}
   "zarith" {>= "1.12"}
   "yojson" {>= "2.0.0" & < "3"}
   "qcheck-core" {>= "0.19"}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 53f69f4047..3943cd7144 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -88,6 +88,7 @@ depends: [
   "odoc-parser" {= "3.0.0" & with-doc}
   "ordering" {= "3.19.1"}
   "ounit2" {= "2.2.7" & with-test}
+  "patricia-tree" {= "0.13.0"}
   "pp" {= "2.0.0"}
   "ppx_blob" {= "0.9.0"}
   "ppx_derivers" {= "1.2.1"}
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index d88465b17f..e6a8542b12 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -442,7 +442,7 @@ struct
       (* Additionally filter get_m in case it contains variables it no longer protects. *)
       let is_in_Gm x _ = is_protected_by ask m x in
       let get_m = CPA.filter is_in_Gm get_m in
-      let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
+      let long_meet m1 m2 = CPA.nonidempotent_union VD.meet m1 m2 in (* TODO: idempotent_union if not using int domain refinement *)
       let meet = long_meet st.cpa get_m in
       if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet;
       {st with cpa = meet}
@@ -508,7 +508,7 @@ struct
     | VarQuery.Global g -> vf (V.global g)
     | _ -> ()
 
-  let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2
+  let long_meet m1 m2 = CPA.nonidempotent_union VD.meet m1 m2 (* TODO: idempotent_union if not using int domain refinement *)
 
   let update_if_mem var value m =
     if CPA.mem var m then
diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
index 64b5a174e8..dee5b0f908 100644
--- a/src/cdomains/baseDomain.ml
+++ b/src/cdomains/baseDomain.ml
@@ -5,7 +5,7 @@ module VD = ValueDomain.Compound
 
 module CPA =
 struct
-  module M0 = MapDomain.MapBot (Basetype.Variables) (VD)
+  module M0 = MapDomain.PatriciaMapBot (Basetype.Variables) (VD)
   module M =
   struct
     include M0
diff --git a/src/common/util/cilType.ml b/src/common/util/cilType.ml
index ecb60bf9d4..3241c990fb 100644
--- a/src/common/util/cilType.ml
+++ b/src/common/util/cilType.ml
@@ -365,6 +365,7 @@ struct
   let equal x y = x.vid = y.vid
   let compare x y = Stdlib.compare x.vid y.vid
   let hash x = x.vid
+  let tag x = x.vid
 
   (* Output *)
   let show x = x.vname
diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml
index 06215d0a63..db04aaf5b8 100644
--- a/src/domain/disjointDomain.ml
+++ b/src/domain/disjointDomain.ml
@@ -572,11 +572,17 @@ struct
   let mapi f m = M.map (fun b ->
       B.mapi f b
     ) m
-  let long_map2 f m1 m2 = M.long_map2 (fun b1 b2 ->
-      B.long_map2 f b1 b2
+  let idempotent_union f m1 m2 = M.idempotent_union (fun b1 b2 ->
+      B.idempotent_union f b1 b2
     ) m1 m2
-  let map2 f m1 m2 = M.map2 (fun b1 b2 ->
-      B.map2 f b1 b2
+  let nonidempotent_union f m1 m2 = M.nonidempotent_union (fun b1 b2 ->
+      B.nonidempotent_union f b1 b2
+    ) m1 m2
+  let idempotent_inter f m1 m2 = M.idempotent_inter (fun b1 b2 ->
+      B.idempotent_inter f b1 b2
+    ) m1 m2
+  let nonidempotent_inter f m1 m2 = M.nonidempotent_inter (fun b1 b2 ->
+      B.nonidempotent_inter f b1 b2
     ) m1 m2
   let merge f m1 m2 = failwith "ProjectiveMap.merge" (* TODO: ? *)
 
@@ -627,6 +633,7 @@ struct
 
   let filter p m = failwith "ProjectiveMap.filter"
 
+  let reflexive_subset_domain_for_all2 _ _ _ = failwith "ProjectiveMap.reflexive_subset_domain_for_all2"
   let leq_with_fct _ _ _ = failwith "ProjectiveMap.leq_with_fct"
   let join_with_fct _ _ _ = failwith "ProjectiveMap.join_with_fct"
   let widen_with_fct _ _ _ = failwith "ProjectiveMap.widen_with_fct"
@@ -735,28 +742,29 @@ struct
   let mapi f m = S.map (fun b ->
       B.mapi f b
     ) m
-  let long_map2 f s1 s2 =
+  let nonidempotent_union f s1 s2 =
     let f b2 (s1, acc) =
       let e2 = fst (B.choose b2) in
       let (s1_match, s1_rest) = S.partition (fun b1 -> C.cong (fst (B.choose b1)) e2) s1 in
       let b' = match S.choose s1_match with
         | b1 ->
           assert (S.cardinal s1_match = 1);
-          B.long_map2 f b1 b2
+          B.nonidempotent_union f b1 b2
         | exception Not_found -> b2
       in
       (s1_rest, S.add b' acc)
     in
     let (s1', acc) = S.fold f s2 (s1, empty ()) in
     S.union s1' acc
-  let map2 f s1 s2 =
+  let idempotent_union _ _ _ = failwith "PairwiseMap.idempotent_union" (* TODO: ? *)
+  let nonidempotent_inter f s1 s2 =
     let f b2 (s1, acc) =
       let e2 = fst (B.choose b2) in
       let (s1_match, s1_rest) = S.partition (fun b1 -> C.cong (fst (B.choose b1)) e2) s1 in
       let acc' = match S.choose s1_match with
         | b1 ->
           assert (S.cardinal s1_match = 1);
-          begin match B.map2 f b1 b2 with
+          begin match B.nonidempotent_inter f b1 b2 with
             | b' when B.is_bot b' ->
               acc (* remove bot bucket to preserve invariant *)
             | exception Lattice.BotValue ->
@@ -769,6 +777,7 @@ struct
       (s1_rest, acc')
     in
     snd (S.fold f s2 (s1, S.empty ()))
+  let idempotent_inter _ _ _ = failwith "PairwiseMap.idempotent_inter" (* TODO: ? *)
   let merge f m1 m2 = failwith "PairwiseMap.merge" (* TODO: ? *)
 
   let leq s1 s2 =
@@ -885,6 +894,7 @@ struct
 
   let filter p s = failwith "PairwiseMap.filter"
 
+  let reflexive_subset_domain_for_all2 _ _ _ = failwith "PairwiseMap.reflexive_subset_domain_for_all2"
   let leq_with_fct _ _ _ = failwith "PairwiseMap.leq_with_fct"
   let join_with_fct _ _ _ = failwith "PairwiseMap.join_with_fct"
   let widen_with_fct _ _ _ = failwith "PairwiseMap.widen_with_fct"
diff --git a/src/domain/dune b/src/domain/dune
index ce4cdcb1a5..46471a768d 100644
--- a/src/domain/dune
+++ b/src/domain/dune
@@ -8,7 +8,8 @@
    batteries.unthreaded
    goblint_std
    goblint_common
-   goblint-cil)
+   goblint-cil
+   patricia-tree)
  (flags :standard -open Goblint_std)
  (preprocess
   (pps
diff --git a/src/domain/hoareDomain.ml b/src/domain/hoareDomain.ml
index 1bd56c0d1d..1981c251f6 100644
--- a/src/domain/hoareDomain.ml
+++ b/src/domain/hoareDomain.ml
@@ -277,7 +277,7 @@ struct
 
   let elements (s: t): (key * R.t) list = bindings s
   let of_list (l: (key * R.t) list): t = List.fold_left (fun acc (x, r) -> add x r acc) (empty ()) l
-  let union = long_map2 R.union
+  let union = idempotent_union R.union
 
 
   (* copied & modified from SetDomain.Hoare_NoTop *)
diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml
index cf563dab44..947208bdff 100644
--- a/src/domain/mapDomain.ml
+++ b/src/domain/mapDomain.ml
@@ -28,8 +28,11 @@ sig
   val add_list_fun: key list -> (key -> value) -> t -> t
 
   val for_all: (key -> value -> bool) -> t -> bool
-  val map2: (value -> value -> value) -> t -> t -> t
-  val long_map2: (value -> value -> value) -> t -> t -> t
+  val reflexive_subset_domain_for_all2: (value -> value -> bool) -> t -> t -> bool
+  val idempotent_inter: (value -> value -> value) -> t -> t -> t
+  val nonidempotent_inter: (value -> value -> value) -> t -> t -> t
+  val idempotent_union: (value -> value -> value) -> t -> t -> t
+  val nonidempotent_union: (value -> value -> value) -> t -> t -> t
   val merge : (key -> value option -> value option -> value option) -> t -> t -> t (* TODO: unused, remove? *)
 
   val cardinal: t -> int
@@ -135,12 +138,102 @@ struct
   (* TODO: groups in XML, JSON? *)
 end
 
-module PMap (Domain: Printable.S) (Range: Lattice.S) : PS with
+module type MapS =
+sig
+  type key
+  type 'a t
+  val empty: 'a t
+  val is_empty: 'a t -> bool
+  val mem:  key -> 'a t -> bool
+  val add: key -> 'a -> 'a t -> 'a t
+  val singleton: key -> 'a -> 'a t
+  val remove: key -> 'a t -> 'a t
+  val merge: (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+  val idempotent_union: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+  val nonidempotent_union: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+  val idempotent_inter: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+  val nonidempotent_inter: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+  val reflexive_compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+  val reflexive_equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+  val reflexive_subset_domain_for_all2: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+  val iter: (key -> 'a -> unit) -> 'a t -> unit
+  val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val for_all: (key -> 'a -> bool) -> 'a t -> bool
+  val exists: (key -> 'a -> bool) -> 'a t -> bool
+  val filter: (key -> 'a -> bool) -> 'a t -> 'a t
+  val cardinal: 'a t -> int
+  val bindings: 'a t -> (key * 'a) list
+  val choose: 'a t -> (key * 'a)
+  val find: key -> 'a t -> 'a
+  val find_opt: key -> 'a t -> 'a option
+  val map: ('a -> 'a) -> 'a t -> 'a t
+  val mapi: (key -> 'a -> 'a) -> 'a t -> 'a t
+end
+
+module StdMap (K: Map.OrderedType): MapS with type key = K.t =
+struct
+  include Map.Make (K)
+
+  let reflexive_equal f x y = x == y || equal f x y
+  let reflexive_compare f x y = if x == y then 0 else compare f x y
+
+  let reflexive_subset_domain_for_all2 f m1 m2 =
+    (* For each key-value in m1, the same key must be in m2 with a geq value: *)
+    let p key value =
+      try f value (find key m2) with Not_found -> false
+    in
+    m1 == m2 || for_all p m1
+
+  let nonidempotent_union op =
+    let f k v1 v2 =
+      match v1, v2 with
+      | Some v1, Some v2 -> Some (op v1 v2)
+      | Some _, _ -> v1
+      | _, Some _ -> v2
+      | _ -> None
+    in
+    merge f
+
+  let idempotent_union f m1 m2 =
+    if m1 == m2 then m1 else nonidempotent_union f m1 m2
+
+  let nonidempotent_inter op =
+    (* Similar to the previous, except we ignore elements that only occur in one
+     * of the mappings, so we start from an empty map *)
+    let f k v1 v2 =
+      match v1, v2 with
+      | Some v1, Some v2 -> Some (op v1 v2)
+      | _ -> None
+    in
+    merge f
+
+  let idempotent_inter f m1 m2 =
+    if m1 == m2 then m1 else nonidempotent_inter f m1 m2
+end
+
+module PatriciaMap (K: PatriciaTree.KEY): MapS with type key = K.t =
+struct
+  include PatriciaTree.MakeMap (K)
+
+  let merge = slow_merge (* TODO: get rid of this *)
+
+  (* The following intentionally do not use [(fun _ -> f)] to avoid extra closure allocations and applications from partial application. *)
+  (* TODO: Benchmark this theory. *)
+  let idempotent_union f = idempotent_union (fun _ v v' -> f v v')
+  let nonidempotent_union f = nonidempotent_union (fun _ v v' -> f v v')
+  let idempotent_inter f = idempotent_inter (fun _ v v' -> f v v')
+  let nonidempotent_inter f = nonidempotent_inter_no_share (fun _ v v' -> f v v')
+  let reflexive_subset_domain_for_all2 f = reflexive_subset_domain_for_all2 (fun _ v v' -> f v v')
+
+  let exists f m = not (for_all (fun k v -> not (f k v)) m)
+  let bindings = to_list
+  let choose = unsigned_min_binding
+end
+
+module GenPMap (Domain: Printable.S) (M: MapS with type key = Domain.t) (Range: Lattice.S) : PS with
   type key = Domain.t and
   type value = Range.t =
 struct
-  module M = Map.Make (Domain)
-
   include Printable.Std
   include M
   type key = Domain.t
@@ -149,10 +242,8 @@ struct
 
   let name () = "map"
 
-  (* And one less brainy definition *)
-  let for_all2 = M.equal
-  let equal x y = x == y || for_all2 Range.equal x y
-  let compare x y = if equal x y then 0 else M.compare Range.compare x y
+  let equal = reflexive_equal Range.equal
+  let compare = reflexive_compare Range.compare
   let hash xs = fold (fun k v a -> a + (Domain.hash k * Range.hash v)) xs 0
 
   let empty () = M.empty
@@ -167,26 +258,6 @@ struct
   let add_list_fun keys f m =
     List.fold_left (fun acc key -> add key (f key) acc) m keys
 
-  let long_map2 op =
-    let f k v1 v2 =
-      match v1, v2 with
-      | Some v1, Some v2 -> Some (op v1 v2)
-      | Some _, _ -> v1
-      | _, Some _ -> v2
-      | _ -> None
-    in
-    M.merge f
-
-  let map2 op =
-    (* Similar to the previous, except we ignore elements that only occur in one
-     * of the mappings, so we start from an empty map *)
-    let f k v1 v2 =
-      match v1, v2 with
-      | Some v1, Some v2 -> Some (op v1 v2)
-      | _ -> None
-    in
-    M.merge f
-
   include Print (Domain) (Range) (
     struct
       type nonrec t = t
@@ -246,10 +317,13 @@ struct
 
   let add_list_fun keys f = lift_f' (M.add_list_fun keys f)
 
-  let long_map2 op = lift_f2' (M.long_map2 op)
+  let idempotent_union op = lift_f2' (M.idempotent_union op)
+  let nonidempotent_union op = lift_f2' (M.nonidempotent_union op)
 
-  let map2 op = lift_f2' (M.map2 op)
+  let idempotent_inter op = lift_f2' (M.idempotent_inter op)
+  let nonidempotent_inter op = lift_f2' (M.nonidempotent_inter op)
 
+  let reflexive_subset_domain_for_all2 f = lift_f2 (M.reflexive_subset_domain_for_all2 f)
   let leq_with_fct f = lift_f2 (M.leq_with_fct f)
   let join_with_fct f = lift_f2' (M.join_with_fct f)
   let widen_with_fct f = lift_f2' (M.widen_with_fct f)
@@ -299,10 +373,13 @@ struct
 
   let add_list_fun keys f = lift_f' (M.add_list_fun keys f)
 
-  let long_map2 op = lift_f2' (M.long_map2 op)
+  let idempotent_union op = lift_f2' (M.idempotent_union op)
+  let nonidempotent_union op = lift_f2' (M.nonidempotent_union op)
 
-  let map2 op = lift_f2' (M.map2 op)
+  let idempotent_inter op = lift_f2' (M.idempotent_inter op)
+  let nonidempotent_inter op = lift_f2' (M.nonidempotent_inter op)
 
+  let reflexive_subset_domain_for_all2 f = lift_f2 (M.reflexive_subset_domain_for_all2 f)
   let leq_with_fct f = lift_f2 (M.leq_with_fct f)
   let join_with_fct f = lift_f2' (M.join_with_fct f)
   let widen_with_fct f = lift_f2' (M.widen_with_fct f)
@@ -371,10 +448,13 @@ struct
   let add_list_set ks v x = time "add_list_set" (M.add_list_set ks v) x
   let add_list_fun ks f x = time "add_list_fun" (M.add_list_fun ks f) x
 
-  let long_map2 f x y = time "long_map2" (M.long_map2 f x) y
+  let idempotent_union f x y = time "idempotent_union" (M.idempotent_union f x) y
+  let nonidempotent_union f x y = time "nonidempotent_union" (M.nonidempotent_union f x) y
 
-  let map2 f x y = time "map2" (M.map2 f x) y
+  let idempotent_inter f x y = time "idempotent_inter" (M.idempotent_inter f x) y
+  let nonidempotent_inter f x y = time "nonidempotent_inter" (M.nonidempotent_inter f x) y
 
+  let reflexive_subset_domain_for_all2 f x y = time "reflexive_subset_domain_for_all2" (M.reflexive_subset_domain_for_all2 f x) y
   let leq_with_fct f x y = time "leq_with_fct" (M.leq_with_fct f x) y
   let join_with_fct f x y = time "join_with_fct" (M.join_with_fct f x) y
   let widen_with_fct f x y = time "widen_with_fct" (M.widen_with_fct f x) y
@@ -382,19 +462,13 @@ struct
   let relift x = M.relift x
 end
 
-module MapBot (Domain: Printable.S) (Range: Lattice.S) : S with
+module GenMapBot (Domain: Printable.S) (M: MapS with type key = Domain.t) (Range: Lattice.S) : S with
   type key = Domain.t and
   type value = Range.t =
 struct
-  include PMap (Domain) (Range)
-
-  let leq_with_fct f m1 m2 =
-    (* For each key-value in m1, the same key must be in m2 with a geq value: *)
-    let p key value =
-      try f value (find key m2) with Not_found -> false
-    in
-    m1 == m2 || for_all p m1
+  include GenPMap (Domain) (M) (Range)
 
+  let leq_with_fct = reflexive_subset_domain_for_all2
   let leq = leq_with_fct Range.leq
 
   let find x m = try find x m with | Not_found -> Range.bot ()
@@ -418,32 +492,28 @@ struct
     | Some w -> w
     | None -> Pretty.dprintf "No binding grew."
 
-  let meet m1 m2 = if m1 == m2 then m1 else map2 Range.meet m1 m2
+  let meet = nonidempotent_inter Range.meet (* TODO: idempotent_inter if not using int domain refinement *)
 
-  let join_with_fct f m1 m2 =
-    if m1 == m2 then m1 else long_map2 f m1 m2
+  let join_with_fct = idempotent_union
   let join = join_with_fct Range.join
 
-  let widen_with_fct f =  long_map2 f
+  let widen_with_fct = idempotent_union
   let widen  = widen_with_fct Range.widen
 
 
-  let narrow = map2 Range.narrow
+  let narrow = nonidempotent_inter Range.narrow (* TODO: idempotent_inter if not using int domain refinement *)
 end
 
-module MapTop (Domain: Printable.S) (Range: Lattice.S) : S with
+module MapBot (Domain: Printable.S) (Range: Lattice.S) = GenMapBot (Domain) (StdMap (Domain)) (Range)
+module PatriciaMapBot (Domain: Printable.S) (Range: Lattice.S) = GenMapBot (Domain) (PatriciaMap (struct include Domain let to_int = tag end)) (Range)
+
+module GenMapTop (Domain: Printable.S) (M: MapS with type key = Domain.t) (Range: Lattice.S) : S with
   type key = Domain.t and
   type value = Range.t =
 struct
-  include PMap (Domain) (Range)
-
-  let leq_with_fct f m1 m2 = (* TODO use merge or sth faster? *)
-    (* For each key-value in m2, the same key must be in m1 with a leq value: *)
-    let p key value =
-      try f (find key m1) value with Not_found -> false
-    in
-    m1 == m2 || for_all p m2
+  include GenPMap (Domain) (M) (Range)
 
+  let leq_with_fct f m1 m2 = reflexive_subset_domain_for_all2 (Fun.flip f) m2 m1
   let leq = leq_with_fct Range.leq
 
   let find x m = try find x m with | Not_found -> Range.top ()
@@ -453,17 +523,16 @@ struct
   let is_bot _ = false
 
   (* let cleanup m = fold (fun k v m -> if Range.is_top v then remove k m else m) m m *)
-  let meet m1 m2 = if m1 == m2 then m1 else long_map2 Range.meet m1 m2
+  let meet = nonidempotent_union Range.meet (* TODO: idempotent_union if not using int domain refinement *)
 
-  let join_with_fct f m1 m2 =
-    if m1 == m2 then m1 else map2 f m1 m2
+  let join_with_fct = idempotent_inter
 
   let join = join_with_fct Range.join
 
-  let widen_with_fct f = map2 f
+  let widen_with_fct f = idempotent_inter f
   let widen = widen_with_fct Range.widen
 
-  let narrow = long_map2 Range.narrow
+  let narrow = nonidempotent_union Range.narrow (* TODO: idempotent_union if not using int domain refinement *)
 
   let pretty_diff () ((m1:t),(m2:t)): Pretty.doc =
     let diff_key k v acc_opt =
@@ -481,6 +550,9 @@ struct
     | None -> Pretty.dprintf "No binding grew."
 end
 
+module MapTop (Domain: Printable.S) (Range: Lattice.S) = GenMapTop (Domain) (StdMap (Domain)) (Range)
+module PatriciaMapTop (Domain: Printable.S) (Range: Lattice.S) = GenMapTop (Domain) (PatriciaMap (struct include Domain let to_int = tag end)) (Range)
+
 exception Fn_over_All of string
 
 module LiftTop (Range: Lattice.S) (M: S with type value = Range.t): S with
@@ -528,15 +600,25 @@ struct
     | `Top -> `Top
     | `Lifted x -> `Lifted (M.add_list_fun ks f x)
 
-  let map2 f x y =
+  let idempotent_inter f x y =
+    match x, y with
+    | `Lifted x, `Lifted y -> `Lifted (M.idempotent_inter f x y)
+    | _ -> raise (Fn_over_All "idempotent_inter")
+
+  let nonidempotent_inter f x y =
+    match x, y with
+    | `Lifted x, `Lifted y -> `Lifted (M.nonidempotent_inter f x y)
+    | _ -> raise (Fn_over_All "nonidempotent_inter")
+
+  let idempotent_union f x y =
     match x, y with
-    | `Lifted x, `Lifted y -> `Lifted (M.map2 f x y)
-    | _ -> raise (Fn_over_All "map2")
+    | `Lifted x, `Lifted y -> `Lifted (M.idempotent_union f x y)
+    | _ -> raise (Fn_over_All "idempotent_union")
 
-  let long_map2 f x y =
+  let nonidempotent_union f x y =
     match x, y with
-    | `Lifted x, `Lifted y -> `Lifted (M.long_map2 f x y)
-    | _ -> raise (Fn_over_All "long_map2")
+    | `Lifted x, `Lifted y -> `Lifted (M.nonidempotent_union f x y)
+    | _ -> raise (Fn_over_All "nonidempotent_union")
 
   let for_all f = function
     | `Top -> raise (Fn_over_All "for_all")
@@ -561,6 +643,12 @@ struct
     | `Lifted x, `Lifted y -> `Lifted (M.merge f x y)
     | _ -> raise (Fn_over_All "merge")
 
+  let reflexive_subset_domain_for_all2 f x y =
+    match (x,y) with
+    | (_, `Top) -> true
+    | (`Top, _) -> false
+    | (`Lifted x, `Lifted y) -> M.reflexive_subset_domain_for_all2 f x y
+
   let leq_with_fct f x y =
     match (x,y) with
     | (_, `Top) -> true
@@ -656,15 +744,25 @@ struct
     | `Bot -> `Bot
     | `Lifted x -> `Lifted (M.add_list_fun ks f x)
 
-  let map2 f x y =
+  let idempotent_inter f x y =
+    match x, y with
+    | `Lifted x, `Lifted y -> `Lifted (M.idempotent_inter f x y)
+    | _ -> raise (Fn_over_All "idempotent_inter")
+
+  let nonidempotent_inter f x y =
+    match x, y with
+    | `Lifted x, `Lifted y -> `Lifted (M.nonidempotent_inter f x y)
+    | _ -> raise (Fn_over_All "nonidempotent_inter")
+
+  let idempotent_union f x y =
     match x, y with
-    | `Lifted x, `Lifted y -> `Lifted (M.map2 f x y)
-    | _ -> raise (Fn_over_All "map2")
+    | `Lifted x, `Lifted y -> `Lifted (M.idempotent_union f x y)
+    | _ -> raise (Fn_over_All "idempotent_union")
 
-  let long_map2 f x y =
+  let nonidempotent_union f x y =
     match x, y with
-    | `Lifted x, `Lifted y -> `Lifted (M.long_map2 f x y)
-    | _ -> raise (Fn_over_All "long_map2")
+    | `Lifted x, `Lifted y -> `Lifted (M.nonidempotent_union f x y)
+    | _ -> raise (Fn_over_All "nonidempotent_union")
 
   let for_all f = function
     | `Bot -> raise (Fn_over_All "for_all")
@@ -700,6 +798,12 @@ struct
     | (`Lifted x, `Lifted y) -> `Lifted(M.widen_with_fct f x y)
     | _ -> y
 
+  let reflexive_subset_domain_for_all2 f x y =
+    match (x,y) with
+    | (`Bot, _) -> true
+    | (_, `Bot) -> false
+    | (`Lifted x, `Lifted y) -> M.reflexive_subset_domain_for_all2 f x y
+
   let leq_with_fct f x y =
     match (x,y) with
     | (`Bot, _) -> true
@@ -758,8 +862,10 @@ struct
       er
   let map f (e, r) = (e, f r)
   let mapi f (e, r) = (e, f e r)
-  let map2 f (e, r) (e', r') = (E.meet e e', f r r')
-  let long_map2 f (e, r) (e', r') = (E.join e e', f r r')
+  let idempotent_inter f (e, r) (e', r') = (E.meet e e', f r r')
+  let nonidempotent_inter f (e, r) (e', r') = (E.meet e e', f r r')
+  let idempotent_union f (e, r) (e', r') = (E.join e e', f r r')
+  let nonidempotent_union f (e, r) (e', r') = (E.join e e', f r r')
   let merge f m1 m2 = failwith "MapDomain.Joined.merge" (* TODO: ? *)
   let fold f (e, r) a = f e r a
   let empty () = (E.bot (), R.bot ())
@@ -792,6 +898,7 @@ struct
       add e (f e) acc
     ) m es
 
+  let reflexive_subset_domain_for_all2 _ _ _ = failwith "MapDomain.Joined.reflexive_subset_domain_for_all2"
   let leq_with_fct _ _ _ = failwith "MapDomain.Joined.leq_with_fct"
   let join_with_fct _ _ _ = failwith "MapDomain.Joined.join_with_fct"
   let widen_with_fct _ _ _ = failwith "MapDomain.Joined.widen_with_fct"
diff --git a/tests/unit/domains/mapDomainTest.ml b/tests/unit/domains/mapDomainTest.ml
index 64be44f77e..5a9abf2d30 100644
--- a/tests/unit/domains/mapDomainTest.ml
+++ b/tests/unit/domains/mapDomainTest.ml
@@ -119,7 +119,7 @@ struct
     assert_bool "for_all broken" (M.for_all fun1 !map)
 
 
-  let test_map2 _ =
+  let test_nonidempotent_inter _ =
     let map1 = ref (get_empty ()) in
     let map2 = ref (get_empty ()) in
     let values1 = ["1","a";"2","b";"3","c";"4","d"] in
@@ -128,11 +128,11 @@ struct
     let fun2 v1 v2 a = v2^a in
     map1 := M.add_list values1 !map1;
     map2 := M.add_list values2 !map2;
-    ignore (M.map2 fun1 !map1 !map2);
-    assert_equal "111" (M.fold fun2 (M.map2 fun1 !map2 !map1) "")
+    ignore (M.nonidempotent_inter fun1 !map1 !map2);
+    assert_equal "111" (M.fold fun2 (M.nonidempotent_inter fun1 !map2 !map1) "")
 
 
-  let test_long_map2 _ =
+  let test_nonidempotent_union _ =
     let map1 = ref (get_empty ()) in
     let map2 = ref (get_empty ()) in
     let values1 = ["1","a";"2","b";"3","c";"4","d"] in
@@ -141,8 +141,8 @@ struct
     let fun2 v1 v2 a = v2^a in
     map1 := M.add_list values1 !map1;
     map2 := M.add_list values2 !map2;
-    ignore (M.long_map2 fun1 !map1 !map2);
-    assert_equal "1111" (M.fold fun2 (M.long_map2 fun1 !map2 !map1) "")
+    ignore (M.nonidempotent_union fun1 !map1 !map2);
+    assert_equal "1111" (M.fold fun2 (M.nonidempotent_union fun1 !map2 !map1) "")
 
 
   let test () =
@@ -155,8 +155,8 @@ struct
       "test_add_list_set"    >:: test_add_list_set;
       "test_add_list_fun"    >:: test_add_list_fun;
       "test_for_all"         >:: test_for_all;
-      "test_map2"            >:: test_map2;
-      "test_long_map2"       >:: test_long_map2;
+      "test_nonidempotent_inter" >:: test_nonidempotent_inter;
+      "test_nonidempotent_union" >:: test_nonidempotent_union;
     ]
 
 end