diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..8e94dfc7ec307a736ad50f0d18cc0d947bc657d0 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -0,0 +1,3 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/sat/eq.txt b/colibri2/tests/solve/smt_array/sat/eq.txt
new file mode 100644
index 0000000000000000000000000000000000000000..504e6870438fd8fc3efa93ed49e55e39ac819a9a
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/sat/eq.txt
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-fun a () (Array Int Int))
+(assert (= (store a 0 0) (store a 1 0)))
+(check-sat)
\ No newline at end of file
diff --git a/colibri2/tests/solve/smt_array/sat/neq.smt2 b/colibri2/tests/solve/smt_array/sat/neq.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..1bdef9a8e8a023ace5c3d07174ad71fe7363cd81
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/sat/neq.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(assert (not (= a b)))
+(check-sat)
diff --git a/colibri2/theories/array/SharingIsCaring.ml b/colibri2/theories/array/SharingIsCaring.ml
index 7320d9d9b78275d12da676295ed8308429b0b5c1..5445f58d9c66cfefc1837633d26fa67cad9a55a5 100644
--- a/colibri2/theories/array/SharingIsCaring.ml
+++ b/colibri2/theories/array/SharingIsCaring.ml
@@ -116,8 +116,8 @@ 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? *)
+(* 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
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 2721b51cc868024259f3ab9c250e1d1d51d7e5ee..9b57a90847861ff8098990056b47c2b9b9dd145d 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -20,6 +20,10 @@
 (*************************************************************************)
 
 open Colibri2_core
+open Colibri2_popop_lib
+open Popop_stdlib
+open Common
+open Colibri2_theories_quantifiers
 
 (*
   Command line options:
@@ -40,7 +44,100 @@ let converter env f =
   GE_Array_DP.converter env f;
   SharingIsCaring.converter env f
 
+module ArrayModelVal = struct
+  type aval = {
+    ind_ty : Ground.Ty.t;
+    val_ty : Ground.Ty.t;
+    vals : Value.t Value.M.t;
+  }
+
+  include Value.Register (struct
+    module T = struct
+      type t = aval = {
+        ind_ty : Ground.Ty.t;
+        val_ty : Ground.Ty.t;
+        vals : Value.t Value.M.t;
+      }
+      [@@deriving eq, ord, hash]
+
+      let pp fmt { ind_ty; val_ty; _ } =
+        Format.fprintf fmt "Array(%a => %a)" Ground.Ty.pp ind_ty Ground.Ty.pp
+          val_ty
+    end
+
+    include T
+    include MkDatatype (T)
+
+    let name = "Array.model.val"
+  end)
+end
+
+let init_ty d =
+  let open Interp.SeqLim in
+  Interp.Register.ty d (fun d ty ->
+      match ty with
+      | { app = { builtin = Expr.Array; _ }; args = [ ind_ty; val_ty ]; _ } ->
+          Some
+            (let+ seq = of_seq d (Base.Sequence.singleton Value.M.empty)
+             and* indv = Interp.ty d ind_ty
+             and* valv = Interp.ty d val_ty in
+             let vals = Value.M.add indv valv seq in
+             ArrayModelVal.nodevalue
+               (ArrayModelVal.index { ind_ty; val_ty; vals }))
+      | _ -> None)
+
+let interp env n = Opt.get_exn Impossible (Egraph.get_value env n)
+
+let compute d g =
+  match Ground.sem g with
+  | { app = { builtin = Expr.Select; _ }; args; _ } -> (
+      let a, k = IArray.extract2_exn args in
+      let av =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d a))
+      in
+      let kv = interp d k in
+      match Value.M.find_opt kv av.vals with
+      | Some fv -> `Some fv
+      | None -> `Uninterpreted)
+  | { app = { builtin = Expr.Store; _ }; args; _ } ->
+      let a, k, v = IArray.extract3_exn args in
+      let av =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d a))
+      in
+      let kv = interp d k in
+      let vv = interp d v in
+      `Some
+        (ArrayModelVal.of_value { av with vals = Value.M.add kv vv av.vals })
+  | { app = { builtin = Builtin.Array_diff; _ }; args; _ } -> (
+      let a, b = IArray.extract2_exn args in
+      let av =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d a))
+      in
+      let bv =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d b))
+      in
+      match Value.M.choose (Value.M.set_inter av.vals bv.vals) with
+      | k, _ -> `Some k
+      | exception Not_found -> `Uninterpreted)
+  | _ -> `None
+
+let init_check env =
+  Interp.Register.check env (fun d t ->
+      match compute d t with
+      | `None -> NA
+      | `Some r ->
+          Interp.check_of_bool (Value.equal r (interp d (Ground.node t)))
+      | `Uninterpreted ->
+          Interp.check_of_bool (Uninterp.On_uninterpreted_domain.check d t));
+  Interp.Register.compute env (fun d t ->
+      match compute d t with
+      | `None -> NA
+      | `Some v -> Value v
+      | `Uninterpreted -> Uninterp.On_uninterpreted_domain.compute d t)
+
 let init env =
+  init_ty env;
+  init_check env;
   Ground.register_converter env converter;
   GE_Array_DP.init env