diff --git a/colibri2/tests/solve/smt_array/errors/ite_2.txt b/colibri2/tests/solve/smt_array/errors/ite_2.txt
deleted file mode 100644
index b88968a7265d3f75ca42702fe1a9879adba377fd..0000000000000000000000000000000000000000
--- a/colibri2/tests/solve/smt_array/errors/ite_2.txt
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic ALL)
-(declare-fun i () Int)
-(declare-fun a () (Array Int Int))
-(declare-fun j () Int)
-(declare-fun v1 () Int)
-(declare-fun v2 () Int)
-(assert (not
-  (ite
-    (= (store a j v1) (store (store a i v2) j v1))
-    (= i j)
-    true
-  )))
-(check-sat)
\ No newline at end of file
diff --git a/colibri2/tests/solve/smt_array/errors/notes.txt b/colibri2/tests/solve/smt_array/errors/notes.txt
index 16453a4205eead4c65af3eeb7f9ae0ecd4e4d8dc..339eeef09a9cc131fa27d401e466dbf4505b0b1b 100644
--- a/colibri2/tests/solve/smt_array/errors/notes.txt
+++ b/colibri2/tests/solve/smt_array/errors/notes.txt
@@ -1,4 +1,3 @@
 
 - eq.txt: timeout
-- ite_1.txt: unsound (--array-res-ext)
-- ite_2.txt: timeout (--array-res-ext)
+
diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
index 8e94dfc7ec307a736ad50f0d18cc0d947bc657d0..ffb6db07fc8988d2a0664480f8e183bb991878be 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -1,3 +1,6 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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 --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/errors/ite_1.txt b/colibri2/tests/solve/smt_array/sat/imp1.smt2
similarity index 70%
rename from colibri2/tests/solve/smt_array/errors/ite_1.txt
rename to colibri2/tests/solve/smt_array/sat/imp1.smt2
index fb808e901b47aeca2e09473f0eb9a233b3aae710..a6c9d6fff44c904a0c0bfca658a555cd75a612db 100644
--- a/colibri2/tests/solve/smt_array/errors/ite_1.txt
+++ b/colibri2/tests/solve/smt_array/sat/imp1.smt2
@@ -6,12 +6,6 @@
 (declare-fun j () I)
 (declare-fun v1 () E)
 (declare-fun v2 () E)
-; (assert (not
-;   (ite
-;     (= (store a j v1) (store (store a i v2) j v1))
-;     (= i j)
-;     true
-;   )))
 (assert (= (store a j v1) (store (store a i v2) j v1)))
 (assert (not (= i j)))
 (check-sat)
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 63dfe2c8614d20b54c342c903481e555bc29a5bd..afaac70e9fe1db20fe1ddc13dfc191017a3c2868 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -175,8 +175,9 @@ module Builtin = struct
     apply_cst array_diff [ ind_ty; val_ty ] [ a; b ]
 
   let apply_array_const v =
-    let wildcard = Expr.Ty.Var.wildcard () in
-    apply_cst array_const [ Expr.Ty.of_var wildcard; v.Expr.term_ty ] [ v ]
+    apply_cst array_const
+      [ Expr.Ty.of_var (Expr.Ty.Var.wildcard ()); v.Expr.term_ty ]
+      [ v ]
 
   let apply_array_def_index a =
     let ind_ty, val_ty = array_ty_args a.Expr.term_ty in
diff --git a/colibri2/theories/nseq/nseq.ml b/colibri2/theories/nseq/nseq.ml
index 71dda86de37eb77e8f2596aac7f5d1256007613b..ef41aa585d0e5cd9b613b389e82cd4ec375c63d8 100644
--- a/colibri2/theories/nseq/nseq.ml
+++ b/colibri2/theories/nseq/nseq.ml
@@ -114,7 +114,7 @@ module Builtin = struct
       (Expr.Ty.pi [ val_ty_var ]
          (Expr.Ty.arrow [ val_nseq_ty; int_ty; int_ty ] val_nseq_ty))
 
-  let get_nseq_val : Expr.ty -> Expr.ty = function
+  let get_nseq_arg : Expr.ty -> Expr.ty = function
     | { ty_descr = TyApp ({ builtin = NSeq; _ }, [ val_ty ]); _ } -> val_ty
     | ty -> failwith (Fmt.str "'%a' is not an nseq type!" Expr.Ty.print ty)
 
@@ -126,57 +126,57 @@ module Builtin = struct
            env s
            (fun ty -> Expr.Ty.apply f [ ty ]))
     in
-    let app1 env s f =
+    let app1 ?(get_nseq_arg = Fun.id) env s f =
       `Term
         (Dolmen_type.Base.term_app1
            (module Dolmen_loop.Typer.T)
            env s
            (fun a ->
-             Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a ]))
+             Expr.Term.apply_cst f [ get_nseq_arg a.Expr.term_ty ] [ a ]))
     in
-    let app2 env s f =
+    let app2 ?(get_nseq_arg = Fun.id) env s f =
       `Term
         (Dolmen_type.Base.term_app2
            (module Dolmen_loop.Typer.T)
            env s
            (fun a b ->
-             Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a; b ]))
+             Expr.Term.apply_cst f [ get_nseq_arg a.Expr.term_ty ] [ a; b ]))
     in
-    let app3 env s f =
+    let app3 env ?(get_nseq_arg = Fun.id) s f =
       `Term
         (Dolmen_type.Base.term_app2
            (module Dolmen_loop.Typer.T)
            env s
            (fun a b ->
-             Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a; b ]))
+             Expr.Term.apply_cst f [ get_nseq_arg a.Expr.term_ty ] [ a; b ]))
     in
     Expr.add_builtins (fun env s ->
         match s with
         | Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "NSeq" } ->
             ty_app1 env s nseq_ty_const
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_get" } ->
+            app2 ~get_nseq_arg env s nseq_get
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_set" } ->
+            app3 ~get_nseq_arg env s nseq_set
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_first" } ->
-            app1 env s nseq_first
+            app1 ~get_nseq_arg env s nseq_first
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_last" } ->
-            app1 env s nseq_last
+            app1 ~get_nseq_arg env s nseq_last
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_content" } ->
-            app1 env s nseq_content
+            app1 ~get_nseq_arg env s nseq_content
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_length" } ->
-            app1 env s nseq_length
-        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_get" } ->
-            app2 env s nseq_get
-        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_set" } ->
-            app3 env s nseq_set
+            app1 ~get_nseq_arg env s nseq_length
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_eq" } ->
-            app2 env s nseq_get
+            app2 ~get_nseq_arg env s nseq_get
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_const" } ->
             app3 env s nseq_const
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_empty" } ->
             app2 env s nseq_empty
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_concat" } ->
-            app2 env s nseq_concat
+            app2 ~get_nseq_arg env s nseq_concat
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_relocate" } ->
-            app2 env s nseq_relocate
+            app2 ~get_nseq_arg env s nseq_relocate
         | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_slice" } ->
-            app3 env s nseq_slice
+            app3 ~get_nseq_arg env s nseq_slice
         | _ -> `Not_found)
 end