diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml
index 4a84f718..05695fe2 100644
--- a/src/base-solver/sidekick_base_solver.ml
+++ b/src/base-solver/sidekick_base_solver.ml
@@ -44,24 +44,22 @@ module Th_data = Sidekick_th_data.Make (struct
     match Term.view t with
     | Term.App_fun ({ fun_view = Fun.Fun_cstor c; _ }, args) -> T_cstor (c, args)
     | Term.App_fun ({ fun_view = Fun.Fun_select sel; _ }, args) ->
-      assert (IArray.length args = 1);
-      T_select (sel.select_cstor, sel.select_i, IArray.get args 0)
+      assert (CCArray.length args = 1);
+      T_select (sel.select_cstor, sel.select_i, CCArray.get args 0)
     | Term.App_fun ({ fun_view = Fun.Fun_is_a c; _ }, args) ->
-      assert (IArray.length args = 1);
-      T_is_a (c, IArray.get args 0)
+      assert (CCArray.length args = 1);
+      T_is_a (c, CCArray.get args 0)
     | _ -> T_other t
 
   let mk_eq = Term.eq
   let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
-
-  let mk_sel tst c i u =
-    Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u)
+  let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) [| u |]
 
   let mk_is_a tst c u : Term.t =
     if c.cstor_arity = 0 then
       Term.eq tst u (Term.const tst (Fun.cstor c))
     else
-      Term.app_fun tst (Fun.is_a c) (IArray.singleton u)
+      Term.app_fun tst (Fun.is_a c) [| u |]
 
   let ty_is_finite = Ty.finite
   let ty_set_is_finite = Ty.set_finite
diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml
index dd960976..f420e075 100644
--- a/src/base/Base_types.ml
+++ b/src/base/Base_types.ml
@@ -170,7 +170,7 @@ type term = {
     term view. *)
 and 'a term_view =
   | Bool of bool
-  | App_fun of fun_ * 'a IArray.t (* full, first-order application *)
+  | App_fun of fun_ * 'a array (* full, first-order application *)
   | Eq of 'a * 'a
   | Not of 'a
   | Ite of 'a * 'a * 'a
@@ -186,12 +186,12 @@ and fun_view =
   | Fun_cstor of cstor
   | Fun_is_a of cstor
   | Fun_def of {
-      pp: 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
-      abs: self:term -> term IArray.t -> term * bool; (* remove the sign? *)
+      pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
+      abs: self:term -> term array -> term * bool; (* remove the sign? *)
       do_cc: bool; (* participate in congruence closure? *)
-      relevant: 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
-      ty: ID.t -> term IArray.t -> ty; (* compute type *)
-      eval: value IArray.t -> value; (* evaluate term *)
+      relevant: 'a. ID.t -> 'a array -> int -> bool; (* relevant argument? *)
+      ty: ID.t -> term array -> ty; (* compute type *)
+      eval: value array -> value; (* evaluate term *)
     }
       (** Methods on the custom term view whose arguments are ['a].
     Terms must be printable, and provide some additional theory handles.
@@ -336,10 +336,9 @@ let pp_term_view_gen ~pp_id ~pp_t out = function
   | Bool false -> Fmt.string out "false"
   | App_fun ({ fun_view = Fun_def { pp = Some pp_custom; _ }; _ }, l) ->
     pp_custom pp_t out l
-  | App_fun (c, a) when IArray.is_empty a -> pp_id out (id_of_fun c)
+  | App_fun (c, [||]) -> pp_id out (id_of_fun c)
   | App_fun (f, l) ->
-    Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_fun f) (Util.pp_iarray pp_t)
-      l
+    Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_fun f) (Util.pp_array pp_t) l
   | Eq (a, b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
   | Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u
   | Ite (a, b, c) ->
@@ -547,13 +546,13 @@ module Fun : sig
     | Fun_cstor of cstor
     | Fun_is_a of cstor
     | Fun_def of {
-        pp: 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
-        abs: self:term -> term IArray.t -> term * bool; (* remove the sign? *)
+        pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
+        abs: self:term -> term array -> term * bool; (* remove the sign? *)
         do_cc: bool; (* participate in congruence closure? *)
-        relevant: 'a. ID.t -> 'a IArray.t -> int -> bool;
+        relevant: 'a. ID.t -> 'a array -> int -> bool;
         (* relevant argument? *)
-        ty: ID.t -> term IArray.t -> ty; (* compute type *)
-        eval: value IArray.t -> value; (* evaluate term *)
+        ty: ID.t -> term array -> ty; (* compute type *)
+        eval: value array -> value; (* evaluate term *)
       }
         (** user defined function symbol.
             A good example can be found in {!Form} for boolean connectives. *)
@@ -594,13 +593,13 @@ end = struct
     | Fun_cstor of cstor
     | Fun_is_a of cstor
     | Fun_def of {
-        pp: 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
-        abs: self:term -> term IArray.t -> term * bool; (* remove the sign? *)
+        pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
+        abs: self:term -> term array -> term * bool; (* remove the sign? *)
         do_cc: bool; (* participate in congruence closure? *)
-        relevant: 'a. ID.t -> 'a IArray.t -> int -> bool;
+        relevant: 'a. ID.t -> 'a array -> int -> bool;
         (* relevant argument? *)
-        ty: ID.t -> term IArray.t -> ty; (* compute type *)
-        eval: value IArray.t -> value; (* evaluate term *)
+        ty: ID.t -> term array -> ty; (* compute type *)
+        eval: value array -> value; (* evaluate term *)
       }
 
   type t = fun_ = { fun_id: ID.t; fun_view: fun_view }
@@ -666,7 +665,7 @@ end
 module Term_cell : sig
   type 'a view = 'a term_view =
     | Bool of bool
-    | App_fun of fun_ * 'a IArray.t
+    | App_fun of fun_ * 'a array
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
@@ -680,7 +679,7 @@ module Term_cell : sig
   val true_ : t
   val false_ : t
   val const : fun_ -> t
-  val app_fun : fun_ -> term IArray.t -> t
+  val app_fun : fun_ -> term array -> t
   val eq : term -> term -> t
   val not_ : term -> t
   val ite : term -> term -> term -> t
@@ -710,7 +709,7 @@ module Term_cell : sig
 end = struct
   type 'a view = 'a term_view =
     | Bool of bool
-    | App_fun of fun_ * 'a IArray.t
+    | App_fun of fun_ * 'a array
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
@@ -746,7 +745,7 @@ end = struct
       match a, b with
       | Bool b1, Bool b2 -> CCBool.equal b1 b2
       | App_fun (f1, a1), App_fun (f2, a2) ->
-        Fun.equal f1 f2 && IArray.equal sub_eq a1 a2
+        Fun.equal f1 f2 && CCArray.equal sub_eq a1 a2
       | Eq (a1, b1), Eq (a2, b2) -> sub_eq a1 a2 && sub_eq b1 b2
       | Not a, Not b -> sub_eq a b
       | Ite (a1, b1, c1), Ite (a2, b2, c2) ->
@@ -770,7 +769,7 @@ end = struct
   let true_ = Bool true
   let false_ = Bool false
   let app_fun f a = App_fun (f, a)
-  let const c = App_fun (c, IArray.empty)
+  let const c = App_fun (c, CCArray.empty)
 
   let eq a b =
     if term_equal_ a b then
@@ -805,13 +804,13 @@ end = struct
       | Fun_undef fty ->
         let ty_args, ty_ret = Ty.Fun.unfold fty in
         (* check arity *)
-        if List.length ty_args <> IArray.length args then
+        if List.length ty_args <> CCArray.length args then
           Error.errorf "Term_cell.apply: expected %d args, got %d@ in %a"
-            (List.length ty_args) (IArray.length args) pp t;
+            (List.length ty_args) (CCArray.length args) pp t;
         (* check types *)
         List.iteri
           (fun i ty_a ->
-            let a = IArray.get args i in
+            let a = CCArray.get args i in
             if not @@ Ty.equal a.term_ty ty_a then
               Error.errorf
                 "Term_cell.apply: %d-th argument mismatch:@ %a does not have \
@@ -839,7 +838,7 @@ end = struct
   let iter f view =
     match view with
     | Bool _ -> ()
-    | App_fun (_, a) -> IArray.iter f a
+    | App_fun (_, a) -> CCArray.iter f a
     | Not u -> f u
     | Eq (a, b) ->
       f a;
@@ -854,7 +853,7 @@ end = struct
   let map f view =
     match view with
     | Bool b -> Bool b
-    | App_fun (fu, a) -> App_fun (fu, IArray.map f a)
+    | App_fun (fu, a) -> App_fun (fu, CCArray.map f a)
     | Not u -> Not (f u)
     | Eq (a, b) -> Eq (f a, f b)
     | Ite (a, b, c) -> Ite (f a, f b, f c)
@@ -872,7 +871,7 @@ module Term : sig
 
   type 'a view = 'a term_view =
     | Bool of bool
-    | App_fun of fun_ * 'a IArray.t
+    | App_fun of fun_ * 'a array
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
@@ -894,13 +893,13 @@ module Term : sig
   val false_ : store -> t
   val bool : store -> bool -> t
   val const : store -> fun_ -> t
-  val app_fun : store -> fun_ -> t IArray.t -> t
+  val app_fun : store -> fun_ -> t array -> t
   val app_fun_l : store -> fun_ -> t list -> t
   val eq : store -> t -> t -> t
   val not_ : store -> t -> t
   val ite : store -> t -> t -> t -> t
 
-  val app_undefined : store -> ID.t -> Ty.Fun.t -> t IArray.t -> t
+  val app_undefined : store -> ID.t -> Ty.Fun.t -> t array -> t
   (** [app_undefined store f ty args] is [app store (Fun.mk_undef f ty) args].
       It builds a function symbol and applies it into a term immediately *)
 
@@ -910,7 +909,7 @@ module Term : sig
       immediately. *)
 
   val select : store -> select -> t -> t
-  val app_cstor : store -> cstor -> t IArray.t -> t
+  val app_cstor : store -> cstor -> t array -> t
   val is_a : store -> cstor -> t -> t
   val lra : store -> t LRA_view.t -> t
   val lia : store -> t LIA_view.t -> t
@@ -980,7 +979,7 @@ end = struct
 
   type 'a view = 'a term_view =
     | Bool of bool
-    | App_fun of fun_ * 'a IArray.t
+    | App_fun of fun_ * 'a array
     | Eq of 'a * 'a
     | Not of 'a
     | Ite of 'a * 'a * 'a
@@ -1039,13 +1038,13 @@ end = struct
     let cell = Term_cell.app_fun f a in
     make st cell
 
-  let app_fun_l st f l = app_fun st f (IArray.of_list l)
-  let[@inline] const st c = app_fun st c IArray.empty
+  let app_fun_l st f l = app_fun st f (CCArray.of_list l)
+  let[@inline] const st c = app_fun st c CCArray.empty
   let[@inline] eq st a b = make st (Term_cell.eq a b)
   let[@inline] not_ st a = make st (Term_cell.not_ a)
   let ite st a b c : t = make st (Term_cell.ite a b c)
-  let select st sel t : t = app_fun st (Fun.select sel) (IArray.singleton t)
-  let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t)
+  let select st sel t : t = app_fun st (Fun.select sel) [| t |]
+  let is_a st c t : t = app_fun st (Fun.is_a c) [| t |]
   let app_cstor st c args : t = app_fun st (Fun.cstor c) args
 
   let[@inline] lra (st : store) (l : t LRA_view.t) : t =
@@ -1133,7 +1132,7 @@ end = struct
 
   let[@inline] is_const t =
     match view t with
-    | App_fun (_, a) -> IArray.is_empty a
+    | App_fun (_, [||]) -> true
     | _ -> false
 
   let cc_view (t : t) =
@@ -1141,7 +1140,7 @@ end = struct
     match view t with
     | Bool b -> C.Bool b
     | App_fun (f, _) when not (Fun.do_cc f) -> C.Opaque t (* skip *)
-    | App_fun (f, args) -> C.App_fun (f, IArray.to_iter args)
+    | App_fun (f, args) -> C.App_fun (f, CCArray.to_iter args)
     | Eq (a, b) -> C.Eq (a, b)
     | Not u -> C.Not u
     | Ite (a, b, c) -> C.If (a, b, c)
@@ -1169,7 +1168,7 @@ end = struct
   (* return [Some] iff the term is an undefined constant *)
   let as_fun_undef (t : term) : (fun_ * Ty.Fun.t) option =
     match view t with
-    | App_fun (c, a) when IArray.is_empty a -> Fun.as_undefined c
+    | App_fun (c, [||]) -> Fun.as_undefined c
     | _ -> None
 
   let as_bool t =
@@ -1212,7 +1211,7 @@ end = struct
   let map_shallow (tst : store) f (t : t) : t =
     match view t with
     | Bool _ -> t
-    | App_fun (hd, a) -> app_fun tst hd (IArray.map f a)
+    | App_fun (hd, a) -> app_fun tst hd (CCArray.map f a)
     | Not u -> not_ tst (f u)
     | Eq (a, b) -> eq tst (f a) (f b)
     | Ite (a, b, c) -> ite tst (f a) (f b) (f c)
diff --git a/src/base/Form.ml b/src/base/Form.ml
index d5035389..45cb908a 100644
--- a/src/base/Form.ml
+++ b/src/base/Form.ml
@@ -21,13 +21,14 @@ let id_imply = ID.make "=>"
 
 let view_id fid args =
   if ID.equal fid id_and then
-    B_and (IArray.to_iter args)
+    B_and (CCArray.to_iter args)
   else if ID.equal fid id_or then
-    B_or (IArray.to_iter args)
-  else if ID.equal fid id_imply && IArray.length args >= 2 then (
+    B_or (CCArray.to_iter args)
+  else if ID.equal fid id_imply && CCArray.length args >= 2 then (
     (* conclusion is stored last *)
-    let len = IArray.length args in
-    B_imply (IArray.to_iter_sub args 0 (len - 1), IArray.get args (len - 1))
+    let len = CCArray.length args in
+    B_imply
+      (Iter.of_array args |> Iter.take (len - 1), CCArray.get args (len - 1))
   ) else
     raise_notrace Not_a_th_term
 
@@ -92,7 +93,7 @@ module Funs = struct
   let ite = T.ite
 end
 
-let as_id id (t : T.t) : T.t IArray.t option =
+let as_id id (t : T.t) : T.t array option =
   match T.view t with
   | App_fun ({ fun_id; _ }, args) when ID.equal id fun_id -> Some args
   | _ -> None
@@ -102,7 +103,7 @@ let flatten_id op sign (l : T.t list) : T.t list =
   CCList.flat_map
     (fun t ->
       match as_id op t with
-      | Some args -> IArray.to_list args
+      | Some args -> CCArray.to_list args
       | None when (sign && T.is_true t) || ((not sign) && T.is_false t) ->
         [] (* idempotent *)
       | None -> [ t ])
@@ -113,19 +114,19 @@ let and_l st l =
   | [] -> T.true_ st
   | l when List.exists T.is_false l -> T.false_ st
   | [ x ] -> x
-  | args -> T.app_fun st Funs.and_ (IArray.of_list args)
+  | args -> T.app_fun st Funs.and_ (CCArray.of_list args)
 
 let or_l st l =
   match flatten_id id_or false l with
   | [] -> T.false_ st
   | l when List.exists T.is_true l -> T.true_ st
   | [ x ] -> x
-  | args -> T.app_fun st Funs.or_ (IArray.of_list args)
+  | args -> T.app_fun st Funs.or_ (CCArray.of_list args)
 
 let and_ st a b = and_l st [ a; b ]
 let or_ st a b = or_l st [ a; b ]
-let and_a st a = and_l st (IArray.to_list a)
-let or_a st a = or_l st (IArray.to_list a)
+let and_a st a = and_l st (CCArray.to_list a)
+let or_a st a = or_l st (CCArray.to_list a)
 let eq = T.eq
 let not_ = T.not_
 
@@ -155,17 +156,17 @@ let equiv st a b =
 let neq st a b = not_ st @@ eq st a b
 
 let imply_a st xs y =
-  if IArray.is_empty xs then
+  if Array.length xs = 0 then
     y
   else
-    T.app_fun st Funs.imply (IArray.append xs (IArray.singleton y))
+    T.app_fun st Funs.imply (CCArray.append xs [| y |])
 
 let imply_l st xs y =
   match xs with
   | [] -> y
-  | _ -> imply_a st (IArray.of_list xs) y
+  | _ -> imply_a st (CCArray.of_list xs) y
 
-let imply st a b = imply_a st (IArray.singleton a) b
+let imply st a b = imply_a st [| a |] b
 let xor st a b = not_ st (equiv st a b)
 
 let distinct_l tst l =
diff --git a/src/base/Model.ml b/src/base/Model.ml
index 2ebef5bd..21c53d05 100644
--- a/src/base/Model.ml
+++ b/src/base/Model.ml
@@ -170,12 +170,12 @@ let eval (m : t) (t : Term.t) : Value.t option =
       *)
     | LIA _l -> assert false (* TODO *)
     | App_fun (c, args) ->
-      (match Fun.view c, (args : _ IArray.t :> _ array) with
+      (match Fun.view c, (args : _ array :> _ array) with
       | Fun_def udef, _ ->
         (* use builtin interpretation function *)
-        let args = IArray.map aux args in
+        let args = CCArray.map aux args in
         udef.eval args
-      | Fun_cstor c, _ -> Value.cstor_app c (IArray.to_list_map aux args)
+      | Fun_cstor c, _ -> Value.cstor_app c (Util.array_to_list_map aux args)
       | Fun_select s, [| u |] ->
         (match aux u with
         | V_cstor { c; args } when Cstor.equal c s.select_cstor ->
@@ -194,7 +194,7 @@ let eval (m : t) (t : Term.t) : Value.t option =
          with Not_found ->
            (match Fun.Map.find c m.funs with
            | fi ->
-             let args = IArray.map aux args |> IArray.to_list in
+             let args = CCArray.map aux args |> CCArray.to_list in
              (match Val_map.find args fi.FI.cases with
              | None -> fi.FI.default
              | Some v -> v)
diff --git a/src/base/Proof.ml b/src/base/Proof.ml
index 25e2821d..96de480e 100644
--- a/src/base/Proof.ml
+++ b/src/base/Proof.ml
@@ -151,14 +151,14 @@ let rec emit_term_ (self : t) (t : Term.t) : term_id =
         PS.Step_view.Expr_if { PS.Expr_if.cond = a; then_ = b; else_ = c }
       | Term_cell.Not a -> PS.Step_view.Expr_not { PS.Expr_not.f = a }
       | Term_cell.App_fun ({ fun_view = Fun.Fun_is_a c; _ }, args) ->
-        assert (IArray.length args = 1);
+        assert (CCArray.length args = 1);
         let c = emit_fun_ self (Fun.cstor c) in
-        let arg = IArray.get args 0 in
+        let arg = CCArray.get args 0 in
         PS.Step_view.Expr_isa { PS.Expr_isa.c; arg }
       | Term_cell.App_fun (f, arr) ->
         let f = emit_fun_ self f in
         PS.Step_view.Expr_app
-          { PS.Expr_app.f; args = (arr : _ IArray.t :> _ array) }
+          { PS.Expr_app.f; args = (arr : _ array :> _ array) }
       | Term_cell.Eq (a, b) ->
         PS.Step_view.Expr_eq { PS.Expr_eq.lhs = a; rhs = b }
       | LRA _ | LIA _ -> assert false
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 504931cd..ce108e2b 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -1279,7 +1279,7 @@ module type SOLVER = sig
 
       The proof of [|- lit = lit'] is directly added to the solver's proof. *)
 
-  val add_clause : t -> lit IArray.t -> proof_step -> unit
+  val add_clause : t -> lit array -> proof_step -> unit
   (** [add_clause solver cs] adds a boolean clause to the solver.
       Subsequent calls to {!solve} will need to satisfy this clause. *)
 
diff --git a/src/mini-cc/tests/sidekick_test_minicc.ml b/src/mini-cc/tests/sidekick_test_minicc.ml
index 8374d9cd..0d96fd3e 100644
--- a/src/mini-cc/tests/sidekick_test_minicc.ml
+++ b/src/mini-cc/tests/sidekick_test_minicc.ml
@@ -24,7 +24,7 @@ module Setup () = struct
   let false_ = Term.false_ tst
   let const c = Term.const tst c
   let app_a f l = Term.app_fun tst f l
-  let app_l f l = Term.app_fun tst f (IArray.of_list l)
+  let app_l f l = Term.app_fun tst f (CCArray.of_list l)
   let not_ x = Term.not_ tst x
   let eq a b = Term.eq tst a b
   let neq a b = Term.not_ tst (eq a b)
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 8a757932..3547d815 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -508,7 +508,7 @@ module Make (A : ARG) :
     [@@inline]
 
     module PC_list = Preprocess_clause (CCList)
-    module PC_arr = Preprocess_clause (IArray)
+    module PC_arr = Preprocess_clause (CCArray)
 
     let preprocess_clause_ = PC_list.top
     let preprocess_clause_iarray_ = PC_arr.top
@@ -966,8 +966,8 @@ module Make (A : ARG) :
   let reset_last_res_ self = self.last_res <- None
 
   (* preprocess clause, return new proof *)
-  let preprocess_clause_ (self : t) (c : lit IArray.t) (pr : proof_step) :
-      lit IArray.t * proof_step =
+  let preprocess_clause_ (self : t) (c : lit array) (pr : proof_step) :
+      lit array * proof_step =
     Solver_internal.preprocess_clause_iarray_ self.si c pr
 
   let mk_lit_t (self : t) ?sign (t : term) : lit =
@@ -980,18 +980,18 @@ module Make (A : ARG) :
   let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self)
 
   (* add [c], without preprocessing its literals *)
-  let add_clause_nopreproc_ (self : t) (c : lit IArray.t) (proof : proof_step) :
+  let add_clause_nopreproc_ (self : t) (c : lit array) (proof : proof_step) :
       unit =
     Stat.incr self.count_clause;
     reset_last_res_ self;
     Log.debugf 50 (fun k ->
-        k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Lit.pp) c);
+        k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c);
     let pb = Profile.begin_ "add-clause" in
     Sat_solver.add_clause_a self.solver (c :> lit array) proof;
     Profile.exit pb
 
   let add_clause_nopreproc_l_ self c p =
-    add_clause_nopreproc_ self (IArray.of_list c) p
+    add_clause_nopreproc_ self (CCArray.of_list c) p
 
   module Perform_delayed_ = Solver_internal.Perform_delayed (struct
     type nonrec t = t
@@ -1003,14 +1003,14 @@ module Make (A : ARG) :
       Sat_solver.add_lit solver.solver ?default_pol lit
   end)
 
-  let add_clause (self : t) (c : lit IArray.t) (proof : proof_step) : unit =
+  let add_clause (self : t) (c : lit array) (proof : proof_step) : unit =
     let c, proof = preprocess_clause_ self c proof in
     add_clause_nopreproc_ self c proof;
     Perform_delayed_.top self.si self;
     (* finish preproc *)
     ()
 
-  let add_clause_l self c p = add_clause self (IArray.of_list c) p
+  let add_clause_l self c p = add_clause self (CCArray.of_list c) p
 
   let assert_terms self c =
     let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 415e730c..fd3dae29 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -280,7 +280,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
   | Statement.Stmt_assert t ->
     if pp_cnf then Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t;
     let lit = Solver.mk_lit_t solver t in
-    Solver.add_clause solver (IArray.singleton lit)
+    Solver.add_clause solver [| lit |]
       (Solver.P.emit_input_clause (Iter.singleton lit) (Solver.proof solver));
     E.return ()
   | Statement.Stmt_assert_clause c_ts ->
@@ -297,7 +297,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
       P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) proof
     in
 
-    Solver.add_clause solver (IArray.of_list c) pr;
+    Solver.add_clause solver (CCArray.of_list c) pr;
     E.return ()
   | Statement.Stmt_get_model ->
     (match Solver.last_res solver with
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index 939a4c36..3b800a79 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -237,7 +237,7 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t =
   | PA.App (f, args) ->
     let args = List.map (conv_term ctx) args in
     (match find_id_ ctx f with
-    | _, Ctx.K_fun f -> T.app_fun tst f (IArray.of_list args)
+    | _, Ctx.K_fun f -> T.app_fun tst f (CCArray.of_list args)
     | _, Ctx.K_ty _ ->
       errorf_ctx ctx "expected function, got type `%s` instead" f)
   | PA.If (a, b, c) ->
diff --git a/src/th-bool-dyn/Sidekick_th_bool_dyn.ml b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml
index 13ffba32..27680ae3 100644
--- a/src/th-bool-dyn/Sidekick_th_bool_dyn.ml
+++ b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml
@@ -4,9 +4,9 @@
 module View = struct
   type 'a t =
     | B_not of 'a
-    | B_and of 'a IArray.t
-    | B_or of 'a IArray.t
-    | B_imply of 'a IArray.t * 'a
+    | B_and of 'a array
+    | B_or of 'a array
+    | B_imply of 'a array * 'a
     | B_atom of 'a
 end
 
@@ -58,35 +58,35 @@ struct
     | B_and subs ->
       if Lit.sign lit then
         (* propagate [lit => subs_i] *)
-        IArray.iter
+        CCArray.iter
           (fun sub ->
             let sublit = SI.mk_lit solver sub in
             SI.propagate_l solver sublit [ lit ])
           subs
       else if final && (not @@ expanded ()) then (
         (* axiom [¬lit => ∨_i ¬ subs_i] *)
-        let subs = IArray.to_list subs in
+        let subs = CCArray.to_list subs in
         let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:false) subs in
         add_axiom c
       )
     | B_or subs ->
       if not @@ Lit.sign lit then
         (* propagate [¬lit => ¬subs_i] *)
-        IArray.iter
+        CCArray.iter
           (fun sub ->
             let sublit = SI.mk_lit solver ~sign:false sub in
             SI.add_local_axiom solver [ Lit.neg lit; sublit ])
           subs
       else if final && (not @@ expanded ()) then (
         (* axiom [lit => ∨_i subs_i] *)
-        let subs = IArray.to_list subs in
+        let subs = CCArray.to_list subs in
         let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:true) subs in
         add_axiom c
       )
     | B_imply (guard, concl) ->
       if Lit.sign lit && final && (not @@ expanded ()) then (
         (* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
-        let guard = IArray.to_list guard in
+        let guard = CCArray.to_list guard in
         let c =
           SI.mk_lit solver concl :: Lit.neg lit
           :: List.map (SI.mk_lit solver ~sign:false) guard
@@ -96,7 +96,7 @@ struct
         (* propagate [¬lit => ¬concl] *)
         SI.propagate_l solver (SI.mk_lit solver ~sign:false concl) [ lit ];
         (* propagate [¬lit => ∧_i guard_i] *)
-        IArray.iter
+        CCArray.iter
           (fun sub ->
             let sublit = SI.mk_lit solver ~sign:true sub in
             SI.propagate_l solver sublit [ lit ])
diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml
index 754734e8..14cd7898 100644
--- a/src/th-bool-static/Sidekick_th_bool_static.ml
+++ b/src/th-bool-static/Sidekick_th_bool_static.ml
@@ -50,7 +50,7 @@ module type ARG = sig
   val view_as_bool : term -> (term, term Iter.t) bool_view
   (** Project the term into the boolean view. *)
 
-  val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term
+  val mk_bool : S.T.Term.store -> (term, term array) bool_view -> term
   (** Make a term from the given boolean view. *)
 
   include
diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml
index 2154cb88..1a266f26 100644
--- a/src/th-cstor/Sidekick_th_cstor.ml
+++ b/src/th-cstor/Sidekick_th_cstor.ml
@@ -1,6 +1,6 @@
 (** {1 Theory for constructors} *)
 
-type ('c, 't) cstor_view = T_cstor of 'c * 't IArray.t | T_other of 't
+type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't
 
 let name = "th-cstor"
 
@@ -29,7 +29,7 @@ module Make (A : ARG) : S with module A = A = struct
     module SI = SI
 
     (* associate to each class a unique constructor term in the class (if any) *)
-    type t = { t: T.t; n: N.t; cstor: Fun.t; args: N.t IArray.t }
+    type t = { t: T.t; n: N.t; cstor: Fun.t; args: N.t array }
 
     let name = name
 
@@ -40,7 +40,7 @@ module Make (A : ARG) : S with module A = A = struct
     let of_term cc n (t : T.t) : _ option * _ =
       match A.view_as_cstor t with
       | T_cstor (cstor, args) ->
-        let args = IArray.map (SI.CC.add_term cc) args in
+        let args = CCArray.map (SI.CC.add_term cc) args in
         Some { n; t; cstor; args }, []
       | _ -> None, []
 
@@ -57,8 +57,8 @@ module Make (A : ARG) : S with module A = A = struct
       in
       if Fun.equal v1.cstor v2.cstor then (
         (* same function: injectivity *)
-        assert (IArray.length v1.args = IArray.length v2.args);
-        IArray.iter2 (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) v1.args v2.args;
+        assert (CCArray.length v1.args = CCArray.length v2.args);
+        CCArray.iter2 (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) v1.args v2.args;
         Ok v1
       ) else
         (* different function: disjointness *)
diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index bf1a4673..672f0aef 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -172,17 +172,17 @@ module Make (A : ARG) : S with module A = A = struct
     let name = "th-data.cstor"
 
     (* associate to each class a unique constructor term in the class (if any) *)
-    type t = { c_n: N.t; c_cstor: A.Cstor.t; c_args: N.t IArray.t }
+    type t = { c_n: N.t; c_cstor: A.Cstor.t; c_args: N.t array }
 
     let pp out (v : t) =
       Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@ :args [@[%a@]]@])" name
-        A.Cstor.pp v.c_cstor N.pp v.c_n (Util.pp_iarray N.pp) v.c_args
+        A.Cstor.pp v.c_cstor N.pp v.c_n (Util.pp_array N.pp) v.c_args
 
     (* attach data to constructor terms *)
     let of_term cc n (t : T.t) : _ option * _ list =
       match A.view_as_data t with
       | T_cstor (cstor, args) ->
-        let args = IArray.map (SI.CC.add_term cc) args in
+        let args = CCArray.map (SI.CC.add_term cc) args in
         Some { c_n = n; c_cstor = cstor; c_args = args }, []
       | _ -> None, []
 
@@ -209,10 +209,9 @@ module Make (A : ARG) : S with module A = A = struct
           mk_expl t1 t2 @@ A.P.lemma_cstor_inj t1 t2 i (SI.CC.proof cc)
         in
 
-        assert (IArray.length c1.c_args = IArray.length c2.c_args);
-        IArray.iteri2
-          (fun i u1 u2 -> SI.CC.merge cc u1 u2 (expl_merge i))
-          c1.c_args c2.c_args;
+        assert (CCArray.length c1.c_args = CCArray.length c2.c_args);
+        Util.array_iteri2 c1.c_args c2.c_args ~f:(fun i u1 u2 ->
+            SI.CC.merge cc u1 u2 (expl_merge i));
         Ok c1
       ) else (
         (* different function: disjointness *)
@@ -342,7 +341,7 @@ module Make (A : ARG) : S with module A = A = struct
           let sel_args =
             A.Cstor.ty_args cstor
             |> Iter.mapi (fun i ty -> A.mk_sel self.tst cstor i t)
-            |> Iter.to_array |> IArray.of_array_unsafe
+            |> Iter.to_array
           in
           A.mk_cstor self.tst cstor sel_args
         in
@@ -421,8 +420,8 @@ module Make (A : ARG) : S with module A = A = struct
         Log.debugf 5 (fun k ->
             k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" name
               N.pp n i A.Cstor.pp c_t);
-        assert (i < IArray.length cstor.c_args);
-        let u_i = IArray.get cstor.c_args i in
+        assert (i < CCArray.length cstor.c_args);
+        let u_i = CCArray.get cstor.c_args i in
         let pr =
           A.P.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc)
         in
@@ -473,12 +472,12 @@ module Make (A : ARG) : S with module A = A = struct
         Log.debugf 5 (fun k ->
             k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name
               N.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
-        assert (sel2.sel_idx < IArray.length c1.c_args);
+        assert (sel2.sel_idx < CCArray.length c1.c_args);
         let pr =
           A.P.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n)
             self.proof
         in
-        let u_i = IArray.get c1.c_args sel2.sel_idx in
+        let u_i = CCArray.get c1.c_args sel2.sel_idx in
         SI.CC.merge cc sel2.sel_n u_i
           (Expl.mk_theory (N.term sel2.sel_n) (N.term u_i)
              [
@@ -545,7 +544,7 @@ module Make (A : ARG) : S with module A = A = struct
     let mk_graph (self : t) cc : graph =
       let g : graph = N_tbl.create ~size:32 () in
       let traverse_sub cstor : _ list =
-        IArray.to_list_map
+        Util.array_to_list_map
           (fun sub_n -> sub_n, SI.CC.find cc sub_n)
           cstor.Monoid_cstor.c_args
       in
@@ -625,7 +624,7 @@ module Make (A : ARG) : S with module A = A = struct
           let args =
             A.Cstor.ty_args c
             |> Iter.mapi (fun i _ty -> A.mk_sel self.tst c i u)
-            |> Iter.to_list |> IArray.of_list
+            |> Iter.to_list |> CCArray.of_list
           in
           A.mk_cstor self.tst c args
         in
@@ -725,7 +724,7 @@ module Make (A : ARG) : S with module A = A = struct
           let args =
             A.Cstor.ty_args base_cstor
             |> Iter.mapi (fun i _ -> A.mk_sel self.tst base_cstor i t)
-            |> IArray.of_iter
+            |> Iter.to_array
           in
           A.mk_cstor self.tst base_cstor args
         in
@@ -746,7 +745,7 @@ module Make (A : ARG) : S with module A = A = struct
     | Some c ->
       Log.debugf 5 (fun k ->
           k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c);
-      let args = IArray.map (recurse si) c.c_args in
+      let args = CCArray.map (recurse si) c.c_args in
       let t = A.mk_cstor self.tst c.c_cstor args in
       Some t
 
diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml
index 9ded391d..e0cafea7 100644
--- a/src/th-data/th_intf.ml
+++ b/src/th-data/th_intf.ml
@@ -4,7 +4,7 @@
     - ['t] is the representation of terms
 *)
 type ('c, 't) data_view =
-  | T_cstor of 'c * 't IArray.t
+  | T_cstor of 'c * 't array
   | T_select of 'c * int * 't
   | T_is_a of 'c * 't
   | T_other of 't
@@ -82,7 +82,7 @@ module type ARG = sig
   val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
   (** Try to view term as a datatype term *)
 
-  val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
+  val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t array -> S.T.Term.t
   (** Make a constructor application term *)
 
   val mk_is_a : S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t
diff --git a/src/th-data/types.ml b/src/th-data/types.ml
index bcb52385..59bf1448 100644
--- a/src/th-data/types.ml
+++ b/src/th-data/types.ml
@@ -11,8 +11,8 @@ and datatype = {
 (* a constructor *)
 and data_cstor = {
   cstor_ty: ty;
-  cstor_args: ty IArray.t; (* argument types *)
-  cstor_proj: cst IArray.t lazy_t; (* projectors *)
+  cstor_args: ty array; (* argument types *)
+  cstor_proj: cst array lazy_t; (* projectors *)
   cstor_test: cst lazy_t; (* tester *)
   cstor_cst: cst; (* the cstor itself *)
   cstor_card: ty_card; (* cardinality of the constructor('s args) *)
@@ -43,10 +43,10 @@ let if_ a b c =
   If (a,b,c)
 
 let cstor_test cstor t =
-  app_cst (Lazy.force cstor.cstor_test) (IArray.singleton t)
+  app_cst (Lazy.force cstor.cstor_test) (CCArray.singleton t)
 
 let cstor_proj cstor i t =
-  let p = IArray.get (Lazy.force cstor.cstor_proj) i in
-  app_cst p (IArray.singleton t)
+  let p = CCArray.get (Lazy.force cstor.cstor_proj) i in
+  app_cst p (CCArray.singleton t)
 
    *)
diff --git a/src/util/Bitvec.ml b/src/util/Bitvec.ml
index 9a3e7a32..b7b3b4bc 100644
--- a/src/util/Bitvec.ml
+++ b/src/util/Bitvec.ml
@@ -1,7 +1,7 @@
-type t = { mutable chunks: bytes (* TODO: use a in32vec with bigarray *) }
+type t = { mutable chunks: bytes }
 
 let create () : t = { chunks = Bytes.make 32 '\x00' }
-let i2c = Char.chr
+let i2c = Char.unsafe_chr
 let c2i = Char.code
 
 (* from index to offset in bytes *)
diff --git a/src/util/Bitvec.mli b/src/util/Bitvec.mli
index 1d2331c0..12558d12 100644
--- a/src/util/Bitvec.mli
+++ b/src/util/Bitvec.mli
@@ -1,4 +1,7 @@
-(** Bitvector *)
+(** Bitvector.
+
+   This provides compact storage with O(1) access to a range of bits,
+   like [bool Vec.t] but packed better. *)
 
 type t
 
diff --git a/src/util/Hash.ml b/src/util/Hash.ml
index 0d3571f2..82a40add 100644
--- a/src/util/Hash.ml
+++ b/src/util/Hash.ml
@@ -77,7 +77,7 @@ let bool b =
 
 let list f l = List.fold_left (combine f) 0x42 l
 let array f = Array.fold_left (combine f) 0x43
-let iarray f = IArray.fold (combine f) 0x44
+let iarray f = CCArray.fold (combine f) 0x44
 let string : string t = Hashtbl.hash
 
 let seq f seq =
diff --git a/src/util/Hash.mli b/src/util/Hash.mli
index 77fdf9be..82c9a1f0 100644
--- a/src/util/Hash.mli
+++ b/src/util/Hash.mli
@@ -10,7 +10,7 @@ val pair : 'a t -> 'b t -> ('a * 'b) t
 val opt : 'a t -> 'a option t
 val list : 'a t -> 'a list t
 val array : 'a t -> 'a array t
-val iarray : 'a t -> 'a IArray.t t
+val iarray : 'a t -> 'a array t
 val seq : 'a t -> 'a Iter.t t
 val combine2 : int -> int -> int
 val combine3 : int -> int -> int -> int
diff --git a/src/util/IArray.ml b/src/util/IArray.ml
deleted file mode 100644
index 37db58d9..00000000
--- a/src/util/IArray.ml
+++ /dev/null
@@ -1,175 +0,0 @@
-(* This file is free software. See file "license" for more details. *)
-
-type 'a t = 'a array
-
-let empty = [||]
-let is_empty a = Array.length a = 0
-let length = Array.length
-let singleton x = [| x |]
-let doubleton x y = [| x; y |]
-let make n x = Array.make n x
-let init n f = Array.init n f
-let sub = Array.sub
-let get = Array.get
-let unsafe_get = Array.unsafe_get
-
-let set a n x =
-  let a' = Array.copy a in
-  a'.(n) <- x;
-  a'
-
-let map = Array.map
-let mapi = Array.mapi
-
-let append a b =
-  let na = length a in
-  Array.init
-    (na + length b)
-    (fun i ->
-      if i < na then
-        a.(i)
-      else
-        b.(i - na))
-
-let iter = Array.iter
-let iteri = Array.iteri
-let fold = Array.fold_left
-
-let foldi f acc a =
-  let n = ref 0 in
-  Array.fold_left
-    (fun acc x ->
-      let acc = f acc !n x in
-      incr n;
-      acc)
-    acc a
-
-exception ExitNow
-
-let for_all p a =
-  try
-    Array.iter (fun x -> if not (p x) then raise ExitNow) a;
-    true
-  with ExitNow -> false
-
-let exists p a =
-  try
-    Array.iter (fun x -> if p x then raise ExitNow) a;
-    false
-  with ExitNow -> true
-
-(** {2 Conversions} *)
-
-type 'a iter = ('a -> unit) -> unit
-type 'a gen = unit -> 'a option
-
-let of_list = Array.of_list
-let to_list = Array.to_list
-
-let of_list_map f l =
-  match l with
-  | [] -> empty
-  | x :: _ ->
-    let arr = make (List.length l) (f x) in
-    List.iteri (fun i x -> Array.unsafe_set arr i (f x)) l;
-    arr
-
-let to_list_map f a = CCArray.fold_right (fun x acc -> f x :: acc) a []
-let of_array_map = Array.map
-let to_array_map = Array.map
-let of_array_unsafe a = a (* careful with that axe, Eugene *)
-
-let to_iter a k = iter k a
-
-let to_iter_sub a i len k =
-  if i < 0 || i + len > Array.length a then invalid_arg "IArray.iter_sub";
-  for j = i to i + len - 1 do
-    k (Array.unsafe_get a j)
-  done
-
-let of_iter s =
-  let l = ref [] in
-  s (fun x -> l := x :: !l);
-  Array.of_list (List.rev !l)
-
-(*$Q
-  Q.(list int) (fun l -> \
-    let g = Iter.of_list l in \
-    of_iter g |> to_iter |> Iter.to_list = l)
-*)
-
-let rec gen_to_list_ acc g =
-  match g () with
-  | None -> List.rev acc
-  | Some x -> gen_to_list_ (x :: acc) g
-
-let of_gen g =
-  let l = gen_to_list_ [] g in
-  Array.of_list l
-
-let to_gen a =
-  let i = ref 0 in
-  fun () ->
-    if !i < Array.length a then (
-      let x = a.(!i) in
-      incr i;
-      Some x
-    ) else
-      None
-
-(*$Q
-  Q.(list int) (fun l -> \
-    let g = Gen.of_list l in \
-    of_gen g |> to_gen |> Gen.to_list = l)
-*)
-
-(** {2 IO} *)
-
-type 'a printer = Format.formatter -> 'a -> unit
-
-let print ?(start = "[|") ?(stop = "|]") ?(sep = ";") pp_item out a =
-  Format.pp_print_string out start;
-  for k = 0 to Array.length a - 1 do
-    if k > 0 then (
-      Format.pp_print_string out sep;
-      Format.pp_print_cut out ()
-    );
-    pp_item out a.(k)
-  done;
-  Format.pp_print_string out stop;
-  ()
-
-(** {2 Binary} *)
-
-let equal = CCArray.equal
-let compare = CCArray.compare
-let for_all2 = CCArray.for_all2
-let exists2 = CCArray.exists2
-
-let map2 f a b =
-  if length a <> length b then invalid_arg "map2";
-  init (length a) (fun i -> f (unsafe_get a i) (unsafe_get b i))
-
-let iter2 f a b =
-  if length a <> length b then invalid_arg "iter2";
-  for i = 0 to length a - 1 do
-    f (unsafe_get a i) (unsafe_get b i)
-  done
-
-let iteri2 f a b =
-  if length a <> length b then invalid_arg "iteri2";
-  for i = 0 to length a - 1 do
-    f i (unsafe_get a i) (unsafe_get b i)
-  done
-
-let fold2 f acc a b =
-  if length a <> length b then invalid_arg "fold2";
-  let rec aux acc i =
-    if i = length a then
-      acc
-    else (
-      let acc = f acc (unsafe_get a i) (unsafe_get b i) in
-      aux acc (i + 1)
-    )
-  in
-  aux acc 0
diff --git a/src/util/IArray.mli b/src/util/IArray.mli
deleted file mode 100644
index 60015ded..00000000
--- a/src/util/IArray.mli
+++ /dev/null
@@ -1,80 +0,0 @@
-(* This file is free software. See file "license" for more details. *)
-
-type 'a t = private 'a array
-(** Array of values of type 'a. The underlying type really is
-    an array, but it will never be modified.
-
-    It should be covariant but OCaml will not accept it. *)
-
-val empty : 'a t
-val is_empty : _ t -> bool
-val length : _ t -> int
-val sub : 'a t -> int -> int -> 'a t
-val singleton : 'a -> 'a t
-val doubleton : 'a -> 'a -> 'a t
-
-val make : int -> 'a -> 'a t
-(** [make n x] makes an array of [n] times [x] *)
-
-val init : int -> (int -> 'a) -> 'a t
-(** [init n f] makes the array [[| f 0; f 1; ... ; f (n-1) |]].
-    @raise Invalid_argument if [n < 0] *)
-
-val get : 'a t -> int -> 'a
-(** Access the element *)
-
-val unsafe_get : 'a t -> int -> 'a
-(** Unsafe access, not bound-checked. Use with caution *)
-
-val set : 'a t -> int -> 'a -> 'a t
-(** Copy the array and modify its copy *)
-
-val map : ('a -> 'b) -> 'a t -> 'b t
-val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t
-val append : 'a t -> 'a t -> 'a t
-val iter : ('a -> unit) -> 'a t -> unit
-val iteri : (int -> 'a -> unit) -> 'a t -> unit
-val foldi : ('a -> int -> 'b -> 'a) -> 'a -> 'b t -> 'a
-val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
-val for_all : ('a -> bool) -> 'a t -> bool
-val exists : ('a -> bool) -> 'a t -> bool
-
-(** {2 Conversions} *)
-
-type 'a iter = ('a -> unit) -> unit
-type 'a gen = unit -> 'a option
-
-val of_list : 'a list -> 'a t
-val to_list : 'a t -> 'a list
-val of_list_map : ('a -> 'b) -> 'a list -> 'b t
-val to_list_map : ('a -> 'b) -> 'a t -> 'b list
-val of_array_map : ('a -> 'b) -> 'a array -> 'b t
-val to_array_map : ('a -> 'b) -> 'a t -> 'b array
-
-val of_array_unsafe : 'a array -> 'a t
-(** Take ownership of the given array. Careful, the array must {b NOT}
-    be modified afterwards! *)
-
-val to_iter : 'a t -> 'a iter
-val to_iter_sub : 'a t -> int -> int -> 'a iter
-val of_iter : 'a iter -> 'a t
-val of_gen : 'a gen -> 'a t
-val to_gen : 'a t -> 'a gen
-
-(** {2 IO} *)
-
-type 'a printer = Format.formatter -> 'a -> unit
-
-val print :
-  ?start:string -> ?stop:string -> ?sep:string -> 'a printer -> 'a t printer
-
-(** {2 Binary} *)
-
-val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-val for_all2 : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-val exists2 : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
-val fold2 : ('acc -> 'a -> 'b -> 'acc) -> 'acc -> 'a t -> 'b t -> 'acc
-val iteri2 : (int -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
-val iter2 : ('a -> 'b -> unit) -> 'a t -> 'b t -> unit
diff --git a/src/util/Int_id.ml b/src/util/Int_id.ml
index b3e5220f..bf69dd40 100644
--- a/src/util/Int_id.ml
+++ b/src/util/Int_id.ml
@@ -1,3 +1,5 @@
+(** Integer-based identifiers. *)
+
 module type S = sig
   type t = private int
 
@@ -8,6 +10,7 @@ module type S = sig
   val of_int_unsafe : int -> t
 end
 
+(** Generate a new type for integer identifiers *)
 module Make () = struct
   type t = int
 
diff --git a/src/util/Profile.mli b/src/util/Profile.mli
index 5cf668ed..e1e0e054 100644
--- a/src/util/Profile.mli
+++ b/src/util/Profile.mli
@@ -1,4 +1,8 @@
-(** {1 Profiling probes} *)
+(** Profiling probes.
+
+   This basic library can produce Catapult traces (a json file)
+   that can be read at [http://ui.perfetto.dev].
+ *)
 
 type probe
 
diff --git a/src/util/Util.ml b/src/util/Util.ml
index 7ff98d7e..8edc454f 100644
--- a/src/util/Util.ml
+++ b/src/util/Util.ml
@@ -14,11 +14,14 @@ let pp_pair ?(sep = " ") pp1 pp2 out t =
   Fmt.pair ~sep:(pp_sep sep) pp1 pp2 out t
 
 let pp_array ?(sep = " ") pp out l = Fmt.array ~sep:(pp_sep sep) pp out l
+let flat_map_l_arr f l = CCList.flat_map (fun x -> CCArray.to_list @@ f x) l
 
-let pp_iarray ?(sep = " ") pp out a =
-  Fmt.iter ~sep:(pp_sep sep) pp out (IArray.to_iter a)
-
-let flat_map_l_ia f l = CCList.flat_map (fun x -> IArray.to_list @@ f x) l
+let array_iteri2 ~f a b =
+  let open Array in
+  if length a <> length b then invalid_arg "iteri2";
+  for i = 0 to length a - 1 do
+    f i (unsafe_get a i) (unsafe_get b i)
+  done
 
 let array_of_list_map f l =
   match l with
diff --git a/src/util/Util.mli b/src/util/Util.mli
index b301b1e2..6ef63b4e 100644
--- a/src/util/Util.mli
+++ b/src/util/Util.mli
@@ -8,11 +8,7 @@ val pp_list : ?sep:string -> 'a printer -> 'a list printer
 val pp_iter : ?sep:string -> 'a printer -> 'a Iter.t printer
 val pp_array : ?sep:string -> 'a printer -> 'a array printer
 val pp_pair : ?sep:string -> 'a printer -> 'b printer -> ('a * 'b) printer
-
-val pp_iarray :
-  ?sep:string -> 'a CCFormat.printer -> 'a IArray.t CCFormat.printer
-
-val flat_map_l_ia : ('a -> 'b IArray.t) -> 'a list -> 'b list
+val flat_map_l_arr : ('a -> 'b array) -> 'a list -> 'b list
 
 val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
 (** [array_of_list_map f l] is the same as [Array.of_list @@ List.map f l] *)
@@ -20,6 +16,7 @@ val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
 val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
 val lazy_map : ('a -> 'b) -> 'a lazy_t -> 'b lazy_t
 val lazy_map2 : ('a -> 'b -> 'c) -> 'a lazy_t -> 'b lazy_t -> 'c lazy_t
+val array_iteri2 : f:(int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
 
 val setup_gc : unit -> unit
 (** Change parameters of the GC *)
diff --git a/src/util/Vec_unit.mli b/src/util/Vec_unit.mli
index 94afb4aa..abda0bf9 100644
--- a/src/util/Vec_unit.mli
+++ b/src/util/Vec_unit.mli
@@ -1 +1,5 @@
+(** Fake vector of unit.
+
+  This just retains the size, as 0 bits of actual storage are required. *)
+
 include Vec_sig.S with type elt = unit