diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 8dba904e1..332723172 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -281,10 +281,12 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     let mangle r =
       Llair.Reg.mk (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
     in
-    let args = List.combine_exn formals actuals in
-    let q' = List.fold ~f:(fun (f, a) q -> assign (mangle f) a q) args q in
+    let args = IArray.combine_exn formals actuals in
+    let q' =
+      IArray.fold ~f:(fun (f, a) q -> assign (mangle f) a q) args q
+    in
     let callee_env =
-      List.fold formals ([], []) ~f:(fun f (is, fs) ->
+      IArray.fold formals ([], []) ~f:(fun f (is, fs) ->
           match apron_typ_of_llair_typ (Llair.Reg.typ f) with
           | None -> (is, fs)
           | Some Texpr1.Int -> (apron_var_of_reg (mangle f) :: is, fs)
@@ -296,8 +298,10 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     let q'' = Abstract1.change_environment man q' callee_env false in
     let q''' =
       Abstract1.rename_array man q''
-        (Array.map ~f:(mangle >> apron_var_of_reg) (Array.of_list formals))
-        (Array.map ~f:apron_var_of_reg (Array.of_list formals))
+        (Array.map
+           ~f:(mangle >> apron_var_of_reg)
+           (IArray.to_array formals))
+        (Array.map ~f:apron_var_of_reg (IArray.to_array formals))
     in
     (q''', {areturn; caller_q= q})
 
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index e698e3e26..4dcd8e1d8 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -441,13 +441,12 @@ let rec xlate_intrinsic_exp :
   | _ -> None
 
 and xlate_values x len val_i =
-  let rec loop i (pre, args) =
-    if i < 0 then (pre, args)
-    else
-      let pre_i, arg_i = xlate_value x (val_i i) in
-      loop (i - 1) (pre_i @ pre, arg_i :: args)
+  let xlate_i j pre_0_i =
+    let pre_j, arg_j = xlate_value x (val_i j) in
+    (arg_j, Iter.append pre_0_i (Iter.of_list pre_j))
   in
-  loop (len - 1) ([], [])
+  let pre, vals = Iter.(fold_map (0 -- (len - 1)) empty ~f:xlate_i) in
+  (Iter.to_list pre, IArray.of_iter vals)
 
 and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
     =
@@ -485,22 +484,22 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.num_operands llv in
         let pre, args = xlate_values x len (Llvm.operand llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | ConstantDataVector ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.vector_size (Llvm.type_of llv) in
         let pre, args = xlate_values x len (Llvm.const_element llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | ConstantDataArray ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.array_length (Llvm.type_of llv) in
         let pre, args = xlate_values x len (Llvm.const_element llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | ConstantStruct ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.num_operands llv in
         let pre, args = xlate_values x len (Llvm.operand llv) in
-        (pre, Exp.record typ (IArray.of_list args))
+        (pre, Exp.record typ args)
     | BlockAddress ->
         let parent = find_name (Llvm.operand llv 0) in
         let name = find_name (Llvm.operand llv 1) in
@@ -1446,9 +1445,9 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
   let typ = xlate_type x (Llvm.type_of llf) in
   let name = Function.mk typ (find_name llf) in
   let formals =
-    Llvm.fold_left_params
-      (fun rev_args param -> xlate_name x param :: rev_args)
-      [] llf
+    Iter.from_iter (fun f -> Llvm.iter_params f llf)
+    |> Iter.map ~f:(xlate_name x)
+    |> IArray.of_iter
   in
   let freturn =
     match typ with
diff --git a/sledge/nonstdlib/array.ml b/sledge/nonstdlib/array.ml
index 57be2e838..282e6b861 100644
--- a/sledge/nonstdlib/array.ml
+++ b/sledge/nonstdlib/array.ml
@@ -12,6 +12,7 @@ include Array
 type 'a t = 'a array [@@deriving compare, equal, sexp]
 
 let of_ x = [|x|]
+let of_iter = Iter.to_array
 
 let of_list_rev = function
   | [] -> [||]
@@ -101,5 +102,6 @@ let fold_map_until xs s ~f ~finish =
         fold_map_until_ s 1
 
 let for_all2_exn xs ys ~f = for_all2 ~f xs ys
+let fold2_exn xs ys init ~f = fold2 ~f:(fun s x y -> f x y s) ~init xs ys
 let to_list_rev_map xs ~f = fold ~f:(fun x ys -> f x :: ys) xs []
 let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
diff --git a/sledge/nonstdlib/array.mli b/sledge/nonstdlib/array.mli
index dfeb69667..06fc28d8c 100644
--- a/sledge/nonstdlib/array.mli
+++ b/sledge/nonstdlib/array.mli
@@ -11,6 +11,7 @@ include module type of ContainersLabels.Array
 type 'a t = 'a array [@@deriving compare, equal, sexp]
 
 val of_ : 'a -> 'a t
+val of_iter : 'a iter -> 'a t
 val of_list_rev : 'a list -> 'a t
 val map : 'a t -> f:('a -> 'b) -> 'b t
 val mapi : 'a t -> f:(int -> 'a -> 'b) -> 'b t
@@ -41,5 +42,6 @@ val fold_map_until :
   -> finish:('b t * 's -> 'c)
   -> 'c
 
+val fold2_exn : 'a t -> 'b t -> 's -> f:('a -> 'b -> 's -> 's) -> 's
 val to_list_rev_map : 'a array -> f:('a -> 'b) -> 'b list
 val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
diff --git a/sledge/nonstdlib/iArray.mli b/sledge/nonstdlib/iArray.mli
index f08db3781..1b0524d77 100644
--- a/sledge/nonstdlib/iArray.mli
+++ b/sledge/nonstdlib/iArray.mli
@@ -35,6 +35,7 @@ val of_array : 'a array -> 'a t
 
 val empty : 'a t
 val of_ : 'a -> 'a t
+val of_iter : 'a iter -> 'a t
 val of_list : 'a list -> 'a t
 val of_list_rev : 'a list -> 'a t
 val init : int -> f:(int -> 'a) -> 'a t
@@ -49,6 +50,8 @@ val map_endo : 'a t -> f:('a -> 'a) -> 'a t
 
 val reduce_adjacent : 'a t -> f:('a -> 'a -> 'a option) -> 'a t
 val split : ('a * 'b) t -> 'a t * 'b t
+val combine : 'a t -> 'b t -> ('a * 'b) t option
+val combine_exn : 'a t -> 'b t -> ('a * 'b) t
 val is_empty : 'a t -> bool
 val length : 'a t -> int
 val get : 'a t -> int -> 'a
@@ -68,3 +71,5 @@ val fold_map_until :
   -> f:('a -> 's -> [`Continue of 'b * 's | `Stop of 'c])
   -> finish:('b t * 's -> 'c)
   -> 'c
+
+val fold2_exn : 'a t -> 'b t -> 's -> f:('a -> 'b -> 's -> 's) -> 's
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 596c63ed7..87d250005 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -32,7 +32,7 @@ module Make (Dom : Domain_intf.Dom) = struct
          t
       -> 'a
       -> unwind:
-           (   Llair.Reg.t list
+           (   Llair.Reg.t iarray
             -> Llair.Reg.Set.t
             -> Dom.from_call
             -> 'a
@@ -43,7 +43,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       | Return of
           { recursive: bool  (** return from a possibly-recursive call *)
           ; dst: Llair.Jump.t
-          ; formals: Llair.Reg.t list
+          ; formals: Llair.Reg.t iarray
           ; locals: Llair.Reg.Set.t
           ; from_call: Dom.from_call
           ; stk: t }
@@ -491,15 +491,16 @@ module Make (Dom : Domain_intf.Dom) = struct
       ~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions)
       opts.entry_points
     |> function
-    | Some {name; formals= []; freturn; locals; entry} ->
+    | Some {name; formals; freturn; locals; entry}
+      when IArray.is_empty formals ->
         Some
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
                    ~globals:
                      (Domain_used_globals.by_function opts.globals name)
-                   ~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
-                   (Dom.init pgm.globals)))
+                   ~actuals:IArray.empty ~areturn:None ~formals:IArray.empty
+                   ~freturn ~locals (Dom.init pgm.globals)))
              entry)
     | _ -> None
 
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index b403e369a..0a3bb8bd5 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -24,7 +24,7 @@ module type Dom = sig
        skip_throw:bool
     -> Llair.Reg.t option
     -> Llair.Function.t
-    -> Llair.Exp.t list
+    -> Llair.Exp.t iarray
     -> t
     -> t option option
 
@@ -33,16 +33,16 @@ module type Dom = sig
   val call :
        summaries:bool
     -> globals:Llair.Global.Set.t
-    -> actuals:Llair.Exp.t list
+    -> actuals:Llair.Exp.t iarray
     -> areturn:Llair.Reg.t option
-    -> formals:Llair.Reg.t list
+    -> formals:Llair.Reg.t iarray
     -> freturn:Llair.Reg.t option
     -> locals:Llair.Reg.Set.t
     -> t
     -> t * from_call
 
   val post : Llair.Reg.Set.t -> from_call -> t -> t
-  val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t
+  val retn : Llair.Reg.t iarray -> Llair.Reg.t option -> from_call -> t -> t
 
   val resolve_callee :
        (Llair.Function.t -> Llair.func list)
@@ -57,7 +57,7 @@ module type Dom = sig
   val pp_summary : summary pp
 
   val create_summary :
-    locals:Llair.Reg.Set.t -> formals:Llair.Reg.t list -> t -> summary * t
+    locals:Llair.Reg.Set.t -> formals:Llair.Reg.t iarray -> t -> summary * t
 
   val apply_summary : t -> summary -> t option
 end
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index 94702c3a2..94e73b254 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -13,7 +13,7 @@ module type State_domain_sig = sig
 
   val create_summary :
        locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.t list
+    -> formals:Llair.Reg.t iarray
     -> entry:t
     -> current:t
     -> summary * t
@@ -76,11 +76,11 @@ module Make (State_domain : State_domain_sig) = struct
       pf
         "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
          globals: {@[%a@]}@ current: %a@]"
-        (List.pp ",@ " Llair.Exp.pp)
-        (List.rev actuals)
-        (List.pp ",@ " Llair.Reg.pp)
-        (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp
-        globals State_domain.pp current]
+        (IArray.pp ",@ " Llair.Exp.pp)
+        actuals
+        (IArray.pp ",@ " Llair.Reg.pp)
+        formals Llair.Reg.Set.pp locals Llair.Global.Set.pp globals
+        State_domain.pp current]
     ;
     let caller_current, state_from_call =
       State_domain.call ~summaries ~globals ~actuals ~areturn ~formals
diff --git a/sledge/src/domain_relation.mli b/sledge/src/domain_relation.mli
index e48f08586..6b703451b 100644
--- a/sledge/src/domain_relation.mli
+++ b/sledge/src/domain_relation.mli
@@ -13,7 +13,7 @@ module type State_domain_sig = sig
 
   val create_summary :
        locals:Llair.Reg.Set.t
-    -> formals:Llair.Reg.t list
+    -> formals:Llair.Reg.t iarray
     -> entry:t
     -> current:t
     -> summary * t
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 85e214ac9..c687772a4 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -75,7 +75,7 @@ let exec_inst inst pre =
 
 let exec_intrinsic ~skip_throw r i es q =
   Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r)
-    (Llair.Function.name i) (List.map ~f:X.term es)
+    (Llair.Function.name i) (IArray.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
 let value_determined_by ctx us a =
@@ -110,17 +110,17 @@ let and_eqs sub formals actuals q =
     let actual' = Term.rename sub actual in
     Sh.and_ (Formula.eq (Term.var formal) actual') q
   in
-  List.fold2_exn ~f:and_eq formals actuals q
+  IArray.fold2_exn ~f:and_eq formals actuals q
 
 let localize_entry globals actuals formals freturn locals shadow pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
-  let formals_set = Var.Set.of_list formals in
+  let formals_set = Var.Set.of_iter (IArray.to_iter formals) in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let wrt =
     Term.Set.of_iter
       (Iter.append
          (Iter.map ~f:X.global (Llair.Global.Set.to_iter globals))
-         (Iter.map ~f:Term.var (List.to_iter formals)))
+         (Iter.map ~f:Term.var (IArray.to_iter formals)))
   in
   let function_summary_pre = garbage_collect entry ~wrt in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
@@ -147,32 +147,30 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
        globals: {@[%a@]}@ q: %a@]"
-      (List.pp ",@ " Llair.Exp.pp)
-      (List.rev actuals)
-      (List.pp ",@ " Llair.Reg.pp)
-      (List.rev formals) Llair.Reg.Set.pp locals Llair.Global.Set.pp globals
-      pp q]
+      (IArray.pp ",@ " Llair.Exp.pp)
+      actuals
+      (IArray.pp ",@ " Llair.Reg.pp)
+      formals Llair.Reg.Set.pp locals Llair.Global.Set.pp globals pp q]
   ;
-  let actuals = List.map ~f:X.term actuals in
+  let actuals = IArray.map ~f:X.term actuals in
   let areturn = Option.map ~f:X.reg areturn in
-  let formals = List.map ~f:X.reg formals in
+  let formals = IArray.map ~f:X.reg formals in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
   let modifs = Var.Set.of_option areturn in
   (* quantify modifs, their current value will be overwritten and so does
      not need to be saved in the freshening renaming *)
   let q = Sh.exists modifs q in
   (* save current values of shadowed formals and locals with a renaming *)
-  let q', shadow =
-    Sh.freshen q ~wrt:(Var.Set.add_list formals freturn_locals)
+  let formals_freturn_locals =
+    Iter.fold ~f:Var.Set.add (IArray.to_iter formals) freturn_locals
   in
+  let q', shadow = Sh.freshen q ~wrt:formals_freturn_locals in
   let unshadow = Var.Subst.invert shadow in
   assert (Var.Set.disjoint modifs (Var.Subst.domain shadow)) ;
   (* pass arguments by conjoining equations between formals and actuals *)
   let entry = and_eqs shadow formals actuals q' in
   (* note: locals and formals are in scope *)
-  assert (
-    Var.Set.subset (Var.Set.add_list formals freturn_locals) ~of_:entry.us
-  ) ;
+  assert (Var.Set.subset formals_freturn_locals ~of_:entry.us) ;
   (* simplify *)
   let entry = simplify entry in
   ( if not summaries then (entry, {areturn; unshadow; frame= Sh.emp})
@@ -201,14 +199,16 @@ let post locals _ q =
 let retn formals freturn {areturn; unshadow; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}%a%a@ unshadow: %a@ q: %a@ frame: %a@]"
-      (List.pp ", " Llair.Reg.pp)
+      (IArray.pp ", " Llair.Reg.pp)
       formals
       (Option.pp "@ freturn: %a" Llair.Reg.pp)
       freturn
       (Option.pp "@ areturn: %a" Var.pp)
       areturn Var.Subst.pp unshadow pp q pp frame]
   ;
-  let formals = List.map ~f:X.reg formals in
+  let formals =
+    Var.Set.of_iter (Iter.map ~f:X.reg (IArray.to_iter formals))
+  in
   let freturn = Option.map ~f:X.reg freturn in
   let q =
     match areturn with
@@ -223,9 +223,7 @@ let retn formals freturn {areturn; unshadow; frame} q =
     | None -> q
   in
   (* exit scope of formals *)
-  let q =
-    Sh.exists (Var.Set.add_list formals (Var.Set.of_option freturn)) q
-  in
+  let q = Sh.exists (Var.Set.union formals (Var.Set.of_option freturn)) q in
   (* reinstate shadowed values of locals *)
   let q = Sh.rename unshadow q in
   (* reconjoin frame *)
@@ -251,11 +249,11 @@ let pp_summary fs {xs; foot; post} =
 let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
     pf "formals %a@ entry: %a@ current: %a"
-      (List.pp ",@ " Llair.Reg.pp)
+      (IArray.pp ",@ " Llair.Reg.pp)
       formals pp entry pp post]
   ;
   let formals =
-    Var.Set.of_iter (Iter.map ~f:X.reg (List.to_iter formals))
+    Var.Set.of_iter (Iter.map ~f:X.reg (IArray.to_iter formals))
   in
   let locals = X.regs locals in
   let foot = Sh.exists locals entry in
diff --git a/sledge/src/domain_sh.mli b/sledge/src/domain_sh.mli
index aa99c8b39..65fb074a0 100644
--- a/sledge/src/domain_sh.mli
+++ b/sledge/src/domain_sh.mli
@@ -11,7 +11,7 @@ include Domain_intf.Dom
 
 val create_summary :
      locals:Llair.Reg.Set.t
-  -> formals:Llair.Reg.t list
+  -> formals:Llair.Reg.t iarray
   -> entry:t
   -> current:t
   -> summary * t
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 1e23b9f4b..32a16e7c9 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -70,7 +70,7 @@ let exec_intrinsic ~skip_throw:_ _ intrinsic actuals st =
       ; "__cxa_allocate_exception"
       ; "_ZN5folly13usingJEMallocEv" ]
       ~f:(String.equal name)
-  then List.fold ~f:used_globals actuals st |> fun res -> Some (Some res)
+  then IArray.fold ~f:used_globals actuals st |> fun res -> Some (Some res)
   else None
 
 type from_call = t [@@deriving sexp]
@@ -78,7 +78,7 @@ type from_call = t [@@deriving sexp]
 (* Set abstract state to bottom (i.e. empty set) at function entry *)
 let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
     ~locals:_ st =
-  (empty, List.fold ~f:used_globals actuals st)
+  (empty, IArray.fold ~f:used_globals actuals st)
 
 let resolve_callee lookup ptr st =
   let st = used_globals ptr st in
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 71f9f99e1..f85f260e6 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -738,7 +738,7 @@ let nondet pre = function Some reg -> kill pre reg | None -> pre
 let abort _ = None
 
 let intrinsic ~skip_throw :
-    Sh.t -> Var.t option -> string -> Term.t list -> Sh.t option option =
+    Sh.t -> Var.t option -> string -> Term.t iarray -> Sh.t option option =
  fun pre areturn intrinsic actuals ->
   let name =
     match String.index intrinsic '.' with
@@ -746,60 +746,60 @@ let intrinsic ~skip_throw :
     | Some i -> String.take i intrinsic
   in
   let skip pre = Some (Some pre) in
-  ( match (areturn, name, actuals) with
+  ( match (areturn, name, IArray.to_array actuals) with
   (*
    * cstdlib - memory management
    *)
   (* void* malloc(size_t size) *)
-  | Some reg, "malloc", [size]
+  | Some reg, "malloc", [|size|]
   (* void* aligned_alloc(size_t alignment, size_t size) *)
-   |Some reg, "aligned_alloc", [size; _] ->
+   |Some reg, "aligned_alloc", [|_; size|] ->
       Some (exec_spec pre (malloc_spec reg size))
   (* void* calloc(size_t number, size_t size) *)
-  | Some reg, "calloc", [size; number] ->
+  | Some reg, "calloc", [|number; size|] ->
       Some (exec_spec pre (calloc_spec reg number size))
   (* int posix_memalign(void** ptr, size_t alignment, size_t size) *)
-  | Some reg, "posix_memalign", [size; _; ptr] ->
+  | Some reg, "posix_memalign", [|ptr; _; size|] ->
       Some (exec_spec pre (posix_memalign_spec reg ptr size))
   (* void* realloc(void* ptr, size_t size) *)
-  | Some reg, "realloc", [size; ptr] ->
+  | Some reg, "realloc", [|ptr; size|] ->
       Some (exec_spec pre (realloc_spec reg ptr size))
   (*
    * jemalloc - non-standard API
    *)
   (* void* mallocx(size_t size, int flags) *)
-  | Some reg, "mallocx", [_; size] ->
+  | Some reg, "mallocx", [|size; _|] ->
       Some (exec_spec pre (mallocx_spec reg size))
   (* void* rallocx(void* ptr, size_t size, int flags) *)
-  | Some reg, "rallocx", [_; size; ptr] ->
+  | Some reg, "rallocx", [|ptr; size; _|] ->
       Some (exec_spec pre (rallocx_spec reg ptr size))
   (* size_t xallocx(void* ptr, size_t size, size_t extra, int flags) *)
-  | Some reg, "xallocx", [_; extra; size; ptr] ->
+  | Some reg, "xallocx", [|ptr; size; extra; _|] ->
       Some (exec_spec pre (xallocx_spec reg ptr size extra))
   (* size_t sallocx(void* ptr, int flags) *)
-  | Some reg, "sallocx", [_; ptr] ->
+  | Some reg, "sallocx", [|ptr; _|] ->
       Some (exec_spec pre (sallocx_spec reg ptr))
   (* void dallocx(void* ptr, int flags) *)
-  | None, "dallocx", [_; ptr]
+  | None, "dallocx", [|ptr; _|]
   (* void sdallocx(void* ptr, size_t size, int flags) *)
-   |None, "sdallocx", [_; _; ptr] ->
+   |None, "sdallocx", [|ptr; _; _|] ->
       Some (exec_spec pre (dallocx_spec ptr))
   (* size_t nallocx(size_t size, int flags) *)
-  | Some reg, "nallocx", [_; size] ->
+  | Some reg, "nallocx", [|size; _|] ->
       Some (exec_spec pre (nallocx_spec reg size))
   (* size_t malloc_usable_size(void* ptr) *)
-  | Some reg, "malloc_usable_size", [ptr] ->
+  | Some reg, "malloc_usable_size", [|ptr|] ->
       Some (exec_spec pre (malloc_usable_size_spec reg ptr))
   (* int mallctl(const char* name, void* oldp, size_t* oldlenp, void* newp,
      size_t newlen) *)
-  | Some _, "mallctl", [newlen; newp; oldlenp; oldp; _] ->
+  | Some _, "mallctl", [|_; oldp; oldlenp; newp; newlen|] ->
       Some (exec_specs pre (mallctl_specs oldp oldlenp newp newlen))
   (* int mallctlnametomib(const char* name, size_t* mibp, size_t* miblenp) *)
-  | Some _, "mallctlnametomib", [miblenp; mibp; _] ->
+  | Some _, "mallctlnametomib", [|_; mibp; miblenp|] ->
       Some (exec_spec pre (mallctlnametomib_spec mibp miblenp))
   (* int mallctlbymib(const size_t* mib, size_t miblen, void* oldp, size_t*
      oldlenp, void* newp, size_t newlen); *)
-  | Some _, "mallctlbymib", [newlen; newp; oldlenp; oldp; miblen; mib] ->
+  | Some _, "mallctlbymib", [|mib; miblen; oldp; oldlenp; newp; newlen|] ->
       Some
         (exec_specs pre
            (mallctlbymib_specs mib miblen oldp oldlenp newp newlen))
@@ -808,17 +808,18 @@ let intrinsic ~skip_throw :
    * cstring
    *)
   (* size_t strlen (const char* ptr) *)
-  | Some reg, "strlen", [ptr] -> Some (exec_spec pre (strlen_spec reg ptr))
+  | Some reg, "strlen", [|ptr|] ->
+      Some (exec_spec pre (strlen_spec reg ptr))
   (*
    * cxxabi
    *)
-  | Some _, "__cxa_allocate_exception", [_] when skip_throw ->
+  | Some _, "__cxa_allocate_exception", [|_|] when skip_throw ->
       skip (Sh.false_ pre.us)
   (*
    * folly
    *)
   (* bool folly::usingJEMalloc() *)
-  | Some _, "_ZN5folly13usingJEMallocEv", [] -> skip pre
+  | Some _, "_ZN5folly13usingJEMallocEv", [||] -> skip pre
   | _ -> None )
   $> function
   | None -> ()
@@ -826,5 +827,4 @@ let intrinsic ~skip_throw :
       [%Trace.info
         "@[<2>exec intrinsic@ @[%a%s(@[%a@])@] from@ @[{ %a@ }@]@]"
           (Option.pp "%a := " Var.pp)
-          areturn intrinsic (List.pp ",@ " Term.pp) (List.rev actuals) Sh.pp
-          pre]
+          areturn intrinsic (IArray.pp ",@ " Term.pp) actuals Sh.pp pre]
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index 578ad571b..7dc2258fa 100644
--- a/sledge/src/exec.mli
+++ b/sledge/src/exec.mli
@@ -27,5 +27,5 @@ val intrinsic :
   -> Sh.t
   -> Var.t option
   -> string
-  -> Term.t list
+  -> Term.t iarray
   -> Sh.t option option
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index bb8504c37..f549a1506 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -38,7 +38,7 @@ type jump = {mutable dst: block; mutable retreating: bool}
 and 'a call =
   { callee: 'a
   ; typ: Typ.t
-  ; actuals: Exp.t list
+  ; actuals: Exp.t iarray
   ; areturn: Reg.t option
   ; return: jump
   ; throw: jump option
@@ -62,7 +62,7 @@ and block =
 
 and func =
   { name: Function.t
-  ; formals: Reg.t list
+  ; formals: Reg.t iarray
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t
@@ -97,7 +97,7 @@ with type jump := jump
   type nonrec 'a call = 'a call =
     { callee: 'a
     ; typ: Typ.t
-    ; actuals: Exp.t list
+    ; actuals: Exp.t iarray
     ; areturn: Reg.t option
     ; return: jump
     ; throw: jump option
@@ -143,7 +143,7 @@ let hash_fold_term s = function
       let s = [%hash_fold: int] s 3 in
       let s = [%hash_fold: Exp.t] s callee in
       let s = [%hash_fold: Typ.t] s typ in
-      let s = [%hash_fold: Exp.t list] s actuals in
+      let s = [%hash_fold: Exp.t iarray] s actuals in
       let s = [%hash_fold: Reg.t option] s areturn in
       let s = [%hash_fold: jump] s return in
       let s = [%hash_fold: jump option] s throw in
@@ -191,7 +191,7 @@ let sexp_of_term = function
         [%sexp
           { callee: Exp.t
           ; typ: Typ.t
-          ; actuals: Exp.t list
+          ; actuals: Exp.t iarray
           ; areturn: Reg.t option
           ; return: jump
           ; throw: jump option
@@ -213,7 +213,7 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
 let sexp_of_func {name; formals; freturn; fthrow; locals; entry; loc} =
   [%sexp
     { name: Function.t
-    ; formals: Reg.t list
+    ; formals: Reg.t iarray
     ; freturn: Reg.t option
     ; fthrow: Reg.t
     ; locals: Reg.Set.t
@@ -260,8 +260,7 @@ let pp_inst fs inst =
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
 
 let pp_actuals pp_actual fs actuals =
-  Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_actual)
-    (List.rev actuals)
+  Format.fprintf fs "@ (@[%a@])" (IArray.pp ",@ " pp_actual) actuals
 
 let pp_formal fs reg = Reg.pp fs reg
 
@@ -325,7 +324,7 @@ and dummy_func =
       Function.mk
         (Typ.pointer ~elt:(Typ.function_ ~args:IArray.empty ~return:None))
         "dummy"
-  ; formals= []
+  ; formals= IArray.empty
   ; freturn= None
   ; fthrow= Reg.mk Typ.ptr "dummy"
   ; locals= Reg.Set.empty
@@ -425,7 +424,7 @@ module Term = struct
     | Call {typ; actuals; areturn; _} -> (
       match typ with
       | Pointer {elt= Function {args; return= retn_typ; _}} ->
-          assert (IArray.length args = List.length actuals) ;
+          assert (IArray.length args = IArray.length actuals) ;
           assert (Option.is_some retn_typ || Option.is_none areturn)
       | _ -> assert false )
     | Return {exp; _} -> (
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 479bbcbeb..7b54458b1 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -56,7 +56,7 @@ type jump = {mutable dst: block; mutable retreating: bool}
 and 'a call =
   { callee: 'a
   ; typ: Typ.t  (** Type of the callee. *)
-  ; actuals: Exp.t list  (** Stack of arguments, first-arg-last. *)
+  ; actuals: Exp.t iarray  (** Actual arguments. *)
   ; areturn: Reg.t option  (** Register to receive return value. *)
   ; return: jump  (** Return destination. *)
   ; throw: jump option  (** Handler destination. *)
@@ -95,7 +95,7 @@ and block = private
     parameters are the function parameters. *)
 and func = private
   { name: Function.t
-  ; formals: Reg.t list  (** Formal parameters, first-param-last stack *)
+  ; formals: Reg.t iarray  (** Formal parameters *)
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t  (** Local registers *)
@@ -155,7 +155,7 @@ module Term : sig
   val call :
        callee:Exp.t
     -> typ:Typ.t
-    -> actuals:Exp.t list
+    -> actuals:Exp.t iarray
     -> areturn:Reg.t option
     -> return:jump
     -> throw:jump option
@@ -188,7 +188,7 @@ module Func : sig
 
   val mk :
        name:Function.t
-    -> formals:Reg.t list
+    -> formals:Reg.t iarray
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> entry:block
@@ -198,7 +198,7 @@ module Func : sig
 
   val mk_undefined :
        name:Function.t
-    -> formals:Reg.t list
+    -> formals:Reg.t iarray
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> loc:Loc.t