diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index 5e251eb6c06..9d705747381 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -26,6 +26,8 @@ let rec pp_prog ppf p =
 
 and pp_item ppf i =
   match i.it with
+  | ImportI id ->
+     fprintf ppf "@[<2>import \"%s\"@]" id.it
   | FieldI (id, typ) ->
     fprintf ppf "@[<2>field %s:@ %a@]"
       id.it
@@ -87,11 +89,13 @@ and pp_returns ppf pars =
     fprintf ppf "@[<1> returns (%a)@]"
       (pp_print_list ~pp_sep:comma (pp_local)) pars
 
-and pp_typ ppf t =
-  match t.it with
+and pp_typ ppf t = pp_typ' ppf t.it
+and pp_typ' ppf t =
+  match t with
   | IntT -> pr ppf "Int"
   | BoolT -> pr ppf "Bool"
   | RefT -> pr ppf "Ref"
+  | ArrayT (_, t) -> fprintf ppf "Array"
 
 and pp_exp ppf exp =
   match exp.it with
@@ -99,8 +103,12 @@ and pp_exp ppf exp =
      fprintf ppf "%s" id.it
   | FldAcc fldacc ->
      pp_fldacc ppf fldacc
-  | MacroCall (m, e) ->
-     fprintf ppf "@[%s(%a)@]" m pp_exp e
+  | MacroArg id ->
+     fprintf ppf "%s" id.it
+  | MacroCall (m, es) ->
+     fprintf ppf "@[%s(%a)@]" m (pp_print_list pp_exp ~pp_sep:comma) es
+  | FuncCall (id, es) ->
+     fprintf ppf "@[%s(%a)@]" id (pp_print_list pp_exp ~pp_sep:comma) es
   | NotE e ->
      fprintf ppf "@[(!%a)@]" pp_exp e
   | MinusE e ->
diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml
index 3c4517c4986..042ba5ea4f6 100644
--- a/src/viper/syntax.ml
+++ b/src/viper/syntax.ml
@@ -10,7 +10,7 @@ type prog = (item list, info) Source.annotated_phrase
 
 and item = (item', info) Source.annotated_phrase
 and item' =
-  (* | import path *)
+  | ImportI of id
   | FieldI of id * typ
   | MethodI of id * par list * par list * exp list * exp list * seqn option
   | InvariantI of string * exp
@@ -49,7 +49,9 @@ and exp' =
   | FldAcc of fldacc
   | PermE of perm          (* perm_amount *)
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
-  | MacroCall of string * exp
+  | MacroCall of string * exp list
+  | MacroArg of id         (* untyped macro argument e.g. "macro(a, f) { a.f }" *)
+  | FuncCall of string * exp list
 
 and perm = (perm', info) Source.annotated_phrase
 
@@ -90,8 +92,21 @@ and stmt' =
 
 and typ = (typ', info) Source.annotated_phrase
 
+
+and mut = Const | Mut
+
 and typ' =
   | IntT
   | BoolT
   | RefT
+  | ArrayT of mut * typ'
+
+let type_field = function
+  | IntT -> "int"
+  | BoolT -> "bool"
+  | RefT -> "ref"
+  | ArrayT _ -> "array" (* TODO *)
 
+let inner_type = function
+  | Source.{it=ArrayT (k, t); _} -> t
+  | Source.{it=t; _} -> t
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index 562e9dfd2cf..361e75510a6 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -62,6 +62,42 @@ exception Unsupported of Source.region * string
 let unsupported at sexp =
   raise (Unsupported (at, (Wasm.Sexpr.to_string 80 sexp)))
 
+let array_acc id_exp (kind, typ) at =
+     let (!!) p = !!! at p in
+     let fld = type_field typ in
+     let pred_name = match kind with | Mut -> "array_acc_mut" | Const -> "array_acc" in
+     !! (MacroCall (pred_name, [id_exp; !!(MacroArg !!fld)]))
+
+let array_size id_exp at =
+  !!! at (FuncCall ("size", [id_exp]))
+
+let array_size_inv id_exp n at =
+  !!! at (EqCmpE (array_size id_exp at, intLitE at n))
+
+let array_alloc id_exp typ es at =
+  match typ.it with
+  | ArrayT (kind, typ) ->
+     let (!!) p = !!! at p in
+     let ref_field = !! (type_field typ) in
+     let init_array = List.mapi (fun i e ->
+       FieldAssignS ((!! (FuncCall ("loc", [id_exp; intLitE at i])), ref_field), e)) es in
+     (* InhaleS (!! (FldAcc (!! (FuncCall ("loc", [var; from_int i])), ref_field)) === e)) es in *)
+     let stmt =  [ InhaleS (array_acc id_exp (Mut, typ) at)
+                 ; InhaleS (array_size_inv id_exp (List.length es) at)
+                 ] @ init_array @ [
+                   ExhaleS (array_acc id_exp (Mut, typ) at)
+                 ; InhaleS (array_acc id_exp (kind, typ) at)]
+     in List.map (!!) stmt
+| _ -> []
+
+(* map type to predicate *)
+let type_acc id typ at =
+  let id_exp = !!! at (LocalVar (id, typ)) in
+  match typ.it with
+  | ArrayT (kind, typ) -> Some (array_acc id_exp (kind, typ) at)
+  | _ -> None
+
+
 type sort = Field | Local | Method
 
 module Env = T.Env
@@ -84,7 +120,7 @@ let rec extract_invariants : item list -> (par -> invariants -> invariants) = fu
   | [] -> fun _ x -> x
   | { it = InvariantI (s, e); at; _ } :: p ->
       fun self es ->
-        !!! at (MacroCall(s, !!! at (LocalVar (fst self, snd self))))
+        !!! at (MacroCall(s, [!!! at (LocalVar (fst self, snd self))]))
         :: extract_invariants p self es
   | _ :: p -> extract_invariants p
 
@@ -121,12 +157,19 @@ let rec extract_concurrency (seq : seqn) : stmt' list * seqn =
   let conc, stmts = List.fold_left extr ([], []) stmts in
   rev conc, { seq with it = fst seq.it, rev stmts }
 
+let prelude =
+  let (!!) p = !!! Source.no_region p in
+  [ !! (ImportI (!! "viper_lib/array.vpr")) ]
+
 let rec unit (u : M.comp_unit) : prog Diag.result =
   Diag.(
+    let open Syntax in
     reset_stamps();
-    try return (unit' u) with
+    let* prog = try return (unit' u) with
     | Unsupported (at, desc) -> error at "0" "viper" ("translation to viper failed:\n"^desc)
-    | _ -> error u.it.M.body.at "1" "viper" "translation to viper failed"
+    | _ -> error u.it.M.body.at "1" "viper" "translation to viper failed" in
+    let prog' = {prog with it = (prelude @ prog.it)}
+    in return prog'
   )
 
 and unit' (u : M.comp_unit) : prog =
@@ -134,7 +177,7 @@ and unit' (u : M.comp_unit) : prog =
   match body.it with
   | M.ActorU(id_opt, decs) ->
     let ctxt = { self = None; ids = Env.empty; ghost_items = ref []; ghost_inits = ref []; ghost_perms = ref []; ghost_conc = ref [] } in
-    let ctxt', inits, mk_is = dec_fields ctxt decs in
+    let ctxt', perms, inits, mk_is = unit_decls ctxt decs in
     let is' = List.map (fun mk_i -> mk_i ctxt') mk_is in
     (* given is', compute ghost_is *)
     let ghost_is = List.map (fun mk_i -> mk_i ctxt') !(ctxt.ghost_items) in
@@ -142,8 +185,6 @@ and unit' (u : M.comp_unit) : prog =
     let self_id = !!! (Source.no_region) "$Self" in
     let self_typ = !!! (self_id.at) RefT in
     let ctxt'' = { ctxt' with self = Some self_id.it } in
-    let perms = List.map (fun (id, _) -> fun (at : region) ->
-       (accE at (self ctxt'' at, id))) inits in
     let ghost_perms = List.map (fun mk_p -> mk_p ctxt'') !(ctxt.ghost_perms) in
     let perm =
       fun (at : region) ->
@@ -154,10 +195,7 @@ and unit' (u : M.comp_unit) : prog =
          (perms @ ghost_perms)
     in
     (* Add initializer *)
-    let init_list = List.map (fun (id, init) ->
-        !!! { left = id.at.left; right = init.at.right }
-          (FieldAssignS((self ctxt'' init.at, id), exp ctxt'' init)))
-        inits in
+    let init_list = List.concat_map (fun init -> init ctxt'') inits in
     let init_list = init_list @ List.map (fun mk_s -> mk_s ctxt'') !(ctxt.ghost_inits) in
     let init_body =
       !!! (body.at) ([], init_list)(* ATG: Is this the correct position? *)
@@ -172,8 +210,8 @@ and unit' (u : M.comp_unit) : prog =
       (^^^)
         at
         (MethodI (id, ins, outs,
-          !!! at (MacroCall("$Perm", self ctxt'' at))::pres,
-          !!! at (MacroCall("$Perm", self ctxt'' at))::posts,
+          !!! at (MacroCall("$Perm", [self ctxt'' at]))::pres,
+          !!! at (MacroCall("$Perm", [self ctxt'' at]))::posts,
           body))
         note
       | x -> x) is'' in
@@ -188,7 +226,7 @@ and unit' (u : M.comp_unit) : prog =
         at
         (MethodI(id, ins, outs,
           pres,
-          posts @ [!!! at (MacroCall("$Inv", self ctxt'' at))],
+          posts @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
           body))
         ActorInit
       )
@@ -199,8 +237,8 @@ and unit' (u : M.comp_unit) : prog =
       } -> ((^^^)
         at
         (MethodI(id, ins, outs,
-          pres @ [!!! at (MacroCall("$Inv", self ctxt'' at))],
-          posts @ [!!! at (MacroCall("$Inv", self ctxt'' at))],
+          pres @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
+          posts @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
           body))
         (PublicFunction x)
       )
@@ -212,76 +250,103 @@ and unit' (u : M.comp_unit) : prog =
     !!! (body.at) is
   | _ -> assert false
 
-and dec_fields (ctxt : ctxt) (ds : M.dec_field list) =
+and unit_decls (ctxt : ctxt) (ds : M.dec_field list) =
+  let addSome x xs = match x with Some x' -> x' :: xs | _ -> xs in
   match ds with
   | [] ->
-    (ctxt, [], [])
+    (ctxt, [], [], [])
   | d :: ds ->
-    let ctxt, init, mk_i = dec_field ctxt d in
-    let ctxt, inits, mk_is = dec_fields ctxt ds in
-    (ctxt, (match init with Some i -> i::inits | _ -> inits), mk_i::mk_is)
-
-and dec_field ctxt d =
-  let ctxt, init, mk_i = dec_field' ctxt d.it in
-   (ctxt,
-    init,
-    fun ctxt' ->
-      let (i, info) = mk_i ctxt' in
-      (^^^) (d.at) i info)
-
-and dec_field' ctxt d =
+    let ctxt, perm, init, mk_i = unit_decl' ctxt d.it (d.at) in
+    let mk_i' = (fun ctxt' ->
+        let (i, info) = mk_i ctxt' in
+        (^^^) (d.at) i info) in
+    let ctxt, perms, inits, mk_is = unit_decls ctxt ds in
+    (ctxt,
+     addSome perm perms,
+     addSome init inits,
+     addSome (Some mk_i') mk_is)
+
+and unit_decl' ctxt (d : M.dec_field') at =
+  let self_id = !!! (Source.no_region) "$Self" in
+  let self_var at = !!! at (LocalVar (!!! at self_id.it, !!! at RefT)) in
   match d.M.dec.it with
+  | M.VarD (x, {it=M.AnnotE ({it=M.ArrayE (mut, es); note;_}, _); at=e_at;_}) ->
+      let lhs = !!! Source.no_region (FldAcc (self_var e_at, id x)) in
+      let typ' = tr_typ note.M.note_typ in
+      { ctxt with ids = Env.add x.it Field ctxt.ids },
+      Some (fun at -> (* perm *)
+              !!! at (AndE (accE at (self_var at, id x),
+                      !!! at (AndE (array_acc lhs (Mut, inner_type typ') at,
+                                    array_size_inv lhs (List.length es) at))))),
+      Some (fun ctxt -> (* init *)
+          let es' = List.map (fun e -> exp ctxt e) es in
+          array_alloc lhs typ' es' e_at),
+      (fun ctxt' ->
+        (FieldI(id x, typ'),
+        NoInfo))
   | M.VarD (x, e) ->
       { ctxt with ids = Env.add x.it Field ctxt.ids },
-      Some (id x, e),
-      fun ctxt' ->
+      Some (fun at -> accE at (self_var at, id x)), (* perm *)
+      Some (fun ctxt -> (* init *)
+              [!!! {left = x.at.left; right = e.at.right}
+                   (FieldAssignS((self_var e.at, id x), exp ctxt e))]),
+      (fun ctxt' ->
         (FieldI(id x, tr_typ e.note.M.note_typ),
-        NoInfo)
+        NoInfo))
   (* async functions *)
   | M.(LetD ({it=VarP f;_},
              {it=FuncE(x, sp, tp, p, t_opt, sugar,
              {it = AsyncE (T.Fut, _, e); _} );_}, None)) -> (* ignore async *)
       { ctxt with ids = Env.add f.it Method ctxt.ids },
-      None,
+      None, (* no perm *)
+      None, (* no init *)
       fun ctxt' ->
         let open Either in
-        let self_id = !!! (Source.no_region) "$Self" in
         let method_args = args p in
         let ctxt'' = { ctxt'
           with self = Some self_id.it;
                ids = List.fold_left (fun env (id, _) -> Env.add id.it Local env) ctxt.ids method_args }
-        in (* TODO: add args (and rets?) *)
+        in
         let stmts = stmt ctxt'' e in
         let _, stmts = extract_concurrency stmts in
         let pres, stmts' = List.partition_map (function { it = PreconditionS exp; _ } -> Left exp | s -> Right s) (snd stmts.it) in
         let posts, stmts' = List.partition_map (function { it = PostconditionS exp; _ } -> Left exp | s -> Right s) stmts' in
         let stmts'' = stmts' @ [!!! Source.no_region (LabelS(!!! (Source.no_region) "$Ret"))] in
-        (MethodI(id f, (self_id, !!! Source.no_region RefT)::method_args, rets t_opt, pres, posts, Some { stmts with it = fst stmts.it, stmts'' } ),
+        (* extract pre/post condition from types *)
+        let type_accs = List.filter_map (fun (id, typ) -> type_acc id typ Source.no_region) method_args in
+        let pres' = type_accs @ pres in
+        let posts' = type_accs @ posts in
+        (MethodI(id f, (self_id, !!! Source.no_region RefT)::method_args, rets t_opt, pres', posts', Some { stmts with it = fst stmts.it, stmts'' } ),
         PublicFunction f.it)
   (* private sync functions *)
   | M.(LetD ({it=VarP f;_},
              {it=FuncE(x, sp, tp, p, t_opt, sugar, e );_},
              None)) ->
       { ctxt with ids = Env.add f.it Method ctxt.ids },
-      None,
+      None, (* no perm *)
+      None, (* no init *)
       fun ctxt' ->
         let open Either in
-        let self_id = !!! (Source.no_region) "$Self" in
         let method_args = args p in
         let ctxt'' = { ctxt'
           with self = Some self_id.it;
-               ids = List.fold_left (fun env (id, _) -> Env.add id.it Local env) ctxt.ids method_args }
-        in (* TODO: add args (and rets?) *)
+               ids  = List.fold_left (fun env (id, _) -> Env.add id.it Local env) ctxt.ids method_args }
+        in
         let stmts = stmt ctxt'' e in
         let _, stmts = extract_concurrency stmts in
         let pres, stmts' = List.partition_map (function { it = PreconditionS exp; _ } -> Left exp | s -> Right s) (snd stmts.it) in
         let posts, stmts' = List.partition_map (function { it = PostconditionS exp; _ } -> Left exp | s -> Right s) stmts' in
         let stmts'' = stmts' @ [!!! Source.no_region (LabelS(!!! (Source.no_region) "$Ret"))] in
-        (MethodI(id f, (self_id, !!! Source.no_region RefT)::method_args, rets t_opt, pres, posts, Some { stmts with it = fst stmts.it, stmts'' } ),
+        (* extract pre/post condition from types *)
+        let type_accs = List.filter_map (fun (id, typ) -> type_acc id typ Source.no_region) method_args in
+        let pres' = type_accs @ pres in
+        let posts' = type_accs @ posts in
+        (MethodI(id f, (self_id, !!! Source.no_region RefT)::method_args, rets t_opt, pres', posts', Some { stmts with it = fst stmts.it, stmts'' } ),
         PrivateFunction f.it)
   | M.(ExpD { it = AssertE (Invariant, e); at; _ }) ->
       ctxt,
-      None,
+      None, (* no perm *)
+      None, (* no init *)
       fun ctxt' ->
         (InvariantI (Printf.sprintf "invariant_%d" at.left.line, exp { ctxt' with self = Some "$Self" }  e), NoInfo)
   | _ ->
@@ -322,12 +387,12 @@ and dec ctxt d =
     { ctxt with ids = Env.add x.it Local ctxt.ids },
     fun ctxt' ->
       ([ !!(id x, tr_typ e.note.M.note_typ) ],
-       [ !!(assign_stmt ctxt' (id x) e) ])
+       assign_stmt ctxt' (id x) e d.at)
   | M.(LetD ({it=VarP x;_}, e, None)) ->
      { ctxt with ids = Env.add x.it Local ctxt.ids },
      fun ctxt' ->
        ([ !!(id x, tr_typ e.note.M.note_typ) ],
-        [ !!(assign_stmt ctxt' (id x) e) ])
+        assign_stmt ctxt' (id x) e d.at)
   | M.(ExpD e) -> (* TODO: restrict to e of unit type? *)
      (ctxt,
       fun ctxt' ->
@@ -386,13 +451,13 @@ and stmt ctxt (s : M.exp) : seqn =
             (self ctxt Source.no_region, !!id),
             (!!(AddE(!!(FldAcc (self ctxt (s.at), !!id)),
                      intLitE Source.no_region 1)))));
-          !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)),
-                              !@(MacroCall("$Inv", self ctxt at))))));
+          !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
+                              !@(MacroCall("$Inv", [self ctxt at]))))));
           !@(SeqnS (
               !@([],
                  [
-                   !@(InhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)),
-                                  !@(AndE(!@(MacroCall("$Inv", self ctxt at)),
+                   !@(InhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
+                                  !@(AndE(!@(MacroCall("$Inv", [self ctxt at])),
                                           !@(GtCmpE(!@(FldAcc (self ctxt at, !@id)),
                                                intLitE Source.no_region 0))))))));
                    !@(FieldAssignS(
@@ -400,21 +465,33 @@ and stmt ctxt (s : M.exp) : seqn =
                           (!@(SubE(!@(FldAcc (self ctxt at, !@id)),
                                    intLitE at 1)))));
                    !!! (e.at) (SeqnS stmts);
-                   !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)),
-                                       !@(MacroCall("$Inv", self ctxt at)))))) ])));
-          !!(InhaleS (!!(AndE(!!(MacroCall("$Perm", self ctxt at)),
-                              !!(MacroCall("$Inv", self ctxt at))))));
+                   !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
+                                       !@(MacroCall("$Inv", [self ctxt at])))))) ])));
+          !!(InhaleS (!!(AndE(!!(MacroCall("$Perm", [self ctxt at])),
+                              !!(MacroCall("$Inv", [self ctxt at]))))));
         ])
   | M.WhileE(e, s1) ->
      let (invs, s1') = extract_loop_invariants s1 in
      let invs' = List.map (fun inv -> exp ctxt inv) invs in
      !!([],
         [ !!(WhileS(exp ctxt e, invs', stmt ctxt s1')) ])
+  (* TODO: remove by Motoko->Motoko transformation *)
+  | M.(AssignE({it = VarE x; _}, {it = ArrayE (mut, es); note={note_typ=typ; _}; _})) ->
+     let typ' = tr_typ typ in
+     let es'  = List.map (exp ctxt) es in
+     let temp_id = fresh_id (fresh_id (id x).it) in
+     let lhs = !!(LocalVar (!!temp_id, typ')) in
+     !! ([!!(!!temp_id, typ')],
+         array_alloc lhs typ' es' (s.at)
+         @ [!!(VarAssignS (id x, !!(LocalVar (!!temp_id, typ'))))])
+  | M.(AssignE({it = IdxE (e1, e2);_}, e3)) ->
+     !!([],
+        [!!(FieldAssignS (fldacc ctxt s.at e1 e2 e3.note.M.note_typ, exp ctxt e3))])
   | M.(AssignE({it = VarE x; _}, e2)) ->
      begin match Env.find x.it ctxt.ids with
      | Local ->
         let loc = !!! (x.at) (x.it) in
-        !!([], [!!(assign_stmt ctxt loc e2)])
+        !!([], assign_stmt ctxt loc e2 s.at)
      | Field ->
        let fld = (self ctxt x.at, id x) in
        !!([],
@@ -444,19 +521,25 @@ and stmt ctxt (s : M.exp) : seqn =
        self_var :: call_args ctxt args))])
   | M.RetE e ->
      !!([],
-        [ !!(assign_stmt ctxt (!!! (Source.no_region) "$Res") e);
-          !!(GotoS(!!! (Source.no_region) "$Ret"))
-        ])
+        assign_stmt ctxt (!!! (Source.no_region) "$Res") e s.at
+        @ [ !!(GotoS(!!! (Source.no_region) "$Ret")) ])
   | _ ->
      unsupported s.at (Arrange.exp s)
 
-and assign_stmt ctxt x e =
+and assign_stmt ctxt x e at =
+  let (!!) p = !!! at p in
   match e with
+  | M.({it=AnnotE (e, _);_}) -> assign_stmt ctxt x e at
   | M.({it = CallE({it = VarE m; _}, inst, args); _}) ->
-    MethodCallS ([x], id m,
-      let self_var = self ctxt m.at in
-      self_var :: call_args ctxt args)
-  | _ -> VarAssignS(x, exp ctxt e)
+     [ !!(MethodCallS ([x], id m,
+                       let self_var = self ctxt m.at in
+                       self_var :: call_args ctxt args))]
+  | M.({it=ArrayE (mut, es); note;_}) ->
+      let es' = List.map (exp ctxt) es in
+      let t' = tr_typ note.M.note_typ in
+      let lhs = !!(LocalVar (x, t')) in
+      (array_alloc lhs t' es' at)
+  | _ -> [!! (VarAssignS(x, exp ctxt e))]
 
 and call_args ctxt e =
   match e with
@@ -479,6 +562,8 @@ and exp ctxt e =
     end
   | M.AnnotE(a, b) ->
     exp ctxt a
+  | M.CallE ({it=M.DotE (id_exp, {it="size";_});_}, _inst, {it=M.TupE ([]);at;_})
+    -> array_size (exp ctxt id_exp) at
   | M.LitE r ->
     begin match !r with
     | M.BoolLit b ->
@@ -518,6 +603,8 @@ and exp ctxt e =
      !!(Implies (exp ctxt e1, exp ctxt e2))
   | M.OldE e ->
     !!(Old (exp ctxt e))
+  | M.IdxE (e1, e2) ->
+     !!(FldAcc (fldacc ctxt e.at e1 e2 e.note.M.note_typ))
   | _ ->
      unsupported e.at (Arrange.exp e)
 
@@ -533,6 +620,10 @@ and rets t_opt =
 
 and id id = { it = id.it; at = id.at; note = NoInfo }
 
+and fldacc ctxt at e1 e2 el_typ =
+  let fld = type_field (tr_typ' el_typ) in
+  !!! at (FuncCall ("loc", [exp ctxt e1; exp ctxt e2])), !!! at fld
+
 and tr_typ typ =
   { it = tr_typ' typ;
     at = Source.no_region;
@@ -542,4 +633,6 @@ and tr_typ' typ =
   | T.Prim T.Int -> IntT
   | T.Prim T.Nat -> IntT    (* Viper has no native support for Nat, so translate to Int *)
   | T.Prim T.Bool -> BoolT
+  | T.Array (T.Mut typ) -> ArrayT (Mut  , tr_typ' (T.normalize typ))
+  | T.Array typ         -> ArrayT (Const, tr_typ' (T.normalize typ))
   | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ (T.normalize typ))
diff --git a/src/viper/viper_lib/array.vpr b/src/viper/viper_lib/array.vpr
new file mode 100644
index 00000000000..ddb4dde99f4
--- /dev/null
+++ b/src/viper/viper_lib/array.vpr
@@ -0,0 +1,25 @@
+domain Array {
+  function loc(a: Array, i: Int): Ref
+  function size(a: Array): Int
+  function first(r: Ref): Array
+  function second(r: Ref): Int
+
+  axiom all_diff {
+    forall a: Array, i: Int :: {loc(a, i)}
+      first(loc(a, i)) == a && second(loc(a, i)) == i
+  }
+
+  axiom size_nonneg {
+    forall a: Array :: size(a) >= 0
+  }
+}
+
+define array_acc_mut(a, t) forall j: Int :: 0 <= j && j < size(a) ==> acc(loc(a, j).t)
+define array_acc(a, t)     forall j: Int :: 0 <= j && j < size(a) ==> acc(loc(a, j).t, 1/2)
+define untouched(a, t) forall j: Int :: 0 <= j && j < size(a) ==> loc(a, j).t == old(loc(a, j).t)
+
+/* typed refs */
+field int: Int
+field bool: Bool
+field ref: Ref
+field array: Array
diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok
index 098fbe22369..a2fa0d08db5 100644
--- a/test/repl/ok/viper.stdout.ok
+++ b/test/repl/ok/viper.stdout.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/run.sh b/test/run.sh
index 142d3a912df..cc27783a545 100755
--- a/test/run.sh
+++ b/test/run.sh
@@ -288,6 +288,7 @@ do
   $ECHO -n "$base:"
   [ -d $out ] || mkdir $out
   [ -d $ok ] || mkdir $ok
+  [ -d $out/viper_lib ] ||  ln -s ../../../src/viper/viper_lib/ $out/viper_lib
 
   rm -rf $out/$base $out/$base.*
 
diff --git a/test/viper/array.mo b/test/viper/array.mo
new file mode 100644
index 00000000000..6e6a0ee2913
--- /dev/null
+++ b/test/viper/array.mo
@@ -0,0 +1,58 @@
+// @verify
+// import Array "mo:base/Array";
+
+actor {
+    
+    var arr : [var Int] = [var 1, 2];
+    var f : Int = 2;
+    var count : Int = 42; // let is not supported
+
+    public func foo(): async Int {
+        var vi_a : [Int] = (([1] : [Int]) : [Int]);
+        var vm_a : [var Int] = [var 1, 2];
+        let li_a : [Bool] = [false];
+        let lm_a : [var Bool] = [var false];
+        // vi_a = [1, 2]
+        vi_a := [1, 2];
+        // li_a := [1, 2]; // error
+        vm_a := [var 42];
+        // lm_a := [1, 2]; // error
+
+        return 42;
+    };
+
+    public func baz1(): async [Int] {
+      let r : [Int] = [1, 2];
+      return r;
+    };
+
+    private func baz2(): [var Int] {
+      let r : [var Int] = [var 1, 2];
+      return r;
+    };
+
+    private func bar(): Int {
+      let x : [Int] = [42, 24];
+      let y : [var Bool] = [var false];
+      y[0] := true;
+      let z : Int = x[0] + x[1];
+      return x[1];
+    };
+
+    public func bar2(x: [Int]):  async Int {
+      assert:func x.size() == 2;
+      let y : [var Bool] = [var false];
+      y[0] := true;
+      let z : Int = x[0] + x[1];
+      return x[1];
+    };
+
+    public func inc() : async Int {
+      arr[0] := arr[0] + 1;
+      return arr[0]
+    };
+
+    public func len(): async Int {
+      return arr.size();
+    };
+}
diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok
new file mode 100644
index 00000000000..ed4b896a3b3
--- /dev/null
+++ b/test/viper/ok/array.silicon.ok
@@ -0,0 +1 @@
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@5.1)
diff --git a/test/viper/ok/array.tc.ok b/test/viper/ok/array.tc.ok
new file mode 100644
index 00000000000..bf84d27a2e0
--- /dev/null
+++ b/test/viper/ok/array.tc.ok
@@ -0,0 +1,8 @@
+array.mo:7.9-7.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
+array.mo:8.9-8.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
+array.mo:13.13-13.17: warning [M0194], unused identifier li_a (delete or rename to wildcard `_` or `_li_a`)
+array.mo:14.13-14.17: warning [M0194], unused identifier lm_a (delete or rename to wildcard `_` or `_lm_a`)
+array.mo:29.18-29.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:34.18-34.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:38.11-38.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:46.11-46.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
new file mode 100644
index 00000000000..6b341ad0846
--- /dev/null
+++ b/test/viper/ok/array.vpr.ok
@@ -0,0 +1,174 @@
+import "viper_lib/array.vpr"
+define $Perm($Self) ((((true && (acc(($Self).arr,write) && (array_acc_mut(
+                                                            ($Self).arr, int) && (
+  size(($Self).arr) == 2)))) && acc(($Self).f,write)) && acc(($Self).count,write)))
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      inhale array_acc_mut(($Self).arr, int)
+      inhale (size(($Self).arr) == 2)
+      (loc(($Self).arr, 0)).int := 1
+      (loc(($Self).arr, 1)).int := 2
+      exhale array_acc_mut(($Self).arr, int)
+      inhale array_acc_mut(($Self).arr, int)
+      ($Self).f := 2
+      ($Self).count := 42 
+    }
+field arr: Array
+field f: Int
+field count: Int
+method foo($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var vi_a: Array
+      var vm_a: Array
+      var li_a: Array
+      var lm_a: Array
+      var vi_a_2: Array
+      var vm_a_2: Array
+      inhale array_acc_mut(vi_a, int)
+      inhale (size(vi_a) == 1)
+      (loc(vi_a, 0)).int := 1
+      exhale array_acc_mut(vi_a, int)
+      inhale array_acc(vi_a, int)
+      inhale array_acc_mut(vm_a, int)
+      inhale (size(vm_a) == 2)
+      (loc(vm_a, 0)).int := 1
+      (loc(vm_a, 1)).int := 2
+      exhale array_acc_mut(vm_a, int)
+      inhale array_acc_mut(vm_a, int)
+      inhale array_acc_mut(li_a, bool)
+      inhale (size(li_a) == 1)
+      (loc(li_a, 0)).bool := false
+      exhale array_acc_mut(li_a, bool)
+      inhale array_acc(li_a, bool)
+      inhale array_acc_mut(lm_a, bool)
+      inhale (size(lm_a) == 1)
+      (loc(lm_a, 0)).bool := false
+      exhale array_acc_mut(lm_a, bool)
+      inhale array_acc_mut(lm_a, bool)
+      inhale array_acc_mut(vi_a_2, int)
+      inhale (size(vi_a_2) == 2)
+      (loc(vi_a_2, 0)).int := 1
+      (loc(vi_a_2, 1)).int := 2
+      exhale array_acc_mut(vi_a_2, int)
+      inhale array_acc(vi_a_2, int)
+      vi_a := vi_a_2
+      inhale array_acc_mut(vm_a_2, int)
+      inhale (size(vm_a_2) == 1)
+      (loc(vm_a_2, 0)).int := 42
+      exhale array_acc_mut(vm_a_2, int)
+      inhale array_acc_mut(vm_a_2, int)
+      vm_a := vm_a_2
+      $Res := 42
+      goto $Ret
+      label $Ret 
+    }
+method baz1($Self: Ref)
+     returns ($Res: Array)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var r: Array
+      inhale array_acc_mut(r, int)
+      inhale (size(r) == 2)
+      (loc(r, 0)).int := 1
+      (loc(r, 1)).int := 2
+      exhale array_acc_mut(r, int)
+      inhale array_acc(r, int)
+      $Res := r
+      goto $Ret
+      label $Ret 
+    }
+method baz2($Self: Ref)
+     returns ($Res: Array)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var r: Array
+      inhale array_acc_mut(r, int)
+      inhale (size(r) == 2)
+      (loc(r, 0)).int := 1
+      (loc(r, 1)).int := 2
+      exhale array_acc_mut(r, int)
+      inhale array_acc_mut(r, int)
+      $Res := r
+      goto $Ret
+      label $Ret 
+    }
+method bar($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var x: Array
+      var y: Array
+      var z: Int
+      inhale array_acc_mut(x, int)
+      inhale (size(x) == 2)
+      (loc(x, 0)).int := 42
+      (loc(x, 1)).int := 24
+      exhale array_acc_mut(x, int)
+      inhale array_acc(x, int)
+      inhale array_acc_mut(y, bool)
+      inhale (size(y) == 1)
+      (loc(y, 0)).bool := false
+      exhale array_acc_mut(y, bool)
+      inhale array_acc_mut(y, bool)
+      (loc(y, 0)).bool := true
+      z := ((loc(x, 0)).int + (loc(x, 1)).int)
+      $Res := (loc(x, 1)).int
+      goto $Ret
+      label $Ret 
+    }
+method bar2($Self: Ref, x: Array)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires array_acc(x, int)
+    requires (size(x) == 2)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures array_acc(x, int)
+    ensures $Inv($Self)
+    { var y: Array
+      var z: Int
+      inhale array_acc_mut(y, bool)
+      inhale (size(y) == 1)
+      (loc(y, 0)).bool := false
+      exhale array_acc_mut(y, bool)
+      inhale array_acc_mut(y, bool)
+      (loc(y, 0)).bool := true
+      z := ((loc(x, 0)).int + (loc(x, 1)).int)
+      $Res := (loc(x, 1)).int
+      goto $Ret
+      label $Ret 
+    }
+method inc($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      (loc(($Self).arr, 0)).int := ((loc(($Self).arr, 0)).int + 1)
+      $Res := (loc(($Self).arr, 0)).int
+      goto $Ret
+      label $Ret 
+    }
+method len($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := size(($Self).arr)
+      goto $Ret
+      label $Ret 
+    }
diff --git a/test/viper/ok/array.vpr.stderr.ok b/test/viper/ok/array.vpr.stderr.ok
new file mode 100644
index 00000000000..bf84d27a2e0
--- /dev/null
+++ b/test/viper/ok/array.vpr.stderr.ok
@@ -0,0 +1,8 @@
+array.mo:7.9-7.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
+array.mo:8.9-8.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
+array.mo:13.13-13.17: warning [M0194], unused identifier li_a (delete or rename to wildcard `_` or `_li_a`)
+array.mo:14.13-14.17: warning [M0194], unused identifier lm_a (delete or rename to wildcard `_` or `_lm_a`)
+array.mo:29.18-29.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:34.18-34.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:38.11-38.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:46.11-46.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok
index 202af03d0c2..73bee59d7d1 100644
--- a/test/viper/ok/assertions.silicon.ok
+++ b/test/viper/ok/assertions.silicon.ok
@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@10.13--10.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@28.15--28.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@11.13--11.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@29.15--29.44)
diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
index a82bb5216f9..8c1edbe39eb 100644
--- a/test/viper/ok/assertions.vpr.ok
+++ b/test/viper/ok/assertions.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).u,write)) && acc(($Self).v,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok
index 4cd9741c5a2..011abed5492 100644
--- a/test/viper/ok/async.silicon.ok
+++ b/test/viper/ok/async.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@33.15--33.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@34.15--34.42)
diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
index 8e10ad1f324..89656e3ef40 100644
--- a/test/viper/ok/async.vpr.ok
+++ b/test/viper/ok/async.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 field $message_async_4: Int
 field $message_async_2: Int
 field $message_async: Int
diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok
index 2738a3acfa7..504f5c4f949 100644
--- a/test/viper/ok/claim-broken.silicon.ok
+++ b/test/viper/ok/claim-broken.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@31.20--31.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@32.20--32.47)
diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
index 2f9e89edf51..663bf47cb53 100644
--- a/test/viper/ok/claim-broken.vpr.ok
+++ b/test/viper/ok/claim-broken.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
index e2a098d0378..38db32f565e 100644
--- a/test/viper/ok/claim-reward-naive.vpr.ok
+++ b/test/viper/ok/claim-reward-naive.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (invariant_5($Self))
 method __init__($Self: Ref)
diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok
index c704b94e8c8..da5ef00f4ad 100644
--- a/test/viper/ok/claim-simple.silicon.ok
+++ b/test/viper/ok/claim-simple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
index b26442befcf..79676ba23d8 100644
--- a/test/viper/ok/claim-simple.vpr.ok
+++ b/test/viper/ok/claim-simple.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
index 2a99877bfe9..1e6fc887724 100644
--- a/test/viper/ok/claim.vpr.ok
+++ b/test/viper/ok/claim.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok
index 69fb8c629a0..da5ef00f4ad 100644
--- a/test/viper/ok/counter.silicon.ok
+++ b/test/viper/ok/counter.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
index 5196861d655..05f57c3a055 100644
--- a/test/viper/ok/counter.vpr.ok
+++ b/test/viper/ok/counter.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) ((true && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok
index 94a1ad16eff..df058df090f 100644
--- a/test/viper/ok/invariant.silicon.ok
+++ b/test/viper/ok/invariant.silicon.ok
@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@7.13--7.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@8.13--8.24)
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
index 4db1a7a12b5..ddbee1e1a4e 100644
--- a/test/viper/ok/invariant.vpr.ok
+++ b/test/viper/ok/invariant.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (((invariant_9($Self) && invariant_10($Self)) && invariant_11($Self)))
 method __init__($Self: Ref)
diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok
index d7ae1e8621c..66b40602054 100644
--- a/test/viper/ok/loop-invariant.silicon.ok
+++ b/test/viper/ok/loop-invariant.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@1.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@2.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (array.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
index d222eeac074..7523752a0b1 100644
--- a/test/viper/ok/loop-invariant.vpr.ok
+++ b/test/viper/ok/loop-invariant.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok
index 05a4c452841..66b40602054 100644
--- a/test/viper/ok/method-call.silicon.ok
+++ b/test/viper/ok/method-call.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (method-call.vpr@1.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@2.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (array.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
index 8cdce6e4f7d..fac7faada10 100644
--- a/test/viper/ok/method-call.vpr.ok
+++ b/test/viper/ok/method-call.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
index 1671de8e2f8..da5ef00f4ad 100644
--- a/test/viper/ok/nats.silicon.ok
+++ b/test/viper/ok/nats.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
index 472e810081c..0ec33e83c6c 100644
--- a/test/viper/ok/nats.vpr.ok
+++ b/test/viper/ok/nats.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) ((true && acc(($Self).x,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
index ac51b18d3e4..60bd828283f 100644
--- a/test/viper/ok/private.vpr.ok
+++ b/test/viper/ok/private.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (invariant_7($Self))
 method __init__($Self: Ref)
diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok
index d0c64d57d11..66b40602054 100644
--- a/test/viper/ok/simple-funs.silicon.ok
+++ b/test/viper/ok/simple-funs.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@1.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@2.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (array.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
index 81d6dcc7626..ba080fa0d97 100644
--- a/test/viper/ok/simple-funs.vpr.ok
+++ b/test/viper/ok/simple-funs.vpr.ok
@@ -1,3 +1,4 @@
+import "viper_lib/array.vpr"
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)