diff --git a/colibri2/tests/generate_tests/dune b/colibri2/tests/generate_tests/dune
index b98d6cdc574641ee1550f528627b9c65975fbb30..57d5e80a7ebf198fd061b1f8dde3f663b2a0585c 100644
--- a/colibri2/tests/generate_tests/dune
+++ b/colibri2/tests/generate_tests/dune
@@ -1,2 +1,3 @@
 (executable
- (name generate_dune_tests))
+ (name generate_dune_tests)
+ (libraries cmdliner))
diff --git a/colibri2/tests/generate_tests/generate_dune_tests.ml b/colibri2/tests/generate_tests/generate_dune_tests.ml
index c41f28df095e1d40885615fd0278b137e71888c0..daf43d36b71f055ef5d94064bb322071d5c0cd54 100644
--- a/colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -18,8 +18,6 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-let dir = Sys.argv.(1)
-let result = if Array.length Sys.argv >= 3 then Some Sys.argv.(2) else None
 let cmd = "%{bin:colibri2} --size=50M --time=60s --max-steps 3500"
 
 let check_status cout result file =
@@ -32,7 +30,8 @@ let check_status cout result file =
      --learning --dont-print-result %%{dep:%s})) (package colibri2))\n"
     cmd result file
 
-let print_test cout file =
+let print_test ?result ?(options = []) cout file =
+  ignore options;
   match result with
   | Some "model" ->
       Printf.fprintf cout
@@ -58,16 +57,31 @@ let print_test cout file =
          colibri2))\n"
         cmd file
 
-let () =
-  let files = Sys.readdir dir in
-  Array.sort String.compare files;
-  let files = Array.to_list files in
-  let files =
-    List.filter
-      (fun f ->
-        List.exists (Filename.check_suffix f) [ "cnf"; ".smt2"; ".psmt2" ])
-      files
+let cli_term =
+  let open Cmdliner in
+  let aux dir result options =
+    let files = Sys.readdir dir in
+    Array.sort String.compare files;
+    let files = Array.to_list files in
+    let files =
+      List.filter
+        (fun f ->
+          List.exists (Filename.check_suffix f) [ "cnf"; ".smt2"; ".psmt2" ])
+        files
+    in
+    let cout = open_out (Filename.concat dir "dune.inc") in
+    List.iter (print_test ?result ~options cout) files;
+    close_out cout
+  in
+  let dir = Arg.(required & pos 0 (some string) None & info []) in
+  let result = Arg.(value & pos 1 (some string) None & info []) in
+  let options =
+    let doc = "A string containing command line options to pass to Colibri2." in
+    Arg.(value & opt_all string [] & info [ "options" ] ~doc)
   in
-  let cout = open_out (Filename.concat dir "dune.inc") in
-  List.iter (print_test cout) files;
-  close_out cout
+  Cmd.v (Cmd.info "run") Term.(const aux $ dir $ result $ options)
+
+let () =
+  match Cmdliner.Cmd.eval_value cli_term with
+  | Ok (`Version | `Help | `Ok ()) -> exit 0
+  | Error (`Parse | `Term | `Exn) -> exit 2
diff --git a/colibri2/theories/array/GE_Array_DP.ml b/colibri2/theories/array/GE_Array_DP.ml
index b6ae7f66e1ecc705c0e34711ee12f8fb80468c4e..82b7ff309fa85ca6a2401661150ee1424699526d 100644
--- a/colibri2/theories/array/GE_Array_DP.ml
+++ b/colibri2/theories/array/GE_Array_DP.ml
@@ -27,36 +27,6 @@ open Colibri2_theories_quantifiers
 module GHT = Datastructure.Hashtbl (Ground)
 module GTHT = Datastructure.Hashtbl (Ground.Ty)
 
-let restrict_ext =
-  Options.register ~pp:Fmt.bool "Array.res-ext"
-    Cmdliner.Arg.(
-      value & flag
-      & info [ "array-res-ext" ] ~doc:"Restrict the extensionality rule")
-
-let restrict_aup =
-  Options.register ~pp:Fmt.bool "Array.res-aup"
-    Cmdliner.Arg.(
-      value & flag & info [ "array-res-aup" ] ~doc:"Restrict the ⇑ rule")
-
-let extended_comb =
-  Options.register ~pp:Fmt.bool "Array.res-comb"
-    Cmdliner.Arg.(
-      value & flag & info [ "array-ext-comb" ] ~doc:"Extended combinators")
-
-let blast_rule =
-  Options.register ~pp:Fmt.bool "Array.blast-rule"
-    Cmdliner.Arg.(
-      value & flag
-      & info [ "array-blast-rule" ]
-          ~doc:"Use the array blast rule when it is suitable")
-
-let default_values =
-  Options.register ~pp:Fmt.bool "Array.def-values"
-    Cmdliner.Arg.(
-      value & flag
-      & info [ "array-def-values" ]
-          ~doc:"Use inference rules for default values")
-
 type size = Inf | Finite of { num : int; size : int } [@@deriving show]
 
 let check_gty_num_size =
@@ -352,36 +322,6 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
   in
   (apply_res_ext_2_1, apply_res_ext_2_2)
 
-(** applied the res-ext rule only on neighbours in the diff-graphs  *)
-let init env =
-  (* extáµ£ (restricted extensionality):
-     - (a = b) ≡ false |> (a[k] ≠ b[k])
-     - a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
-  if Options.get env restrict_ext then
-    if Options.get env use_diff_graph then (
-      (* (a = b) ≡ false |> (a[k] ≠ b[k]) (when a and b are neighbours) *)
-      Equality.register_hook_new_disequality env (apply_res_ext_1_2 env);
-      (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k])
-         (when a and b are neighbours) *)
-      Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_2 env))
-    else (
-      (* (a = b) ≡ false |> (a[k] ≠ b[k]) *)
-      (* TODO: Are a and b always of the same type? *)
-      Equality.register_hook_new_disequality env (apply_res_ext_1_1 env);
-      (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
-      Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_1 env));
-  let l = [ (adown_pattern, adown_run) ] in
-  let l =
-    if Options.get env restrict_aup then (raup_pattern, raup_run) :: l
-    else (aup_pattern, aup_run) :: l
-  in
-  let l =
-    if Options.get env extended_comb then
-      (const_read_pattern, const_read_run) :: l
-    else l
-  in
-  List.iter (fun (p, r) -> InvertedPath.add_callback env p r) l
-
 let new_array =
   let db = Datastructure.Push.create Ground.pp "Array.db" in
   fun env ind_gty val_gty f ->
@@ -615,177 +555,3 @@ let apply_blast_rule =
     in
     Egraph.register env n;
     Boolean.set_true env n
-
-let converter env (f : Ground.t) =
-  let s = Ground.sem f in
-  let fn = Ground.node f in
-  let f_is_array =
-    match s.ty with
-    | { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ]; _ } ->
-        add_array_gty env fn ind_gty val_gty;
-        Id_dom.set_id env fn;
-        new_array env ind_gty val_gty f;
-        true
-    | _ -> false
-  in
-  match s with
-  | { app = { builtin = Expr.Base; id_ty; _ }; args; tyargs; _ } ->
-      if IArray.is_empty args then (
-        if Options.get env restrict_aup && f_is_array then
-          (* update of the Linearity domain *)
-          Linearity_dom.upd_dom env fn Empty)
-      else if Options.get env restrict_ext then (
-        (* update of the Foreign domain *)
-        let subst, arg_tys =
-          match id_ty.ty_descr with
-          | Pi (tyvl, { ty_descr = Expr.Arrow (ptys, _); _ }) ->
-              ( List.fold_left2
-                  (fun m k v -> Expr.Ty.Var.M.add k v m)
-                  Expr.Ty.Var.M.empty tyvl tyargs,
-                ptys )
-          | Expr.Arrow (ptys, _) -> (Expr.Ty.Var.M.empty, ptys)
-          | _ -> (Expr.Ty.Var.M.empty, [])
-        in
-        assert (arg_tys <> []);
-        IArray.iteri
-          ~f:(fun i n ->
-            let gty = Ground.Ty.convert subst (List.nth arg_tys i) in
-            match gty with
-            | { app = { builtin = Expr.Array; _ }; _ } ->
-                Ground.add_ty env n gty;
-                Foreign_dom.set_dom env gty n IsForeign
-            | _ -> ())
-          args)
-  | {
-   app = { builtin = Expr.Select; _ };
-   args;
-   tyargs = [ ind_gty; val_gty ];
-   _;
-  } ->
-      Array_value.propagate_value env f;
-      let a, i = IArray.extract2_exn args in
-      Egraph.register env a;
-      Egraph.register env i;
-      let gty = Ground.Ty.array ind_gty val_gty in
-      Ground.add_ty env a gty;
-      (* update of the Foreign domain *)
-      if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then (
-        Ground.add_ty env i ind_gty;
-        Foreign_dom.set_dom env gty i IsForeign);
-      if Options.get env extended_comb then (
-        (* when a new read is encountered, check if map⇑ can be applied *)
-        Array_dom.add_read ~hook:add_array_read_hook env a i;
-        (* 𝝐≠: v = a[i], i is not 𝝐 |> i ≠ 𝝐 or blast *)
-        let subst =
-          mk_subst
-            [ (STV.va, a); (STV.vi, i) ]
-            [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
-        in
-        let eps_term = Builtin.apply_array_def_index STV.ta in
-        let eps_node = convert ~subst env eps_term in
-        Egraph.register env eps_node;
-        if not (Egraph.is_equal env i eps_node) then (
-          let ind_gty, _ = array_gty_args ind_gty in
-          if check_gty_num_size env ind_gty then
-            (* application of the blast rule *)
-            apply_blast_rule env a ind_gty val_gty
-          else
-            (* application of 𝝐≠ *)
-            let i_eps_neq_node =
-              convert ~subst env (Expr.Term.neq eps_term STV.ti)
-            in
-            Egraph.register env i_eps_neq_node;
-            Boolean.set_true env i_eps_neq_node))
-  | {
-   app = { builtin = Expr.Store; _ };
-   args;
-   tyargs = [ ind_gty; val_gty ];
-   _;
-  } ->
-      Array_value.propagate_value env f;
-      let a, k, v = IArray.extract3_exn args in
-      Egraph.register env a;
-      Egraph.register env k;
-      Egraph.register env v;
-      add_array_gty env a ind_gty val_gty;
-      Id_dom.set_id env a;
-      (* update of the Linearity domain *)
-      if Options.get env restrict_aup then
-        Linearity_dom.upd_dom env fn (Linear a);
-      (* application of the `idx` rule *)
-      let subst =
-        mk_subst
-          [ (STV.va, a); (STV.vk, k); (STV.vv, v) ]
-          [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
-      in
-      let store_term = mk_store_term STV.ta STV.tk STV.tv in
-      let rn =
-        convert ~subst env
-          (Expr.Term.eq (mk_select_term store_term STV.tk) STV.tv)
-      in
-      Egraph.register env rn;
-      Boolean.set_true env rn;
-      (* application of the `U𝛿` rule *)
-      if Options.get env default_values then (
-        let eq_term =
-          Expr.Term.eq
-            (Builtin.apply_array_def_value store_term)
-            (Builtin.apply_array_def_value STV.ta)
-        in
-        let eq_node = convert ~subst env eq_term in
-        Egraph.register env eq_node;
-        Boolean.set_true env eq_node)
-  | {
-   app = { builtin = Builtin.Array_diff; _ };
-   args;
-   tyargs = [ ind_gty; val_gty ];
-   _;
-  } ->
-      Array_value.propagate_value env f;
-      let a, b = IArray.extract2_exn args in
-      Egraph.register env a;
-      Egraph.register env b;
-      Id_dom.set_id env a;
-      Id_dom.set_id env b;
-      add_array_gty env a ind_gty val_gty;
-      add_array_gty env b ind_gty val_gty
-  | {
-   app = { builtin = Builtin.Array_const; _ };
-   (* TODO: what should be done with the free ind_ty variable? *)
-   args;
-   tyargs = [ val_gty ];
-   _;
-  } ->
-      Array_value.propagate_value env f;
-      let v = IArray.extract1_exn args in
-      Egraph.register env v;
-      (* application of the `K𝛿` rule *)
-      if Options.get env default_values then (
-        let subst = mk_subst [ (STV.vv, v) ] [ (STV.val_ty_var, val_gty) ] in
-        (* TODO: make a separate array node and set it's type? *)
-        let eq_node =
-          convert ~subst env
-            (Expr.Term.eq
-               (Builtin.apply_array_def_value
-                  (Builtin.apply_array_const STV.tv))
-               STV.tv)
-        in
-        Egraph.register env eq_node;
-        Boolean.set_true env eq_node)
-  | {
-   app = { builtin = Builtin.Array_map; _ };
-   args;
-   tyargs = [ bi_ind_ty; bi_val_ty; a_val_ty ];
-   _;
-  }
-    when Options.get env extended_comb || Options.get env default_values ->
-      (if Options.get env extended_comb then
-       let f_arity = IArray.length args - 1 in
-       IArray.iteri args ~f:(fun i n ->
-           if i > 0 then (
-             Id_dom.set_id env n;
-             add_array_gty env n bi_ind_ty bi_val_ty;
-             Array_dom.add_map_parent ~hook:add_array_map_hook env n f
-               { bi_ind_ty; bi_val_ty; a_val_ty; f_arity })));
-      new_map env f
-  | _ -> ()
diff --git a/colibri2/theories/array/GE_Array_DP.mli b/colibri2/theories/array/GE_Array_DP.mli
index 325a7d15828a9af2d030f4f9a8b9896543292cec..1066dc7077068e360c992dcf1262792d32f62d54 100644
--- a/colibri2/theories/array/GE_Array_DP.mli
+++ b/colibri2/theories/array/GE_Array_DP.mli
@@ -19,5 +19,34 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-val init : Egraph.wt -> unit
-val converter : Egraph.wt -> Ground.t -> unit
+open Colibri2_theories_quantifiers
+
+val check_gty_num_size : Egraph.rw Egraph.t -> Ground.Ty.t -> bool
+val adown_pattern : Pattern.t
+val adown_run : Egraph.wt -> Ground.Subst.t -> unit
+val aup_pattern : Pattern.t
+val aup_run : Egraph.wt -> Ground.Subst.t -> unit
+val raup_pattern : Pattern.t
+val raup_run : Egraph.wt -> Ground.Subst.t -> unit
+val const_read_pattern : Pattern.t
+val const_read_run : Egraph.wt -> Ground.Subst.t -> unit
+val apply_res_ext_1_1 : Egraph.wt -> Node.S.t -> unit
+val apply_res_ext_1_2 : Egraph.wt -> Node.S.t -> unit
+val apply_res_ext_2_1 : Egraph.wt -> Ground.Ty.t -> Node.t -> unit
+val apply_res_ext_2_2 : Egraph.wt -> Ground.Ty.t -> Node.t -> unit
+val new_array : Egraph.wt -> Ground.Ty.t -> Ground.Ty.t -> Ground.t -> unit
+
+val map_adowm :
+  Expr.term ->
+  Expr.term ->
+  Expr.term list ->
+  Pattern.t * (Egraph.wt -> Ground.Subst.t -> unit)
+
+val add_array_read_hook :
+  Egraph.wt -> Node.t -> Array_dom.map_info Ground.M.t -> unit
+
+val add_array_map_hook :
+  Egraph.wt -> Ground.t -> Node.S.t -> Array_dom.map_info -> unit
+
+val new_map : Egraph.rw Egraph.t -> Ground.t -> unit
+val apply_blast_rule : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit
diff --git a/colibri2/theories/array/SharingIsCaring.ml b/colibri2/theories/array/SharingIsCaring.ml
index 00fdab2dd98fcafa2f263c9e50ac08482da03df0..8421192d8f12cc01d59b24afc252ca4fc559155b 100644
--- a/colibri2/theories/array/SharingIsCaring.ml
+++ b/colibri2/theories/array/SharingIsCaring.ml
@@ -20,7 +20,6 @@
 (*************************************************************************)
 
 open Colibri2_core
-open Colibri2_popop_lib
 open Common
 open DiffGraph
 
@@ -82,66 +81,3 @@ let update_np_dp env a b k =
   let ap = { node = a; id = aid } in
   let bp = { node = b; id = bid } in
   add_edge env ap bp k
-
-let init env =
-  if Options.get env use_diff_graph then
-    Id_dom.register_merge_hook env eq_arrays_norm
-
-(* TODO: should this converter not redo what was already done in
-   GEADP.converter? is it safe? *)
-let converter env (f : Ground.t) =
-  if Options.get env use_diff_graph then
-    let s = Ground.sem f in
-    match s with
-    | {
-     app = { builtin = Expr.Store; _ };
-     args;
-     tyargs = [ ind_gty; val_gty ];
-     _;
-    } ->
-        Array_value.propagate_value env f;
-        let a = Ground.node f in
-        let b, k, v = IArray.extract3_exn args in
-        Egraph.register env a;
-        (* is this necessary? *)
-        Egraph.register env b;
-        Egraph.register env k;
-        Egraph.register env v;
-        Id_dom.set_id env a;
-        Id_dom.set_id env b;
-        add_array_gty env a ind_gty val_gty;
-        add_array_gty env b ind_gty val_gty;
-        let ak =
-          sem_to_node
-            (Ground.apply env Expr.Term.Const.Array.select [ ind_gty; val_gty ]
-               (IArray.of_list [ a; k ]))
-        in
-        Egraph.register env ak;
-        if not (Egraph.is_equal env ak v) then (
-          let agty =
-            Ground.Ty.{ app = Expr.Ty.Const.array; args = [ ind_gty; val_gty ] }
-          in
-          let akv_eq =
-            sem_to_node
-              (Ground.apply env Expr.Term.Const.eq [ agty ]
-                 (IArray.of_list [ ak; v ]))
-          in
-          Egraph.register env akv_eq;
-          Boolean.set_true env akv_eq);
-        let bk =
-          sem_to_node
-            (Ground.apply env Expr.Term.Const.Array.select [ ind_gty; val_gty ]
-               (IArray.of_list [ b; k ]))
-        in
-        Egraph.register env bk;
-        if Egraph.is_equal env bk v then (
-          let eqn =
-            sem_to_node
-              (Ground.apply env Expr.Term.Const.eq
-                 [ Ground.Ty.array ind_gty val_gty ]
-                 (IArray.of_list [ a; b ]))
-          in
-          Egraph.register env eqn;
-          Boolean.set_true env eqn)
-        else update_np_dp env a b k
-    | _ -> ()
diff --git a/colibri2/theories/array/SharingIsCaring.mli b/colibri2/theories/array/SharingIsCaring.mli
index 325a7d15828a9af2d030f4f9a8b9896543292cec..a852135358066d611a4aaa9b3bdb89a7a2ec72e2 100644
--- a/colibri2/theories/array/SharingIsCaring.mli
+++ b/colibri2/theories/array/SharingIsCaring.mli
@@ -19,5 +19,5 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-val init : Egraph.wt -> unit
-val converter : Egraph.wt -> Ground.t -> unit
+val eq_arrays_norm : Egraph.wt -> DiffGraph.t -> DiffGraph.t -> unit
+val update_np_dp : Egraph.wt -> Node.t -> Node.t -> Node.t -> unit
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 7fe10b4d2858fe3e5b89a8be3a40d47504b9c4a7..f01d689b8d7b81feeb3c25e3f9002835319b3021 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -20,6 +20,11 @@
 (*************************************************************************)
 
 open Colibri2_core
+open Colibri2_popop_lib
+open Common
+open Colibri2_theories_quantifiers
+open GE_Array_DP
+open SharingIsCaring
 
 (*
   Command line options:
@@ -36,14 +41,253 @@ open Colibri2_core
     - "--array-diff-graph": uses the diff graph
 *)
 
-let converter env f =
-  GE_Array_DP.converter env f;
-  SharingIsCaring.converter env f
+let converter env (f : Ground.t) =
+  let s = Ground.sem f in
+  let fn = Ground.node f in
+  let f_is_array =
+    match s.ty with
+    | { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ]; _ } ->
+        add_array_gty env fn ind_gty val_gty;
+        Id_dom.set_id env fn;
+        new_array env ind_gty val_gty f;
+        true
+    | _ -> false
+  in
+  match s with
+  | { app = { builtin = Expr.Base; id_ty; _ }; args; tyargs; _ } ->
+      if IArray.is_empty args then (
+        if Options.get env restrict_aup && f_is_array then
+          (* update of the Linearity domain *)
+          Linearity_dom.upd_dom env fn Empty)
+      else if Options.get env restrict_ext then (
+        (* update of the Foreign domain *)
+        let subst, arg_tys =
+          match id_ty.ty_descr with
+          | Pi (tyvl, { ty_descr = Expr.Arrow (ptys, _); _ }) ->
+              ( List.fold_left2
+                  (fun m k v -> Expr.Ty.Var.M.add k v m)
+                  Expr.Ty.Var.M.empty tyvl tyargs,
+                ptys )
+          | Expr.Arrow (ptys, _) -> (Expr.Ty.Var.M.empty, ptys)
+          | _ -> (Expr.Ty.Var.M.empty, [])
+        in
+        assert (arg_tys <> []);
+        IArray.iteri
+          ~f:(fun i n ->
+            let gty = Ground.Ty.convert subst (List.nth arg_tys i) in
+            match gty with
+            | { app = { builtin = Expr.Array; _ }; _ } ->
+                Ground.add_ty env n gty;
+                Foreign_dom.set_dom env gty n IsForeign
+            | _ -> ())
+          args)
+  | {
+   app = { builtin = Expr.Select; _ };
+   args;
+   tyargs = [ ind_gty; val_gty ];
+   _;
+  } ->
+      Array_value.propagate_value env f;
+      let ai = Ground.node f in
+      Egraph.register env ai;
+      let a, i = IArray.extract2_exn args in
+      Egraph.register env a;
+      Egraph.register env i;
+      let gty = Ground.Ty.array ind_gty val_gty in
+      Ground.add_ty env a gty;
+      (* update of the Foreign domain *)
+      if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then (
+        Ground.add_ty env i ind_gty;
+        Foreign_dom.set_dom env gty i IsForeign);
+      if Options.get env extended_comb then (
+        (* when a new read is encountered, check if map⇑ can be applied *)
+        Array_dom.add_read ~hook:add_array_read_hook env a i;
+        (* 𝝐≠: v = a[i], i is not 𝝐 |> i ≠ 𝝐 or blast *)
+        let subst =
+          mk_subst
+            [ (STV.va, a); (STV.vi, i) ]
+            [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
+        in
+        let eps_term = Builtin.apply_array_def_index STV.ta in
+        let eps_node = convert ~subst env eps_term in
+        Egraph.register env eps_node;
+        if not (Egraph.is_equal env i eps_node) then (
+          let ind_gty, _ = array_gty_args ind_gty in
+          if check_gty_num_size env ind_gty then
+            (* application of the blast rule *)
+            apply_blast_rule env a ind_gty val_gty
+          else
+            (* application of 𝝐≠ *)
+            let i_eps_neq_node =
+              convert ~subst env (Expr.Term.neq eps_term STV.ti)
+            in
+            Egraph.register env i_eps_neq_node;
+            Boolean.set_true env i_eps_neq_node))
+  | {
+   app = { builtin = Expr.Store; _ };
+   args;
+   tyargs = [ ind_gty; val_gty ];
+   _;
+  } ->
+      Array_value.propagate_value env f;
+      let a = Ground.node f in
+      Egraph.register env a;
+      let b, k, v = IArray.extract3_exn args in
+      Egraph.register env b;
+      Egraph.register env k;
+      Egraph.register env v;
+      add_array_gty env a ind_gty val_gty;
+      add_array_gty env b ind_gty val_gty;
+      Id_dom.set_id env a;
+      Id_dom.set_id env b;
+      (* update of the Linearity domain *)
+      if Options.get env restrict_aup then
+        Linearity_dom.upd_dom env fn (Linear b);
+      (* application of the `idx` rule *)
+      let subst =
+        mk_subst
+          [ (STV.va, b); (STV.vk, k); (STV.vv, v) ]
+          [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
+      in
+      let store_term = mk_store_term STV.ta STV.tk STV.tv in
+      let rn =
+        convert ~subst env
+          (Expr.Term.eq (mk_select_term store_term STV.tk) STV.tv)
+      in
+      Egraph.register env rn;
+      Boolean.set_true env rn;
+      (* application of the `U𝛿` rule *)
+      if Options.get env default_values then (
+        let eq_term =
+          Expr.Term.eq
+            (Builtin.apply_array_def_value store_term)
+            (Builtin.apply_array_def_value STV.ta)
+        in
+        let eq_node = convert ~subst env eq_term in
+        Egraph.register env eq_node;
+        Boolean.set_true env eq_node);
+      if Options.get env use_diff_graph then (
+        let ak =
+          sem_to_node
+            (Ground.apply env Expr.Term.Const.Array.select [ ind_gty; val_gty ]
+               (IArray.of_list [ a; k ]))
+        in
+        Egraph.register env ak;
+        if not (Egraph.is_equal env ak v) then (
+          let agty =
+            Ground.Ty.{ app = Expr.Ty.Const.array; args = [ ind_gty; val_gty ] }
+          in
+          let akv_eq =
+            sem_to_node
+              (Ground.apply env Expr.Term.Const.eq [ agty ]
+                 (IArray.of_list [ ak; v ]))
+          in
+          Egraph.register env akv_eq;
+          Boolean.set_true env akv_eq);
+        let bk =
+          sem_to_node
+            (Ground.apply env Expr.Term.Const.Array.select [ ind_gty; val_gty ]
+               (IArray.of_list [ b; k ]))
+        in
+        Egraph.register env bk;
+        if Egraph.is_equal env bk v then (
+          (* is this necessary? *)
+          let eqn =
+            sem_to_node
+              (Ground.apply env Expr.Term.Const.eq
+                 [ Ground.Ty.array ind_gty val_gty ]
+                 (IArray.of_list [ a; b ]))
+          in
+          Egraph.register env eqn;
+          Boolean.set_true env eqn)
+        else update_np_dp env a b k)
+  | {
+   app = { builtin = Builtin.Array_diff; _ };
+   args;
+   tyargs = [ ind_gty; val_gty ];
+   _;
+  } ->
+      Array_value.propagate_value env f;
+      let a, b = IArray.extract2_exn args in
+      Egraph.register env a;
+      Egraph.register env b;
+      Id_dom.set_id env a;
+      Id_dom.set_id env b;
+      add_array_gty env a ind_gty val_gty;
+      add_array_gty env b ind_gty val_gty
+  | {
+   app = { builtin = Builtin.Array_const; _ };
+   (* TODO: what should be done with the free ind_ty variable? *)
+   args;
+   tyargs = [ val_gty ];
+   _;
+  } ->
+      Array_value.propagate_value env f;
+      let v = IArray.extract1_exn args in
+      Egraph.register env v;
+      (* application of the `K𝛿` rule *)
+      if Options.get env default_values then (
+        let subst = mk_subst [ (STV.vv, v) ] [ (STV.val_ty_var, val_gty) ] in
+        (* TODO: make a separate array node and set it's type? *)
+        let eq_node =
+          convert ~subst env
+            (Expr.Term.eq
+               (Builtin.apply_array_def_value
+                  (Builtin.apply_array_const STV.tv))
+               STV.tv)
+        in
+        Egraph.register env eq_node;
+        Boolean.set_true env eq_node)
+  | {
+   app = { builtin = Builtin.Array_map; _ };
+   args;
+   tyargs = [ bi_ind_ty; bi_val_ty; a_val_ty ];
+   _;
+  }
+    when Options.get env extended_comb || Options.get env default_values ->
+      (if Options.get env extended_comb then
+       let f_arity = IArray.length args - 1 in
+       IArray.iteri args ~f:(fun i n ->
+           if i > 0 then (
+             Id_dom.set_id env n;
+             add_array_gty env n bi_ind_ty bi_val_ty;
+             Array_dom.add_map_parent ~hook:add_array_map_hook env n f
+               { bi_ind_ty; bi_val_ty; a_val_ty; f_arity })));
+      new_map env f
+  | _ -> ()
 
 let init env =
   Array_value.init_ty env;
   Array_value.init_check env;
   Ground.register_converter env converter;
-  GE_Array_DP.init env
+  if Options.get env use_diff_graph then
+    Id_dom.register_merge_hook env eq_arrays_norm;
+  (* extáµ£ (restricted extensionality):
+     - (a = b) ≡ false |> (a[k] ≠ b[k])
+     - a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
+  if Options.get env restrict_ext then
+    if Options.get env use_diff_graph then (
+      (* (a = b) ≡ false |> (a[k] ≠ b[k]) (when a and b are neighbours) *)
+      Equality.register_hook_new_disequality env (apply_res_ext_1_2 env);
+      (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k])
+         (when a and b are neighbours) *)
+      Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_2 env))
+    else (
+      (* (a = b) ≡ false |> (a[k] ≠ b[k]) *)
+      (* TODO: Are a and b always of the same type? *)
+      Equality.register_hook_new_disequality env (apply_res_ext_1_1 env);
+      (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
+      Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_1 env));
+  let l = [ (adown_pattern, adown_run) ] in
+  let l =
+    if Options.get env restrict_aup then (raup_pattern, raup_run) :: l
+    else (aup_pattern, aup_run) :: l
+  in
+  let l =
+    if Options.get env extended_comb then
+      (const_read_pattern, const_read_run) :: l
+    else l
+  in
+  List.iter (fun (p, r) -> InvertedPath.add_callback env p r) l
 
 let () = Init.add_default_theory init
diff --git a/colibri2/theories/array/array_value.ml b/colibri2/theories/array/array_value.ml
index 5a81747324ae509cba75954f2bd0ddab0c406c2b..bb91aea0a5a5ebab708b89f71c2f77b4b483530c 100644
--- a/colibri2/theories/array/array_value.ml
+++ b/colibri2/theories/array/array_value.ml
@@ -107,7 +107,7 @@ let all_arrays d ind_ty val_ty =
   in
   let vals = Interp.SeqLim.limit d (Interp.SeqLim.concat vals) in
   let open Interp.SeqLim in
-  let+ vals and* other = Interp.ty d val_ty in
+  let+ vals = vals and* other = Interp.ty d val_ty in
   ArrayModelVal.nodevalue (ArrayModelVal.index { ind_ty; val_ty; vals; other })
 
 let init_ty d =
diff --git a/colibri2/theories/array/array_value.mli b/colibri2/theories/array/array_value.mli
new file mode 100644
index 0000000000000000000000000000000000000000..4c5ac269eace2a03dca16d02ae39676a87a01abf
--- /dev/null
+++ b/colibri2/theories/array/array_value.mli
@@ -0,0 +1,24 @@
+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+val init_ty : Egraph.wt -> unit
+val init_check : Egraph.wt -> unit
+val propagate_value : Egraph.wt -> Ground.t -> unit
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index afaac70e9fe1db20fe1ddc13dfc191017a3c2868..0bfd05688106aabcc502afb06b747d670661bb2b 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -23,6 +23,36 @@ open Colibri2_core
 open Colibri2_popop_lib
 open Popop_stdlib
 
+let restrict_ext =
+  Options.register ~pp:Fmt.bool "Array.res-ext"
+    Cmdliner.Arg.(
+      value & flag
+      & info [ "array-res-ext" ] ~doc:"Restrict the extensionality rule")
+
+let restrict_aup =
+  Options.register ~pp:Fmt.bool "Array.res-aup"
+    Cmdliner.Arg.(
+      value & flag & info [ "array-res-aup" ] ~doc:"Restrict the ⇑ rule")
+
+let extended_comb =
+  Options.register ~pp:Fmt.bool "Array.res-comb"
+    Cmdliner.Arg.(
+      value & flag & info [ "array-ext-comb" ] ~doc:"Extended combinators")
+
+let blast_rule =
+  Options.register ~pp:Fmt.bool "Array.blast-rule"
+    Cmdliner.Arg.(
+      value & flag
+      & info [ "array-blast-rule" ]
+          ~doc:"Use the array blast rule when it is suitable")
+
+let default_values =
+  Options.register ~pp:Fmt.bool "Array.def-values"
+    Cmdliner.Arg.(
+      value & flag
+      & info [ "array-def-values" ]
+          ~doc:"Use inference rules for default values")
+
 let use_diff_graph =
   Options.register ~pp:Fmt.bool "Array.diff-graph"
     Cmdliner.Arg.(
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index b1aaf85e7fcf3a95c2f94978780deb67072986bb..1c318c7c64d9fb8ec19ba084f1364427c9463edc 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -19,6 +19,11 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
+val restrict_ext : bool Options.t
+val restrict_aup : bool Options.t
+val extended_comb : bool Options.t
+val blast_rule : bool Options.t
+val default_values : bool Options.t
 val use_diff_graph : bool Options.t
 val debug : Debug.flag
 val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t