diff --git a/colibri2/core/colibri2_core.ml b/colibri2/core/colibri2_core.ml
index 272f9f79649d78ef3a74b21b9ae21b84093411e0..9cff4634ab1d357e0933ed35f4bb53e443be5265 100644
--- a/colibri2/core/colibri2_core.ml
+++ b/colibri2/core/colibri2_core.ml
@@ -106,16 +106,25 @@ module Dom = struct
    restricted to a singleton return the corresponding value *)
   end
 
-  module Make (L : Lattice) : sig
-    include S with type t = L.t
+  module type LS = sig
+    type t
 
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val set_dom : Egraph.wt -> Node.t -> t -> unit
     (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
 
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val upd_dom : Egraph.wt -> Node.t -> t -> unit
     (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
         [l] with the current value of the domain. *)
-  end = struct
+  end
+
+  module type DS = sig
+    type t
+
+    include S with type t := t
+    include LS with type t := t
+  end
+
+  module Make (L : Lattice) : DS with type t = L.t = struct
     type t = L.t
 
     let pp = L.pp
@@ -169,14 +178,7 @@ module Dom = struct
 
   (** [Lattice(L)] register a domain as a lattice. It returns useful function
      for setting and updating the domain *)
-  module Lattice (L : Lattice) : sig
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
-
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
-        [l] with the current value of the domain. *)
-  end = struct
+  module Lattice (L : Lattice) : LS with type t = L.t = struct
     module S = Make (L)
 
     let () = register (module S)
diff --git a/colibri2/core/colibri2_core.mli b/colibri2/core/colibri2_core.mli
index 14b2650f275979276c56d727d8ea8369fd304f29..b3cca4eec2d3270d4ba7723b6a2fe7350dd1cb1e 100644
--- a/colibri2/core/colibri2_core.mli
+++ b/colibri2/core/colibri2_core.mli
@@ -566,29 +566,29 @@ and Dom : sig
         restricted to a singleton return the corresponding value *)
   end
 
-  module Make (L : Lattice) : sig
-    include S with type t = L.t
+  module type LS = sig
+    type t
 
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val set_dom : Egraph.wt -> Node.t -> t -> unit
     (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
 
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val upd_dom : Egraph.wt -> Node.t -> t -> unit
     (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
         [l] with the current value of the domain. *)
   end
 
+  module type DS = sig
+    include S
+    include LS with type t := t
+  end
+
+  module Make (L : Lattice) : DS with type t = L.t
+
   val register : (module S) -> unit
 
   (** [Lattice(L)] register a domain as a lattice. It returns useful function
      for setting and updating the domain *)
-  module Lattice (L : Lattice) : sig
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
-
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
-        [l] with the current value of the domain. *)
-  end
+  module Lattice (L : Lattice) : LS with type t := L.t
 end
 
 module Expr = Expr
diff --git a/colibri2/tests/solve/smt_array/sat/dune b/colibri2/tests/solve/smt_array/sat/dune
index 6f1afca1f3bcfb061a1b657c3a3d59fa1217b9b3..6961407484c34044d304a32c6d47398de1775bd2 100644
--- a/colibri2/tests/solve/smt_array/sat/dune
+++ b/colibri2/tests/solve/smt_array/sat/dune
@@ -18,6 +18,14 @@
     "array-res-ext array-res-aup"
     --options
     "array-diff-graph"
+    --options
+    "array-choice"
+    --options
+    "array-res-ext array-choice"
+    --options
+    "array-res-ext array-res-aup array-choice"
+    --options
+    "array-diff-graph array-choice"
     ;--options
     ;"array-diff-graph array-res-ext"
     ;--options
diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
index fa6ea239231f67ba82e39426a5df3a9834262edd..19710c39dd36a5b2294b1b736b3bf1b04e22d111 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -34,3 +34,39 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat 
 --dont-print-result %{dep:test1.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/unsat/dune b/colibri2/tests/solve/smt_array/unsat/dune
index dcbf0700e8726adf1193888695e5e7dd18b013bc..5227ff747b452c43da9bab2f09c32b7226c975a7 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune
+++ b/colibri2/tests/solve/smt_array/unsat/dune
@@ -18,6 +18,14 @@
     "array-res-ext array-res-aup"
     --options
     "array-diff-graph"
+    --options
+    "array-choice"
+    --options
+    "array-res-ext array-choice"
+    --options
+    "array-res-ext array-res-aup array-choice"
+    --options
+    "array-diff-graph array-choice"
     ;--options
     ;"array-diff-graph array-res-ext"
     ;--options
diff --git a/colibri2/tests/solve/smt_array/unsat/dune.inc b/colibri2/tests/solve/smt_array/unsat/dune.inc
index 925b4d26e97c936e573d3f93b8095d5f575f6fd5..3924334bbb63002b8d4dd542c6c82e2339ee3502 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune.inc
+++ b/colibri2/tests/solve/smt_array/unsat/dune.inc
@@ -178,3 +178,183 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
 --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+--dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
diff --git a/colibri2/theories/array/DiffGraph.ml b/colibri2/theories/array/DiffGraph.ml
index 35bc3e5a57c2821a0684ef813c135045baa1fc4a..5ee8fb1522ce23b7888dd730e32d2e655d867395 100644
--- a/colibri2/theories/array/DiffGraph.ml
+++ b/colibri2/theories/array/DiffGraph.ml
@@ -25,38 +25,20 @@ open Popop_stdlib
 open Common
 module HT = Datastructure.Hashtbl (DInt)
 
-module NHT = struct
-  let nodes = HT.create Node.pp "diffgraph_nodes"
-  let set = HT.set nodes
-  let find = HT.find nodes
-  let find_opt = HT.find_opt nodes
-  let change ~f = HT.change f nodes
-  let remove = HT.remove nodes
-end
+module NHT = MkIHT (struct
+  type t = Node.t
 
-let pp_nid env fmt i =
-  match NHT.find_opt env i with
-  | Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
-  | None -> Format.fprintf fmt "Not_found{id = %d}" i
-
-let s_remove_opt s_opt v =
-  match s_opt with
-  | Some s ->
-      let ns = DInt.S.remove v s in
-      if DInt.S.is_empty ns then None else Some ns
-  | None -> raise Not_found
+  let pp = Node.pp
+  let name = "diffgraph_nodes"
+end)
 
 module DG = struct
-  let diff_graph =
-    HT.create
-      (fun fmt (m, (_ : Node.t DInt.M.t)) -> Node.M.pp DInt.S.pp fmt m)
-      "diff_graph_db"
+  include MkIHT (struct
+    type t = DInt.S.t Node.M.t * Node.t DInt.M.t
 
-  let set = HT.set diff_graph
-  let find = HT.find diff_graph
-  let find_opt = HT.find_opt diff_graph
-  let change ~f = HT.change f diff_graph
-  let remove = HT.remove diff_graph
+    let pp fmt (m, (_ : Node.t DInt.M.t)) = Node.M.pp DInt.S.pp fmt m
+    let name = "diffgraph_nodes"
+  end)
 
   let diffgraph_opt =
     Debug.register_flag ~desc:"Print the entire DiffGraph into a dot file"
@@ -120,10 +102,7 @@ module DG = struct
                  mnp (DInt.M.remove nid m)
         | exception Not_found -> ()
       in
-      aux
-        (HT.fold
-           (fun id (_, m) acc -> DInt.M.add id m acc)
-           diff_graph env DInt.M.empty)
+      aux (fold (fun id (_, m) acc -> DInt.M.add id m acc) env DInt.M.empty)
     in
     fun env ?msg () ->
       if Debug.test_flag diffgraph_opt then (
@@ -138,85 +117,32 @@ module DG = struct
 end
 
 module Id_dom = struct
-  module IVal = struct
-    module T = struct
-      type t = DInt.t [@@deriving eq, ord, hash, show]
-    end
-
-    include T
-    include MkDatatype (T)
-
-    let name = "Array.id.value"
-  end
-
-  let merge_hooks = Datastructure.Push.create Fmt.nop "Array.Id_dom.merge_hooks"
-
-  let register_merge_hook env
-      (f : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) =
-    Datastructure.Push.push merge_hooks env f
-
-  module D = struct
-    include Dom.Make (struct
-      module Value = Value.Register (IVal)
-
-      type t = IVal.t [@@deriving eq, show]
-
-      let is_singleton _ _ = None
-
-      let key =
-        Dom.Kind.create
-          (module struct
-            type nonrec t = t
-
-            let name = "Array.id"
-          end)
-
-      let inter _ v _ = Some v
-    end)
-
-    let merge env (d1, n1) (d2, n2) b =
-      (match (d1, n1, d2, n2) with
-      | Some id1, n1, Some id2, n2 ->
-          Datastructure.Push.iter merge_hooks env ~f:(fun f ->
-              f env (n1, id1) (n2, id2) b)
-          (* id1 always stays, b allows to determine which one will become the
-             representative *)
-      | _ ->
-          (* Ideally, should be unreachable, but it is with the test
-             "./colibri2/tests/solve/smt_array/unsat/ite1.smt2"? *)
-          ());
-
-      merge env (d1, n1) (d2, n2) b
-  end
+  include MkIdDom (struct
+    let n1 = "Array.Id.value"
+    let n2 = "Array.Id_dom.merge_hooks"
+    let n3 = "Array.id"
+  end)
+
+  let new_id_hook env id n b =
+    if b then (
+      DG.set env id (Node.M.empty, DInt.M.empty);
+      NHT.set env id n)
+
+  let set_id env n = set_id ~new_id_hook env n
+  let get_id env n = get_id ~new_id_hook env n
+end
 
-  let () = Dom.register (module D)
+let pp_nid env fmt i =
+  match NHT.find_opt env i with
+  | Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
+  | None -> Format.fprintf fmt "Not_found{id = %d}" i
 
-  let set_id, get_id =
-    let id_counter = ref 0 in
-    let set_id env n =
-      match Egraph.get_dom env D.key n with
-      | None ->
-          incr id_counter;
-          Debug.dprintf3 Common.debug "set_id of %a: none -> %d" Node.pp n
-            !id_counter;
-          D.set_dom env n !id_counter;
-          DG.set env !id_counter (Node.M.empty, DInt.M.empty);
-          NHT.set env !id_counter n
-      | Some id -> Debug.dprintf3 Common.debug "set_id of %a: %d" Node.pp n id
-    in
-    let get_id env n =
-      (* is this a good idea?
-         TODO: Find out why it crashes occasionally with
-         restricted extensionality *)
-      match Egraph.get_dom env D.key n with
-      | Some id -> id
-      | None ->
-          Debug.dprintf2 Common.debug "get_id of %a: No idea found!" Node.pp n;
-          set_id env n;
-          !id_counter
-    in
-    (set_id, get_id)
-end
+let s_remove_opt s_opt v =
+  match s_opt with
+  | Some s ->
+      let ns = DInt.S.remove v s in
+      if DInt.S.is_empty ns then None else Some ns
+  | None -> raise Not_found
 
 let are_linked env id1 id2 =
   let rec aux (seen : DInt.S.t) (m : Node.t DInt.M.t) =
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index d7f95f7aa7651802d6559ccc4e471583829f6672..576c4507ee19749e6aec128266e9403f4bad5429 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -22,6 +22,7 @@
 open Colibri2_core
 open Colibri2_popop_lib
 open Popop_stdlib
+module HT = Datastructure.Hashtbl (DInt)
 
 let restrict_ext =
   Options.register ~pp:Fmt.bool "Array.res-ext"
@@ -336,3 +337,104 @@ let mk_array_const env v val_gty =
 let distinct_arrays_term a b =
   let diff = Builtin.apply_array_diff a b in
   Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
+
+module MkIHT (V : sig
+  type t
+
+  val pp : t Pp.pp
+  val name : string
+end) =
+struct
+  let db = HT.create V.pp V.name
+  let set (env : Egraph.wt) = HT.set db env
+  let find (env : Egraph.wt) = HT.find db env
+  let find_opt (env : Egraph.wt) = HT.find_opt db env
+  let change ~f (env : Egraph.wt) = HT.change f db env
+  let remove (env : Egraph.wt) = HT.remove db env
+  let iter = HT.iter db
+  let fold f env acc = HT.fold f db env acc
+end
+
+module MkIdDom (N : sig
+  val n1 : string
+  val n2 : string
+  val n3 : string
+end) =
+struct
+  module IVal = struct
+    module T = struct
+      type t = DInt.t [@@deriving eq, ord, hash, show]
+    end
+
+    include T
+    include MkDatatype (T)
+
+    let name = N.n1
+  end
+
+  let merge_hooks = Datastructure.Push.create Fmt.nop N.n2
+
+  let register_merge_hook env (f : Egraph.wt -> 'a -> 'a -> bool -> unit) =
+    Datastructure.Push.push merge_hooks env f
+
+  module D = struct
+    include Dom.Make (struct
+      module Value = Value.Register (IVal)
+
+      type t = IVal.t [@@deriving eq, show]
+
+      let is_singleton _ _ = None
+
+      let key =
+        Dom.Kind.create
+          (module struct
+            type nonrec t = t
+
+            let name = N.n3
+          end)
+
+      let inter _ v _ = Some v
+    end)
+
+    let merge env (d1, n1) (d2, n2) b =
+      (match (d1, n1, d2, n2) with
+      | Some id1, n1, Some id2, n2 ->
+          Datastructure.Push.iter merge_hooks env ~f:(fun f ->
+              f env (n1, id1) (n2, id2) b)
+          (* id1 always stays, b allows to determine which one will become the
+             representative *)
+      | _ ->
+          (* Ideally, should be unreachable, but it is with the test
+             "./colibri2/tests/solve/smt_array/unsat/ite1.smt2"? *)
+          ());
+      merge env (d1, n1) (d2, n2) b
+  end
+
+  let () = Dom.register (module D)
+
+  let set_id, get_id =
+    let id_counter = ref 0 in
+    let set_id ?(new_id_hook = fun _ _ _ _ -> ()) env n =
+      match Egraph.get_dom env D.key n with
+      | None ->
+          incr id_counter;
+          Debug.dprintf3 debug "set_id of %a: none -> %d" Node.pp n !id_counter;
+          D.set_dom env n !id_counter;
+          new_id_hook env !id_counter n true
+      | Some id ->
+          Debug.dprintf3 debug "set_id of %a: %d" Node.pp n id;
+          new_id_hook env id n false
+    in
+    let get_id ?(new_id_hook = fun _ _ _ _ -> ()) env n =
+      (* is this a good idea?
+         TODO: Find out why it crashes occasionally with
+         restricted extensionality *)
+      match Egraph.get_dom env D.key n with
+      | Some id -> id
+      | None ->
+          Debug.dprintf2 debug "get_id of %a: No idea found!" Node.pp n;
+          set_id ~new_id_hook env n;
+          !id_counter
+    in
+    (set_id, get_id)
+end
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 1517008ce0cf77af8388003162c3903288d9015b..1b17f37df9750073aee0bfc6207919d53b70d5cd 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -133,3 +133,43 @@ val mk_distinct_arrays :
 
 val mk_array_const : 'a Egraph.t -> Node.t -> Ground.Ty.t -> Node.t
 val distinct_arrays_term : Expr.term -> Expr.term -> Expr.term
+
+module MkIHT (V : sig
+  type t
+
+  val pp : t Colibri2_popop_lib.Pp.pp
+  val name : string
+end) : sig
+  val set : Egraph.wt -> int -> V.t -> unit
+  val find : Egraph.wt -> int -> V.t
+  val find_opt : Egraph.wt -> int -> V.t option
+  val change : f:(V.t option -> V.t option) -> Egraph.wt -> int -> unit
+  val remove : Egraph.wt -> int -> unit
+  val iter : f:(int -> V.t -> unit) -> Egraph.wt -> unit
+  val fold : (int -> V.t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
+end
+
+module MkIdDom (_ : sig
+  val n1 : string
+  val n2 : string
+  val n3 : string
+end) : sig
+  val register_merge_hook :
+    Egraph.wt ->
+    (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
+    unit
+
+  module D : Dom.DS with type t = int
+
+  val set_id :
+    ?new_id_hook:(Egraph.wt -> int -> Node.t -> bool -> unit) ->
+    Egraph.wt ->
+    Node.t ->
+    unit
+
+  val get_id :
+    ?new_id_hook:(Egraph.wt -> int -> Node.t -> bool -> unit) ->
+    Egraph.wt ->
+    Node.t ->
+    int
+end