diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 02c3bf0ba731783f6f9457dadedeed7b078a4c95..f6998ec99629420b9b6586ece3359beb0f8bd526 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -1,3 +1,4 @@
+open Colibri2_popop_lib
 open Nodes
 
 module All = struct
@@ -17,7 +18,7 @@ module All = struct
   type term = {
     app: Expr.Term.Const.t;
     tyargs : ty list;
-    args : Node.t list;
+    args : Node.t IArray.t;
     ty:ty
   }
 end
@@ -89,7 +90,7 @@ module Term = struct
     type t = All.term = {
       app: Expr.Term.Const.t;
       tyargs : Ty.t list;
-      args : Node.t list;
+      args : Node.t IArray.t;
       ty:Ty.t
     }[@@deriving hash, ord, eq ]
 
@@ -97,9 +98,14 @@ module Term = struct
       | [] -> ()
       | l -> Fmt.pf fmt "%a" Fmt.(paren (list ?sep pp)) l
 
+    let array_paren ?(sep=Fmt.nop) ~(paren:_ Fmt.t -> _ Fmt.t) pp fmt t =
+      if IArray.is_empty t then ()
+      else
+        Fmt.pf fmt "%a" (paren (IArray.pp ~sep pp)) t
+
     let pp fmt t =
       let infix sep =
-        Fmt.(list_paren ~sep:(fun fmt () -> Fmt.pf fmt "@ %s" sep) ~paren:parens Node.pp) fmt t.args
+        Fmt.(array_paren ~sep:(fun fmt () -> Fmt.pf fmt "@ %s" sep) ~paren:parens Node.pp) fmt t.args
       in
       match t.app.builtin with
       | Expr.Equal
@@ -117,7 +123,7 @@ module Term = struct
         Fmt.pf fmt "%a%a%a"
           Expr.Term.Const.pp t.app
           Fmt.(list_paren ~sep:comma ~paren:brackets Ty.pp) t.tyargs
-          Fmt.(list_paren ~sep:comma ~paren:parens Node.pp) t.args
+          Fmt.(array_paren ~sep:comma ~paren:parens Node.pp) t.args
   end
   include T
   include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
@@ -174,7 +180,7 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
     ThTerm.node @@ ThTerm.index @@
       { Term.app = f;
         tyargs = List.map (Ty.convert subst.ty) tyargs;
-        args = List.map (convert ~subst) args;
+        args = IArray.of_list_map ~f:(convert ~subst) args;
         ty = Ty.convert subst.ty t.ty;
       }
   | Expr.Binder (Exists(ty_vars,term_vars) as b, body)
@@ -231,7 +237,7 @@ module Defs = struct
         | exception Not_found -> ()
         | fundef ->
           let subst = {
-            Subst.term = Expr.Term.Var.M.of_list (List.combine fundef.tvl tvl);
+            Subst.term = Expr.Term.Var.M.of_list (Base.List.mapi ~f:(fun i v -> (v,IArray.get tvl i)) fundef.tvl);
             Subst.ty = Expr.Ty.Var.M.of_list (List.combine fundef.tyl tyl);
           } in
           let n = convert ~subst fundef.body in
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index 8321dac26b9c3a9418b23fefebb3fd229544e480..aa66b0730f6780af04b6c2982f4ad8632a082adf 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -1,3 +1,4 @@
+open Colibri2_popop_lib
 open Nodes
 
 module All: sig
@@ -9,7 +10,7 @@ module All: sig
   type term = {
     app: Expr.Term.Const.t;
     tyargs : ty list;
-    args : Node.t list;
+    args : Node.t IArray.t;
     ty:ty
   }
 
@@ -74,7 +75,7 @@ module Term: sig
   type t = All.term = {
     app: Expr.Term.Const.t;
     tyargs : Ty.t list;
-    args : Node.t list;
+    args : Node.t IArray.t;
     ty:Ty.t
   } [@@deriving hash, ord, eq ]
 
@@ -87,7 +88,7 @@ include RegisteredThTerm with type s := Term.t
 
 val convert : ?subst:Subst.t -> Expr.Term.t -> Node.t
 
-val apply : Expr.Term.Const.t -> Ty.t list -> Node.t list -> Term.t
+val apply : Expr.Term.Const.t -> Ty.t list -> Node.t IArray.t -> Term.t
 
 val init: Egraph.t -> unit
 
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 929fecfcf39f570480baa2c55dc4da10753e72e3..eca08223ad2e17d053c739dcf4dc99e0820c4cf1 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -201,7 +201,7 @@ let check_ground_terms d =
   Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
       if Option.is_none (Egraph.get_value d (Ground.node g)) then
         raise (GroundTermWithoutValueAfterModelFixing g);
-      List.iter (Ground.sem g).args ~f:(fun n ->
+      IArray.iter (Ground.sem g).args ~f:(fun n ->
           if Option.is_none (Egraph.get_value d n) then
             raise (ArgOfGroundTermWithoutValueAfterModelFixing (g, n)));
       if not (check d g) then (
@@ -237,14 +237,15 @@ let sequence_of_ground d =
   Datastructure.Queue.iter Data.reg_ground d ~f:(fun g ->
       let n = Egraph.find d (Ground.node g) in
       push n;
-      List.iter ~f:push (Ground.sem g).args;
+      IArray.iter ~f:push (Ground.sem g).args;
       Hashtbl.add_multi n2g ~key:n ~data:g);
   let partition =
     WTO.partition ?pref:None ~inits:(Queue.to_list inits) ~succs:(fun n ->
-        if Option.is_some (Egraph.get_value d n) then []
+        if Option.is_some (Egraph.get_value d n) then Sequence.empty
         else
           let gs = Hashtbl.find_multi n2g n in
-          List.concat_map gs ~f:(fun g -> (Ground.sem g).args))
+          Sequence.concat_map (Sequence.of_list gs) ~f:(fun g ->
+              IArray.to_seq (Ground.sem g).args))
   in
   Debug.dprintf2 debug "FixModel wto:%a" (Wto.pp_partition Node.pp) partition;
   Sequence.Generator.run (partition_to_seq partition)
@@ -340,8 +341,7 @@ module WatchArgs = struct
   module Daemon = struct
     type t = {
       callback : Egraph.t -> Ground.t -> unit;
-      ground : Ground.t;  (** perhaps ground should have an array for args *)
-      args : Node.t array;
+      ground : Ground.t;
       current : int Context.Ref.t;  (** already set before *)
     }
 
@@ -371,17 +371,18 @@ module WatchArgs = struct
     let delay = Events.FixingModel
 
     let rec check_if_set d args i =
-      if Option.is_none (Egraph.get_value d args.(i)) then Some i
+      if Option.is_none (Egraph.get_value d (IArray.get args i)) then Some i
       else
         let i = 1 + i in
-        if Array.length args <= i then None else check_if_set d args i
+        if IArray.length args <= i then None else check_if_set d args i
 
-    let attach d r i = Egraph.attach_any_value d r.args.(i) key r
+    let attach d r i =
+      Egraph.attach_any_value d (IArray.get (Ground.sem r.ground).args i) key r
 
     let run d r =
       let o_current = Context.Ref.get r.current in
-      assert (o_current < Array.length r.args);
-      (match check_if_set d r.args o_current with
+      assert (o_current < IArray.length (Ground.sem r.ground).args);
+      (match check_if_set d (Ground.sem r.ground).args o_current with
       | None -> r.callback d r.ground
       | Some current ->
           assert (current <> o_current);
@@ -389,23 +390,20 @@ module WatchArgs = struct
       None
 
     let create d callback ground =
-      match (Ground.sem ground).args with
-      | [] -> callback d ground
-      | _ -> (
-          let args = Array.of_list (Ground.sem ground).args in
-          let r current =
-            (* Debug.dprintf3 debug "Interp create %a (%i)" Ground.pp ground
-             *   current; *)
-            {
-              callback;
-              ground;
-              args;
-              current = Context.Ref.create (Egraph.context d) current;
-            }
-          in
-          match check_if_set d args 0 with
-          | None -> callback d ground
-          | Some current -> attach d (r current) current)
+      if IArray.is_empty (Ground.sem ground).args then callback d ground
+      else
+        let r current =
+          (* Debug.dprintf3 debug "Interp create %a (%i)" Ground.pp ground
+           *   current; *)
+          {
+            callback;
+            ground;
+            current = Context.Ref.create (Egraph.context d) current;
+          }
+        in
+        match check_if_set d (Ground.sem ground).args 0 with
+        | None -> callback d ground
+        | Some current -> attach d (r current) current
   end
 
   let () = Egraph.Wait.register_dem (module Daemon)
diff --git a/src_colibri2/popop_lib/IArray.ml b/src_colibri2/popop_lib/IArray.ml
index 8818468faff705f580c6ef03065216baa0edc04a..cf071ce33ef7b2ba0c1c05c7bcd9ef32d4e81229 100644
--- a/src_colibri2/popop_lib/IArray.ml
+++ b/src_colibri2/popop_lib/IArray.ml
@@ -20,16 +20,36 @@
 
 type 'a t = 'a array
 
+let is_empty = function [||] -> true | _ -> false
+let not_empty = function [||] -> false | _ -> true
+let empty = [||]
+
 let of_list = Array.of_list
+let of_list_map ~f = function
+  | [] -> empty
+  | h::l ->
+    let len = List.length l in
+    let a = Array.make (len + 1) (f h) in
+    let rec fill i = function
+      | [] -> ()
+      | hd::tl ->
+        Array.unsafe_set a i (f hd);
+        fill (i+1) tl
+    in
+    fill 1 l;
+    a
+
 let of_array = Array.copy
 let of_iter l (iter : ('a -> unit) -> unit) =
-  if l = 0 then [||] else
+  if l = 0 then empty else
     let res = Array.make l (Obj.magic 0 : 'a) in
     let r = ref 0 in
     iter (fun v -> res.(!r) <- v; incr r);
     assert (!r == l);
     res
 
+let to_list = Array.to_list
+let to_seq = Base.Array.to_sequence
 
 
 let length = Array.length
@@ -96,15 +116,79 @@ let hash_fold_t h s t =
 
 let get = Array.get
 
-let iter = Array.iter
-let iteri = Array.iteri
-let fold = Array.fold_left
+let iter ~f a = Array.iter f a
+let iteri ~f a = Array.iteri f a
+let fold ~f ~init a = Array.fold_left f init a
 
-let foldi f x a =
+let foldi a ~init:x ~f =
   let r = ref x in
   for i = 0 to Array.length a - 1 do
     r := f i !r (Array.unsafe_get a i)
   done;
   !r
 
-let pp sep p fmt a = Pp.iter1 iter sep p fmt a
+let foldi_non_empty_exn ~init ~f a =
+  if Array.length a = 0 then invalid_arg "IArray.fold_non_empty_exn: empty array";
+  let r = ref (init (Array.unsafe_get a 0)) in
+  for i = 1 to Array.length a - 1 do
+    r := f i !r (Array.unsafe_get a i)
+  done;
+  !r
+
+let fold2_exn ~init ~f a1 a2 =
+  if Array.length a1 <> Array.length a2 then invalid_arg "IArray.fold2_exn: different length";
+  let r = ref init in
+  for i = 0 to Array.length a1 - 1 do
+    r := f !r a1.(i) a2.(i)
+  done;
+  !r
+
+let for_alli ~f a1 =
+  let exception False in
+  try
+    for i = 0 to Array.length a1 - 1 do
+      if not (f i a1.(i)) then raise False
+    done;
+    true
+  with False -> false
+
+let for_alli_non_empty_exn ~init ~f a =
+  if Array.length a = 0 then invalid_arg "IArray.for_alli_non_empty_exn: empty array";
+  let first = init a.(0) in
+  let exception False in
+  try
+    for i = 1 to Array.length a - 1 do
+      if not (f i first a.(i)) then raise False
+    done;
+    true
+  with False -> false
+
+let for_all2_exn ~f a1 a2 =
+  if Array.length a1 <> Array.length a2 then invalid_arg "IArray.fold2_exn: different length";
+  let exception False in
+  try
+    for i = 0 to Array.length a1 - 1 do
+      if not (f a1.(i) a2.(i)) then raise False
+    done;
+    true
+  with False -> false
+
+let map ~f a = Array.map f a
+
+let pp ?(sep=Fmt.comma) p fmt a = Pp.iter1 (fun f e -> iter ~f e) sep p fmt a
+
+let extract1_exn = function
+  | [| a |] -> a
+  | _ -> invalid_arg "IArray not of size 1"
+
+let extract2_exn = function
+  | [| a; b |] -> (a,b)
+  | _ -> invalid_arg "IArray not of size 2"
+
+let extract3_exn = function
+  | [| a; b; c |] -> (a,b,c)
+  | _ -> invalid_arg "IArray not of size 3"
+
+let extract4_exn = function
+  | [| a; b; c; d |] -> (a,b,c,d)
+  | _ -> invalid_arg "IArray not of size 4"
diff --git a/src_colibri2/popop_lib/IArray.mli b/src_colibri2/popop_lib/IArray.mli
index 319b6a31c68d222a3f9c0fadea9b99af73d18323..bb21e7d189444a498a9cf53218143a7fa9623873 100644
--- a/src_colibri2/popop_lib/IArray.mli
+++ b/src_colibri2/popop_lib/IArray.mli
@@ -25,11 +25,15 @@
 type 'a t
 
 val of_list: 'a list -> 'a t
+val of_list_map: f:('a -> 'b) -> 'a list -> 'b t
 val of_array: 'a array -> 'a t
 val of_iter: int -> (('a -> unit) -> unit) -> 'a t
 (** create the array using an iterator. The integer indicate the
     number of iteration that will occur *)
 
+val empty: 'a t
+val is_empty: 'a t -> bool
+val not_empty: 'a t -> bool
 val length: 'a t -> int
 
 val compare: ('a -> 'a ->  int)  -> 'a t -> 'a t -> int
@@ -41,9 +45,25 @@ val hash   : ('a -> int) -> 'a t -> int
 val hash_fold_t   : 'a Base.Hash.folder -> 'a t Base.Hash.folder
 
 
-val iter : ('a -> unit)  -> 'a t -> unit
-val iteri : (int -> 'a -> unit)  -> 'a t -> unit
-val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
-val foldi : (int -> 'b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+val iter : f:('a -> unit)  -> 'a t -> unit
+val iteri : f:(int -> 'a -> unit)  -> 'a t -> unit
+val fold : f:('b -> 'a -> 'b) -> init:'b -> 'a t -> 'b
+val foldi : 'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b) -> 'b
+val foldi_non_empty_exn : init:('a -> 'b) -> f:(int -> 'b -> 'a -> 'b) -> 'a t -> 'b
+(** The accumulator is obtained with the first elements *)
 
-val pp: unit Pp.pp -> 'a Pp.pp -> 'a t Pp.pp
+val fold2_exn : init:'acc -> f:('acc -> 'a -> 'b -> 'acc) -> 'a t -> 'b t -> 'acc
+val for_alli : f:(int -> 'a -> bool) -> 'a t -> bool
+val for_all2_exn : f:('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+val for_alli_non_empty_exn : init:('a -> 'acc) -> f:(int -> 'acc -> 'a -> bool) -> 'a t -> bool
+val map: f:('a -> 'b) -> 'a t -> 'b t
+
+val pp: ?sep:unit Pp.pp -> 'a Pp.pp -> 'a t Pp.pp
+
+val extract1_exn: 'a t -> 'a
+val extract2_exn: 'a t -> 'a * 'a
+val extract3_exn: 'a t -> 'a * 'a * 'a
+val extract4_exn: 'a t -> 'a * 'a * 'a * 'a
+
+val to_list: 'a t -> 'a list
+val to_seq: 'a t -> 'a Base.Sequence.t
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
index a53a7bd6cecd10bf4aacb4d88ad2a19d549de02d..f7a4d3d58a8896bac14b34227d46b43c254393e4 100644
--- a/src_colibri2/stdlib/wto.ml
+++ b/src_colibri2/stdlib/wto.ml
@@ -139,7 +139,7 @@ module Make(N:sig
                             numbering.  Note that we replaced the DFN=0
                             test by presence in the Hashtable. *)
       mutable num: level;          (* Number of visited nodes. *)
-      succs: N.t -> (N.t list);    (* Successors transition. *)
+      succs: N.t -> (N.t Base.Sequence.t);    (* Successors transition. *)
       stack: N.t Stack.t
     }
 
@@ -169,11 +169,11 @@ module Make(N:sig
       DFN.replace state.dfn vertex (Parent n);
       (* Visit all its successors *)
       let succs = state.succs vertex in
-      let (loop,partition) = List.fold_left (fun (loop,partition) succ ->
+      let (loop,partition) = Base.Sequence.fold ~f:(fun (loop,partition) succ ->
           let (loop',partition) = visit ~pref state succ partition in
           let loop = min_loop loop loop' in
           (loop,partition)
-        ) (NoLoop,partition) succs
+        ) ~init:(NoLoop,partition) succs
       in
       match loop with
       (* We are not in a loop. Add the vertex to the partition *)
@@ -209,13 +209,13 @@ module Make(N:sig
         (* Makes [vertex] invisible in the subsequents visits. *)
         DFN.replace state.dfn vertex Invisible;
         (* Restart the component analysis *)
-        let component = List.fold_left
-            (fun component succ ->
+        let component = Base.Sequence.fold
+            ~f:(fun component succ ->
                let (loop,component) = visit ~pref state succ component in
                (* Since we reset the component we should have no loop *)
                assert (is_no_loop loop);
                component
-            ) [] succs
+            ) ~init:[] succs
         in
         (NoLoop,Component(vertex,component)::partition)
       | _ ->
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
index d09bd5a537687ced45cdfda8d37a5e7463eb0f05..a4226b3b926b18f9f1510658c4a0b42bb713adfb 100644
--- a/src_colibri2/stdlib/wto.mli
+++ b/src_colibri2/stdlib/wto.mli
@@ -60,7 +60,9 @@ module Make(Node:sig
 
   (** Implements Bourdoncle "Efficient chaotic iteration strategies with
   widenings" algorithm to compute a WTO. *)
-  val partition: ?pref:pref -> inits:Node.t list -> succs:(Node.t -> Node.t list) -> Node.t partition
+  val partition: ?pref:pref -> inits:Node.t list ->
+    succs:(Node.t -> Node.t Base.Sequence.t) ->
+    Node.t partition
 
   val equal_component: Node.t component -> Node.t component -> bool
   val equal_partition: Node.t partition -> Node.t partition -> bool
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index c00d1838eb33e5b5fb9bb7ec2eab2ff9b4cc06ee..e8b62ee4055d68c711bb292358b4656e1d83a736 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -160,7 +160,8 @@ let converter d (f : Ground.t) =
   let reg n = Egraph.register d n in
   let open Monad in
   match Ground.sem f with
-  | { app = { builtin = Expr.Tester { adt; case; _ }; _ }; args = [ e ]; _ } ->
+  | { app = { builtin = Expr.Tester { adt; case; _ }; _ }; args; _ } ->
+      let e = IArray.extract1_exn args in
       reg e;
       wait.for_value d Boolean.BoolValue.key r
         (set e
@@ -177,18 +178,16 @@ let converter d (f : Ground.t) =
             | One { case = case'; _ } -> Some (Case.equal case case')));
       Adt_value.propagate_value d f
   | { app = { builtin = Expr.Constructor { case; _ }; _ }; args; _ } ->
-      List.iter reg args;
+      IArray.iter ~f:reg args;
       let fields =
-        Base.List.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
+        IArray.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
             Field.M.add field a acc)
       in
       upd_dom d r (One { case; fields });
       Adt_value.propagate_value d f
-  | {
-   app = { builtin = Expr.Destructor { case; field; adt; _ }; _ };
-   args = [ e ];
-   _;
-  } ->
+  | { app = { builtin = Expr.Destructor { case; field; adt; _ }; _ }; args; _ }
+    ->
+      let e = IArray.extract1_exn args in
       reg e;
       Egraph.register_decision d (Decide.new_decision e adt case);
       let upd d =
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index e00920dfd28727fa7a78ab8dee9056964bef0c10..eb1c0974e58a6de1363353ce95801588004260d6 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -43,7 +43,8 @@ let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
 let compute d g =
   match Ground.sem g with
-  | { app = { builtin = Expr.Tester { case; _ }; _ }; args = [ e ]; _ } ->
+  | { app = { builtin = Expr.Tester { case; _ }; _ }; args; _ } ->
+      let e = IArray.extract1_exn args in
       let v = coerce_nodevalue (interp d e) in
       let v = value v in
       `Some
@@ -55,16 +56,13 @@ let compute d g =
    _;
   } ->
       let fields =
-        Base.List.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
+        IArray.foldi ~init:Field.M.empty args ~f:(fun field acc a ->
             Field.M.add field (interp d a) acc)
       in
       let v = { tyargs; adt; case; fields } in
       `Some (nodevalue (index v))
-  | {
-   app = { builtin = Expr.Destructor { case; field; _ }; _ };
-   args = [ e ];
-   _;
-  } ->
+  | { app = { builtin = Expr.Destructor { case; field; _ }; _ }; args; _ } ->
+      let e = IArray.extract1_exn args in
       let v = coerce_nodevalue (interp d e) in
       let v = value v in
       if Case.equal case v.case then
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index cbb5f1848077d1475a103e73f67f836eb78d7b19..b362031ac2d2427a188ec0aee5440b3f3359178a 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -228,7 +228,8 @@ let converter d (f:Ground.t) =
   | { app = {builtin = Dolmen_std.Expr.Base; _ }; tyargs = _; args = _; ty }
     when Ground.Ty.equal ty Ground.Ty.int ->
     upd_dom d r D.integers
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let (a,b) = IArray.extract2_exn args in
     reg a; reg b;
     let wakeup =
       set r (let+ va = get a and+ vb = get b in D.add va vb) &&
@@ -236,7 +237,8 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in D.minus vr va)
     in
     List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b;r]
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let (a,b) = IArray.extract2_exn args in
     reg a; reg b;
     let wakeup =
       set r (let+ va = get a and+ vb = get b in D.minus va vb) &&
@@ -244,20 +246,25 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in D.minus va vr)
     in
     List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b;r]
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a;
     let wakeup =
       set r (let+ va = get a in D.mult_cst Q.minus_one va) &&
       set a (let+ vr = get r in D.mult_cst Q.minus_one vr)
     in
     List.iter (fun n -> wait.for_dom d dom n wakeup) [a;r]
-  | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false) `Lt a b
-  | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some true | Gt -> Some false) `Le a b
-  | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Le -> None | Lt -> Some false  | Ge | Gt -> Some true) `Ge a b
-  | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some false  | Gt -> Some true) `Gt a b
   | _ -> ()
 
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index ca059d1598ea2e451b02f4f9bee1e51957b01042..55052ceef36ff1b5566fcf560817dbe1a1acfd72 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -192,13 +192,16 @@ let converter d (f:Ground.t) =
     let res = Ground.node f in
   let reg n = Egraph.register d n in
   match Ground.sem f with
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.one;b,Q.one])
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.one;b,Q.minus_one])
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a;
     assume_poly_equality d res (Polynome.of_list Q.zero [a,Q.minus_one])
   | _ -> ()
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index e162fde0304ae5eb0b86d5e3b549cd584d4e94d2..5907e5f0eb6c24d8ae6eccb5be051c2381cead1b 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -359,20 +359,24 @@ let converter d (f:Ground.t) =
   let res = Ground.node f in
   let reg n = Egraph.register d n in
   match Ground.sem f with
-  | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     assume_poly_equality d res (Product.of_list [a,Q.one;b,Q.one])
-  | { app = {builtin = Expr.Div}; tyargs = []; args = [num;den]; _ } ->
+  | { app = {builtin = Expr.Div}; tyargs = []; args; _ } ->
+    let num,den = IArray.extract2_exn args in
     reg num; reg den;
     wait.for_dom d Dom_interval.dom den
       (fun d _ ->
          if Dom_interval.is_not_zero d den then
            assume_poly_equality d num (Product.of_list [res,Q.one;den,Q.one])
       )
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     List.iter (fun x -> wait.for_dom d dom x (factorize res a Q.one b)) [a;b]
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg a; reg b;
     List.iter (fun x -> wait.for_dom d dom x (factorize res a Q.minus_one b)) [a;b]
   | _ -> ()
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 9549bce8f25d7c3645c94572ee91e888be47cbea..23aad9c4b967f78ffbfd4ed8dc850f8297f65edd 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -102,13 +102,17 @@ let make_equations d (eqs,vars) g =
   | Some truth ->
     let p,bound,p_non_norm =
       match Ground.sem g with
-      | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Strict truth a b
-      | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Large truth a b
-      | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Large truth b a
-      | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+      | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
         mk_eq d Strict truth b a
       | _ -> assert false
     in
@@ -205,7 +209,7 @@ let converter d (f:Ground.t) =
       Egraph.attach_dom d n Dom_polynome.dom Daemon.key ();
       Egraph.attach_node d n Daemon.key ();
     in
-    List.iter attach args;
+    IArray.iter ~f:attach args;
     Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key ();
     Datastructure.Queue.push comparisons d f;
     Egraph.register_delayed_event d Daemon.key ()
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index 2daa4f5bcce43ffb06e1fdc88f491f96a43d0cfd..50d80ce3532ac65d55263a8106cbe8a8b91003ad 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -9,7 +9,8 @@ let init,attach =
 let converter d (f:Ground.t) =
   let res = Ground.node f in
   match Ground.sem f with
-  | { app = {builtin = Expr.Mul}; tyargs = []; args = [arg1;arg2]; _ } -> begin
+  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } -> begin
+      let arg1,arg2 = Colibri2_popop_lib.IArray.extract2_exn args in
       Egraph.register d arg1; Egraph.register d arg2;
       attach d arg1 (res,arg2);
       attach d arg2 (res,arg1)
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 32e1544694d7842ee8ae69d5e882bac6c09df2c1..a99103e3dbfcca6cbad9080aaf090fe9c6f86f82 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -133,34 +133,48 @@ module Check = struct
             ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
             | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
             );
-          args = [a] } ->
+          args } ->
+        let a = IArray.extract1_exn args in
         !< (!> a)
-      | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Integer s}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         !< (Q.of_string s)
-      | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Decimal s}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         !< (Q.of_string_decimal s)
-      | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Rational s}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         !< (Q.of_string_decimal s)
-      | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Add}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Q.add !>a !>b)
-      | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Sub}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Q.sub !>a !>b)
-      | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; ty = _ } ->
+      | { app = {builtin = Expr.Minus}; tyargs = []; args; ty = _ } ->
+        let a = IArray.extract1_exn args in
         !< (Q.neg !>a)
-      | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Mul}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Q.mul !>a !>b)
-      | { app = {builtin = Expr.Div}; tyargs = []; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Div}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         if Q.is_zero !>b then `Uninterp
         else !< (Q.div !>a !>b)
-      | { app = {builtin = Expr.Lt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.lt !>arg1 !>arg2)
-      | { app = {builtin = Expr.Leq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.leq !>arg1 !>arg2)
-      | { app = {builtin = Expr.Gt}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.gt !>arg1 !>arg2)
-      | { app = {builtin = Expr.Geq}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !<< (Q.geq !>arg1 !>arg2)
-      | { app = {builtin = Expr.Floor}; tyargs = []; args = [a]; _ } ->
+      | { app = {builtin = Expr.Lt}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.lt !>a !>b)
+      | { app = {builtin = Expr.Leq}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.leq !>a !>b)
+      | { app = {builtin = Expr.Gt}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.gt !>a !>b)
+      | { app = {builtin = Expr.Geq}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !<< (Q.geq !>a !>b)
+      | { app = {builtin = Expr.Floor}; tyargs = []; args; _ } ->
+        let a = IArray.extract1_exn args in
         !< (Q.floor (!> a))
       | _ -> `None
 
@@ -204,15 +218,20 @@ let converter d (f:Ground.t) =
         ( [{app={builtin = (Expr.Int|Expr.Rat);_};_};{app={builtin = Expr.Real;_};_}]
         | [{app={builtin = Expr.Int;_};_};{app={builtin = Expr.Rat;_};_}]
         );
-      args = [a] } ->
+      args } ->
+    let a = IArray.extract1_exn args in
     merge a; Check.attach d f
-  | { app = {builtin = Expr.Integer s}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.Integer s}; tyargs = []; args; _ } ->
+    assert ( IArray.is_empty args);
     merge (cst (Q.of_string s))
-  | { app = {builtin = Expr.Decimal s}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.Decimal s}; tyargs = []; args; _ } ->
+assert ( IArray.is_empty args);
     merge (cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Rational s}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.Rational s}; tyargs = []; args; _ } ->
+assert ( IArray.is_empty args);
     merge (cst (Q.of_string_decimal s))
-  | { app = {builtin = Expr.Add}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+let a,b = IArray.extract2_exn args in
     reg a; reg b; Check.attach d f;
     let wait =
       set r (let+ va = get a and+ vb = get b in Q.add va vb) &&
@@ -220,7 +239,8 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in Q.sub vr va)
     in
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
-  | { app = {builtin = Expr.Sub}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+let a,b = IArray.extract2_exn args in
     reg a; reg b; Check.attach d f;
     let wait =
       set r (let+ va = get a and+ vb = get b in Q.sub va vb) &&
@@ -228,30 +248,37 @@ let converter d (f:Ground.t) =
       set b (let+ va = get a and+ vr = get r in Q.sub va vr)
     in
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
-  | { app = {builtin = Expr.Mul}; tyargs = []; args = [a;b]; _ } ->
-    reg a; reg b; Check.attach d f;
-    let wait =
-      set r (let+ va = get a and+ vb = get b in Q.mul va vb) &&
-      set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.div vr vb)) &&
-      set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
-    in
-    List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
-  | { app = {builtin = Expr.Minus}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Mul}; tyargs = []; args; _ } ->
+  let a,b = IArray.extract2_exn args in
+  reg a; reg b; Check.attach d f;
+  let wait =
+    set r (let+ va = get a and+ vb = get b in Q.mul va vb) &&
+    set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.div vr vb)) &&
+    set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
+  in
+  List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
+  | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a; Check.attach d f;
     let wait =
       set r (let+ va = get a in Q.neg va) &&
       set a (let+ vr = get r in Q.neg vr)
     in
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;r]
-  | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.lt a b; Check.attach d f;
-  | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.le a b; Check.attach d f;
-  | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.gt a b; Check.attach d f;
-  | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     cmp Q.ge a b; Check.attach d f;
-  | { app = {builtin = Expr.Floor}; tyargs = []; args = [a]; _ } ->
+  | { app = {builtin = Expr.Floor}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
     reg a; Check.attach d f;
   | _ -> ()
 
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 89fd485417fd2fb4bea3c7b2276af896d7c40ba8..7278dc23785d5fb30e5ca2bad164a7b1e7b3aaa8 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -98,7 +98,7 @@ module T = struct
       print_cl fmt node true
     | None ->
       let print_cl topnot fmt (node,b) = print_cl fmt node (mulbool topnot b) in
-      let aux b fmt' m = IArray.fold (fun sofar e -> e::sofar) [] m
+      let aux b fmt' m = IArray.fold ~f:(fun sofar e -> e::sofar) ~init:[] m
                         |> List.rev
                         |> Fmt.(list ~sep:(const char ',') (print_cl b) fmt')
       in
@@ -112,7 +112,7 @@ let sem = ThTermKind.create_key (module struct type t = T.t let name = "Prop" en
 
 (* let iter f x = IArray.iter f x.lits *)
 
-let fold f acc x = IArray.fold f acc x.T.lits
+let fold f acc x = IArray.fold ~f ~init:acc x.T.lits
 
 let find x n =
   fold (fun acc (n1,b) -> if Node.equal n1 n then Some b else acc) None x
@@ -130,7 +130,7 @@ module Th = struct
 
   exception Found of Node.t * bool
   let find_not_known d l =
-    IArray.iter (fun (node,b) ->
+    IArray.iter ~f:(fun (node,b) ->
       match Egraph.get_value d node with
       | Some _ -> ()
       | None -> raise (Found (node,b))
@@ -138,13 +138,13 @@ module Th = struct
 
   let _bcp d l absorbent =
     try
-      let res = IArray.fold (fun acc node ->
+      let res = IArray.fold ~f:(fun acc node ->
         match is d node, acc with
         | Some b, _ when Bool.equal b absorbent -> raise (TopKnown absorbent)
         | Some _, _ -> acc
         | None, Some _ -> raise Exit
         | None, None -> Some node)
-        None l in
+        ~init:None l in
       match res with
       | None -> raise (TopKnown (not absorbent))
       | _ -> res
@@ -285,7 +285,7 @@ module DaemonPropa = struct
     (** \/ c1 c2 = false ==> c1 = false /\ c2 = false *)
     | Some b when not (mulbool v.topnot b) ->
       let set_dom_down_false (node,sign) = set_bool d node sign in
-      IArray.iter set_dom_down_false v.lits;
+      IArray.iter ~f:set_dom_down_false v.lits;
       false
     | Some _ -> true
     end
@@ -331,7 +331,7 @@ module DaemonInit = struct
             DaemonPropaNot.init d thterm node
           | None ->
             assert (not lazy_propagation);
-            IArray.iter (fun (node,_) -> Egraph.register d node) v.lits;
+            IArray.iter ~f:(fun (node,_) -> Egraph.register d node) v.lits;
             if DaemonPropa.init d thterm then ()
         (** we could register a decision here, if we want to do
             decision on any boolean operations not only variable *)
@@ -423,7 +423,7 @@ let chobool n = {
 
 let converter d (f:Ground.t) =
   let res = Ground.node f in
-  let reg_args args = List.iter (Egraph.register d) args in
+  let reg_args args = IArray.iter ~f:(Egraph.register d) args in
   let reg n =
     Egraph.register d n;
     Egraph.merge d res n
@@ -433,16 +433,20 @@ let converter d (f:Ground.t) =
     when Ground.Ty.equal ty Ground.Ty.bool  ->
     Egraph.register_decision d (chobool res)
   | { app = {builtin = Expr.Or}; tyargs = []; args; _ } ->
-    reg_args args; reg (_or args)
+    reg_args args; reg (_or (IArray.to_list args))
   | { app = {builtin = Expr.And}; tyargs = []; args; _ } ->
-    reg_args args; reg (_and args)
-  | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2] as args; _ } ->
-    reg_args args; reg (gen false [arg1,true;arg2,false])
-  | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg] as args; _ } ->
-    reg_args args; reg (_not arg)
-  | { app = {builtin = Expr.True}; tyargs = []; args = []; _ } ->
+    reg_args args; reg (_and (IArray.to_list args))
+  | { app = {builtin = Expr.Imply}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
+    reg_args args; reg (gen false [a,true;b,false])
+  | { app = {builtin = Expr.Neg}; tyargs = []; args; _ } ->
+    let a = IArray.extract1_exn args in
+    reg_args args; reg (_not a)
+  | { app = {builtin = Expr.True}; tyargs = []; args; _ } ->
+    assert ( IArray.is_empty args);
     reg _true
-  | { app = {builtin = Expr.False}; tyargs = []; args = []; _ } ->
+  | { app = {builtin = Expr.False}; tyargs = []; args; _ } ->
+    assert ( IArray.is_empty args);
     reg _false
   | _ -> ()
 
@@ -459,19 +463,24 @@ let init_check d =
         check r
       in
       match Ground.sem t with
-      | { app = {builtin = Expr.Or}; tyargs = []; args = args; ty = _ } ->
-        !< (List.fold_left (||) false (List.map (!>) args))
-      | { app = {builtin = Expr.And}; tyargs = []; args = args; ty = _ } ->
-        !< (List.fold_left (&&) true (List.map (!>) args))
-      | { app = {builtin = Expr.Imply}; tyargs = []; args = [arg1;arg2]; ty = _ } ->
-        !< ( not (!> arg1) || !> arg2 )
-      | { app = {builtin = Expr.Xor}; tyargs = []; args = [arg1;arg2]; _ } ->
-        !< ( not (Bool.equal (!> arg1) (!> arg2) ))
-      | { app = {builtin = Expr.Neg}; tyargs = []; args = [arg]; ty = _ } ->
-        !< (not (!> arg))
-      | { app = {builtin = Expr.True}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.Or}; tyargs = []; args; ty = _ } ->
+        !< (IArray.fold ~f:(||) ~init:false (IArray.map ~f:(!>) args))
+      | { app = {builtin = Expr.And}; tyargs = []; args; ty = _ } ->
+        !< (IArray.fold ~f:(&&) ~init:true (IArray.map ~f:(!>) args))
+      | { app = {builtin = Expr.Imply}; tyargs = []; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
+        !< ( not (!> a) || !> b )
+      | { app = {builtin = Expr.Xor}; tyargs = []; args; _ } ->
+        let a,b = IArray.extract2_exn args in
+        !< ( not (Bool.equal (!> a) (!> b) ))
+      | { app = {builtin = Expr.Neg}; tyargs = []; args; ty = _ } ->
+        let a = IArray.extract1_exn args in
+        !< (not (!> a))
+      | { app = {builtin = Expr.True}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         check values_true
-      | { app = {builtin = Expr.False}; tyargs = []; args = []; ty = _ } ->
+      | { app = {builtin = Expr.False}; tyargs = []; args; ty = _ } ->
+        assert ( IArray.is_empty args);
         check values_false
       | _ -> None
     )
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 29bef0af8486fe492dc1207670cffa304078b935..b0234ea78d25d869cbfbb0ee016579919fe5ff4e 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -578,21 +578,23 @@ let init_check d =
         check r
       in
       match Ground.sem t with
-      | { app = {builtin = Expr.Equal}; tyargs = [_]; args = a::l; ty = _ } ->
-        let a = interp a in
-        !< (List.for_all (fun t -> Value.equal a (interp t)) l)
-      | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Equal}; tyargs = [_]; args; ty = _ } ->
+        assert (IArray.not_empty args);
+        !< (IArray.for_alli_non_empty_exn ~init:interp ~f:(fun _ a t -> Value.equal a (interp t)) args)
+      | { app = {builtin = Expr.Equiv}; tyargs = [_]; args; ty = _ } ->
+        let a,b = IArray.extract2_exn args in
         !< (Value.equal (interp a) (interp b))
-      | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; ty = _ } ->
+      | { app = {builtin = Expr.Distinct}; tyargs = [_]; args; ty = _ } ->
         begin
           try
             let fold acc v = Value.S.add_new Exit (interp v) acc in
-            let _ = List.fold_left fold Value.S.empty args in
+            let _ = IArray.fold ~f:fold ~init:Value.S.empty args in
             check Boolean.values_true
           with Exit ->
             check Boolean.values_false
         end
-      | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; ty = _ } ->
+      | { app = {builtin = Expr.Ite}; tyargs = [_]; args; ty = _ } ->
+        let c,a,b = IArray.extract3_exn args in
         check (if (!> c) then interp a else interp b)
       | _ -> None
     )
@@ -610,14 +612,17 @@ let converter d (t:Ground.t) =
   in
   match Ground.sem t with
   | { app = {builtin = Expr.Equal}; tyargs = [_]; args = l; _ } ->
-    reg (equality (List.map of_term l))
-  | { app = {builtin = Expr.Equiv}; tyargs = [_]; args = [a;b]; _ } ->
+    reg (equality (List.map of_term (IArray.to_list l)))
+  | { app = {builtin = Expr.Equiv}; tyargs = [_]; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg (equality [of_term a;of_term b])
-  | { app = {builtin = Expr.Distinct}; tyargs = [_]; args = args; _ } ->
-    reg (disequality (List.map of_term args))
-  | { app = {builtin = Expr.Ite}; tyargs = [_]; args = [c;a;b]; _ } ->
+  | { app = {builtin = Expr.Distinct}; tyargs = [_]; args; _ } ->
+    reg (disequality (List.map of_term (IArray.to_list args)))
+  | { app = {builtin = Expr.Ite}; tyargs = [_]; args; _ } ->
+    let c,a,b = IArray.extract3_exn args in
     reg (ite (of_term c) (of_term a) (of_term b))
-  | { app = {builtin = Expr.Xor}; tyargs = []; args = [a;b]; _ } ->
+  | { app = {builtin = Expr.Xor}; tyargs = []; args; _ } ->
+    let a,b = IArray.extract2_exn args in
     reg (disequality ([of_term a;of_term b]))
   | _ -> ()
 
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index daa271b5373d057cc9502f1814e53612d3909c75..61c29b4c0cfbb75fe92fc644734344cb0134c3db 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -13,7 +13,7 @@ type t' = {
   triggers : Trigger.t list;
   ups :
     (Expr.Ty.t list
-    * Pattern.t list
+    * Pattern.t IArray.t
     * int (* from which argument we come *)
     * t)
     list
@@ -56,8 +56,7 @@ let rec exec d acc substs n ip =
           if Ground.Subst.S.is_empty substs then substs
           else
             let i = ref (-1) in
-            Base.List.fold2_exn args pargs ~init:substs
-              ~f:(fun substs args parg ->
+            IArray.fold2_exn args pargs ~init:substs ~f:(fun substs args parg ->
                 incr i;
                 if Int.equal !i pos then substs
                 else Pattern.match_term d substs args parg)
@@ -155,13 +154,13 @@ let insert_pattern d (trigger : Trigger.t) =
         let ips = [ ip ] in
         ips
   and insert_children pp_vars f tytl tl =
-    List.foldi
-      (fun acc pos p ->
+    IArray.foldi
+      ~f:(fun pos acc p ->
         let f_pos = F_Pos.{ f; pos } in
         let ips = aux f_pos pp_vars p in
         let ips = List.map (add_up f_pos tytl tl) ips in
         ips @ acc)
-      [] tl
+      ~init:[] tl
   in
   let pp_vars = Pattern.get_pps trigger.pat in
   match trigger.pat with
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index 2f566d44bbb701123bbea8b52a32efcb55bb912d..df42bb012d5d6047d81ffcea5544d31acc4146d4 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -1,3 +1,4 @@
+open Colibri2_popop_lib
 (** information added on nodes *)
 
 type t = {
@@ -22,7 +23,10 @@ let congruence_closure d ~other parent0 ~repr parent1 =
       let h = Ground.Term.H.create 10 in
       let norm g =
         let g = Ground.sem g in
-        { g with Ground.Term.args = List.map find_as_if g.Ground.Term.args }
+        {
+          g with
+          Ground.Term.args = IArray.map ~f:find_as_if g.Ground.Term.args;
+        }
       in
       let s = ref (Ground.S.union g1 g2) in
       let not_first g = s := Ground.S.remove g !s in
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index c389e73115d2d7e7f61ec9cae47637f01fd33921..26af230dfaba9d4a79cc8cd93e8a02dc4a1e9bda 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -8,7 +8,7 @@ module T = struct
 
   type t =
     | Var of Expr.Term.Var.t
-    | App of F.t * Expr.Ty.t list * t list
+    | App of F.t * Expr.Ty.t list * t IArray.t
     | Node of Node.t
   [@@deriving eq, ord, hash]
 
@@ -18,7 +18,7 @@ module T = struct
         Fmt.pf fmt "%a[%a](%a)" F.pp f
           Fmt.(list ~sep:comma Expr.Ty.pp)
           tyl
-          Fmt.(list ~sep:comma pp)
+          Fmt.(IArray.pp ~sep:comma pp)
           tl
     | Node n -> Node.pp fmt n
 end
@@ -35,7 +35,7 @@ let rec of_term ~subst (t : Expr.Term.t) =
   | App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term ~subst a
   | App (f, tys, tl) ->
       (* todo type substitution *)
-      App (f, tys, List.map (of_term ~subst) tl)
+      App (f, tys, IArray.of_list_map ~f:(of_term ~subst) tl)
   | _ -> (* absurd *) assert false
 
 let init = Ground.Subst.S.singleton Ground.Subst.empty
@@ -101,7 +101,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
             if Ground.Subst.S.is_empty substs then acc
             else
               let substs =
-                Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
+                IArray.fold2_exn args pargs ~init:substs ~f:(match_term d)
               in
               Ground.Subst.S.union substs acc)
           Ground.Subst.S.empty s
@@ -139,7 +139,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
           let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
           assert (Term.Const.equal f pf);
           List.for_all2 (check_ty subst) tyl ptyl
-          && List.for_all2 (check_term d subst) args pargs)
+          && IArray.for_all2_exn ~f:(check_term d subst) args pargs)
         s
   | Node n' -> Egraph.is_equal d n n'
 
@@ -158,14 +158,16 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
               (Ground.tys d n)
           then Node.S.singleton (Egraph.find_def d n)
           else raise Not_found)
-  | App (pf, ptyl, []) ->
+  | App (pf, ptyl, pargs) when IArray.is_empty pargs ->
       let g =
-        Ground.apply pf (List.map (Ground.Ty.convert subst.ty) ptyl) []
+        Ground.apply pf
+          (List.map (Ground.Ty.convert subst.ty) ptyl)
+          IArray.empty
         |> Ground.index |> Ground.node
       in
       if Egraph.is_registered d g then Node.S.singleton (Egraph.find d g)
       else raise Not_found
-  | App (pf, ptyl, parg :: pargs) ->
+  | App (pf, ptyl, pargs) ->
       let find_app pos n =
         Opt.get_def Ground.S.empty
         @@
@@ -189,9 +191,9 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
         nodes
       in
       let nodes =
-        Lists.fold_lefti
-          (fun acc i parg -> Node.S.inter acc (get_parents (i + 1) parg))
-          (get_parents 0 parg) pargs
+        IArray.foldi_non_empty_exn
+          ~f:(fun i acc parg -> Node.S.inter acc (get_parents (i + 1) parg))
+          ~init:(get_parents 0) pargs
       in
       if Node.S.is_empty nodes then raise Not_found else nodes
   | Node n -> Node.S.singleton n
@@ -204,16 +206,18 @@ let get_pps pattern =
     match p with
     | Var v -> Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
     | App (f, _, tl) ->
-        List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
+        IArray.foldi
+          ~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
+          ~init:acc tl
     | Node _ -> acc
   in
   let m =
     match pattern with
     | Var _ | Node _ -> Expr.Term.Var.M.empty
     | App (f, _, tl) ->
-        List.foldi
-          (fun acc pos p -> aux acc F_Pos.{ f; pos } p)
-          Expr.Term.Var.M.empty tl
+        IArray.foldi
+          ~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
+          ~init:Expr.Term.Var.M.empty tl
   in
   Expr.Term.Var.M.map
     (fun s ->
@@ -261,7 +265,7 @@ let match_any_term d (p : t) : Ground.Subst.S.t =
           assert (Term.Const.equal f pf);
           let substs = List.fold_left2 match_ty init tyl ptyl in
           let substs =
-            Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
+            IArray.fold2_exn args pargs ~init:substs ~f:(match_term d)
           in
           Ground.Subst.S.union substs acc)
         Ground.Subst.S.empty
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index c8e528bfb03dc584542b9c4b59f1c95bc6f16049..a545681a16217f9c9076b5f07d626883ae2fce6c 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -1,8 +1,9 @@
+open Colibri2_popop_lib
 (** Pattern *)
 
 type t =
   | Var of Expr.Term.Var.t
-  | App of F.t * Expr.Ty.t list * t list
+  | App of F.t * Expr.Ty.t list * t IArray.t
   | Node of Node.t
 
 include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 4d30a899b3d52b86a599d2b3e50511f67f5f3271..aab7a0b9df825935ef1d1926fd23270aefe8a0cc 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -227,24 +227,23 @@ let quantifier_registered d th =
 let application_useless d thg =
   let g = Ground.sem thg in
   let n = Ground.node thg in
-  match g.args with
-  | [] -> false (* No argument no congruence closure *)
-  | _ ->
-      let find_app pos n =
-        Opt.get_def Ground.S.empty
-        @@
-        let open Option in
-        let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
-        F_Pos.M.find_opt { f = g.app; pos } info.parents
-      in
-      let check_arg pos arg =
-        Ground.S.exists
-          (fun arg ->
-            Egraph.is_equal d n (Ground.node arg)
-            && List.for_all2 Ground.Ty.equal (Ground.sem arg).tyargs g.tyargs)
-          (find_app pos arg)
-      in
-      Base.List.for_alli ~f:check_arg g.args
+  if IArray.is_empty g.args then false (* No argument no congruence closure *)
+  else
+    let find_app pos n =
+      Opt.get_def Ground.S.empty
+      @@
+      let open Option in
+      let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
+      F_Pos.M.find_opt { f = g.app; pos } info.parents
+    in
+    let check_arg pos arg =
+      Ground.S.exists
+        (fun arg ->
+          Egraph.is_equal d n (Ground.node arg)
+          && List.for_all2 Ground.Ty.equal (Ground.sem arg).tyargs g.tyargs)
+        (find_app pos arg)
+    in
+    IArray.for_alli ~f:check_arg g.args
 
 let add_info_on_ground_terms d thg =
   Debug.dprintf2 debug_full "[Quant] add_info_on_ground_terms %a" Ground.pp thg;
@@ -268,7 +267,7 @@ let add_info_on_ground_terms d thg =
         parents = F_Pos.M.singleton { f = g.app; pos } (Ground.S.singleton thg);
       }
   in
-  List.iteri add_pc g.args;
+  IArray.iteri ~f:add_pc g.args;
   merge_info res
     { Info.empty with apps = F.M.singleton g.app (Ground.S.singleton thg) };
   Context.Queue.push (F.EnvApps.find Pattern.env_ground_by_apps d g.app) thg;
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index 5ca45cb49fff70e59d0bf7ada1c81de451be6515..a20932dd6e3327da0d9cb355d099fcdb57f4c42b 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -278,11 +278,9 @@ module UFModel = struct
   module Values = struct
     (** instantiated function symbol *)
     module T = struct
-      let hash_fold_list = Base.hash_fold_list
-
-      type t = Value.t list [@@deriving eq, ord, hash]
+      type t = Value.t IArray.t [@@deriving eq, ord, hash]
 
-      let pp fmt l = Fmt.(list ~sep:comma Value.pp) fmt l
+      let pp fmt l = Fmt.(IArray.pp ~sep:comma Value.pp) fmt l
     end
 
     include T
@@ -310,7 +308,7 @@ module UFModel = struct
     let check_or_update g d _ =
       let interp n = Option.get_exn (Egraph.get_value d n) in
       let s = Ground.sem g in
-      let lv = List.map interp s.args in
+      let lv = IArray.map ~f:interp s.args in
       let v = interp (Ground.node g) in
       match find d s lv with
       | Some v' -> if not (Value.equal v v') then Egraph.contradiction d
@@ -331,7 +329,7 @@ module On_uninterpreted_domain = struct
   let check d t =
     let interp n = Option.get_exn (Egraph.get_value d n) in
     let s = Ground.sem t in
-    let lv = List.map interp s.args in
+    let lv = IArray.map ~f:interp s.args in
     let v = interp (Ground.node t) in
     match UFModel.find d s lv with Some v' -> Value.equal v v' | None -> false
 end
@@ -346,7 +344,7 @@ let init_check d =
 let converter d (t : Ground.t) =
   match Ground.sem t with
   | { app = { builtin = Dolmen_std.Expr.Base; _ }; args; _ } ->
-      List.iter (Egraph.register d) args;
+      IArray.iter ~f:(Egraph.register d) args;
       UFModel.init_attach_value d t
   | _ -> ()