diff --git a/backend/cn/check.ml b/backend/cn/check.ml
index 67b8fd5ac..544c84bc3 100644
--- a/backend/cn/check.ml
+++ b/backend/cn/check.ml
@@ -98,13 +98,13 @@ let rec pattern_match (M_Pattern (loc, _, pattern)) it =
    | M_CaseCtor (constructor, pats) ->
       match constructor, pats with
       | M_Cnil item_bt, [] ->
-         let@ () = add_c (LC.t_ (eq__ it (nil_ ~item_bt))) in
+         let@ () = add_c loc (LC.t_ (eq__ it (nil_ ~item_bt))) in
          return []
       | M_Ccons, [p1; p2] ->
          let@ item_bt = infer_pattern p1 in
          let@ a1 = pattern_match p1 (head_ ~item_bt it) in
          let@ a2 = pattern_match p2 (tail_ it) in
-         let@ () = add_c (LC.t_ (ne_ (it, nil_ ~item_bt))) in
+         let@ () = add_c loc (LC.t_ (ne_ (it, nil_ ~item_bt))) in
          return (a1 @ a2)
       | M_Ctuple, pats ->
          let@ all_as = ListM.mapiM (fun i p ->
@@ -393,7 +393,7 @@ let check_single_ct loc expr =
     let@ provable = provable loc in
     begin match provable (t_ eq) with
       | `True ->
-        let@ () = add_c (t_ eq) in
+        let@ () = add_c loc (t_ eq) in
         return ct
        | `False ->
         (* TODO: this is the most likely case, give a better error *)
@@ -713,7 +713,7 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t)
        let@ eq_opt = get_eq_in_model loc msg ptr ptr_opts in
        Pp.debug 5 (lazy (Pp.item "function pointer application: case splitting on" (IT.pp eq_opt)));
        let aux e cond =
-         let@ () = add_c (t_ cond) in
+         let@ () = add_c loc (t_ cond) in
          Pp.debug 5 (lazy (Pp.item "checking consistency of eq branch" (IT.pp cond)));
          let@ provable = provable loc in
          match provable (t_ (bool_ false)) with
@@ -764,7 +764,7 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t)
   | M_PEif (pe, e1, e2) ->
      check_pexpr ~expect:Bool pe (fun c ->
      let aux e cond = 
-       let@ () = add_c (t_ cond) in
+       let@ () = add_c loc (t_ cond) in
        Pp.debug 5 (lazy (Pp.item "checking consistency of if-branch" (IT.pp cond)));
        let@ provable = provable loc in
        match provable (t_ (bool_ false)) with
@@ -1023,7 +1023,7 @@ let instantiate loc filter arg =
   let arg_s = Sym.fresh_make_uniq "instance" in
   let arg_it = sym_ (arg_s, IT.bt arg) in
   let@ () = add_l arg_s (IT.bt arg_it) (loc, lazy (Sym.pp arg_s)) in
-  let@ () = add_c (LC.t_ (eq__ arg_it arg)) in
+  let@ () = add_c loc (LC.t_ (eq__ arg_it arg)) in
   let@ constraints = all_constraints () in
   let extra_assumptions = 
     List.filter_map (fun lc ->
@@ -1037,7 +1037,7 @@ let instantiate loc filter arg =
   in
   if List.length extra_assumptions == 0 then Pp.warn loc (Pp.string "nothing instantiated")
   else ();
-  add_cs extra_assumptions
+  add_cs loc extra_assumptions
 
 
 
@@ -1181,8 +1181,8 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
              IT.fresh Loc
         in
         let@ () = add_l ret_s (IT.bt ret) (loc, lazy (Pp.string "allocation")) in
-        let@ () = add_c (t_ (representable_ (Pointer act.ct, ret))) in
-        let@ () = add_c (t_ (alignedI_ ~align:arg ~t:ret)) in
+        let@ () = add_c loc (t_ (representable_ (Pointer act.ct, ret))) in
+        let@ () = add_c loc (t_ (alignedI_ ~align:arg ~t:ret)) in
         let@ () = 
           add_r loc
             (P { name = Owned (act.ct, Uninit); 
@@ -1315,7 +1315,7 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
   | _, M_Eif (c_pe, e1, e2) ->
      check_pexpr ~expect:Bool c_pe (fun carg ->
      let aux lc nm e = 
-       let@ () = add_c (t_ lc) in
+       let@ () = add_c loc (t_ lc) in
        let@ provable = provable loc in
        match provable (t_ (bool_ false)) with
        | `True -> return ()
@@ -1427,7 +1427,7 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
             | M_CN_extract (to_extract, it) ->
                let@ predicate_name = RI.predicate_name_of_to_extract loc to_extract in
                let@ it = WIT.check loc Integer it in
-               add_movable_index (predicate_name, it)
+               add_movable_index loc (predicate_name, it)
             | M_CN_unfold (f, args) ->
                let@ def = get_logical_function_def loc f in
                let has_args, expect_args = List.length args, List.length def.args in
@@ -1445,7 +1445,7 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
                   in
                   fail (fun _ -> {loc; msg = Generic msg})
                | Some body -> 
-                  add_c (LC.t_ (eq_ (pred_ f args def.return_bt, body)))
+                  add_c loc (LC.t_ (eq_ (pred_ f args def.return_bt, body)))
                end
             | M_CN_apply (lemma, args) ->
                let@ (_loc, lemma_typ) = get_lemma loc lemma in
@@ -1536,10 +1536,10 @@ let bind_arguments (loc : Loc.t) (full_args : _ mu_arguments) =
   let rec aux_l resources = function
     | M_Define ((s, it), info, args) ->
        let@ () = add_l s (IT.bt it) (fst info, lazy (Sym.pp s)) in
-       let@ () = add_c (LC.t_ (def_ s it)) in
+       let@ () = add_c (fst info) (LC.t_ (def_ s it)) in
        aux_l resources args
     | M_Constraint (lc, info, args) ->
-       let@ () = add_c lc in
+       let@ () = add_c (fst info) lc in
        aux_l resources args
     | M_Resource ((s, (re, bt)), info, args) ->
        let@ () = add_l s bt (fst info, lazy (Sym.pp s)) in
@@ -1718,7 +1718,7 @@ let record_globals globs =
          let bt = Loc in
          let info = (Loc.unknown, lazy (Pp.item "global" (Sym.pp sym))) in
          let@ () = add_a sym bt info in
-         let@ () = add_c (t_ (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt)))) in
+         let@ () = add_c Loc.unknown (t_ (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt)))) in
          return ()
     ) globs 
 
@@ -1729,7 +1729,7 @@ let wf_check_and_record_functions mu_funs mu_call_sigs =
     (* let lc1 = t_ (ne_ (null_, sym_ (fsym, Loc))) in *)
     let lc2 = t_ (representable_ (Pointer Void, sym_ (fsym, Loc))) in
     let@ () = add_l fsym Loc (loc, lazy (Pp.item "global fun-ptr" (Sym.pp fsym))) in
-    let@ () = add_cs [(* lc1; *) lc2] in
+    let@ () = add_cs loc [(* lc1; *) lc2] in
     add_fun_decl fsym (loc, ft, Pmap.find fsym mu_call_sigs)
   in
   let welltyped_ping fsym =
diff --git a/backend/cn/pack.ml b/backend/cn/pack.ml
index 2538e41fa..3d2ec1409 100644
--- a/backend/cn/pack.ml
+++ b/backend/cn/pack.ml
@@ -18,6 +18,18 @@ let resource_empty provable resource =
   | `False -> `NonEmpty (constr, Solver.model ())
 
 
+let unfolded_array init (ict, olength) pointer = 
+  let length = Option.get olength in
+  let q_s, q = IT.fresh_named Integer "i" in
+  Q { 
+    name = Owned (ict, init);
+    pointer = pointer;
+    q = q_s;
+    step = int_ (Memory.size_of_ctype ict);
+    iargs = [];
+    permission = and_ [((int_ 0) %<= q); (q %< (int_ length))]
+  }
+  
 
 let packing_ft loc global provable ret = 
   match ret with
@@ -26,18 +38,7 @@ let packing_ft loc global provable ret =
       | Owned ((Void | Integer _ | Pointer _ | Function _), _init) -> 
          None
       | Owned ((Array (ict, olength)) as ct, init) ->
-         let length = Option.get olength in
-         let qpred = 
-           let q_s, q = IT.fresh_named Integer "i" in
-           Q { 
-             name = Owned (ict, init);
-             pointer = ret.pointer;
-             q = q_s;
-             step = int_ (Memory.size_of_ctype ict);
-             iargs = [];
-             permission = and_ [((int_ 0) %<= q); (q %< (int_ length))]
-           }
-         in
+         let qpred = unfolded_array init (ict, olength) ret.pointer in
          let o_s, o = IT.fresh_named (BT.of_sct ct) "value" in
          let at = 
            LAT.Resource ((o_s, (qpred, IT.bt o)), (loc, None),
@@ -86,11 +87,56 @@ let packing_ft loc global provable ret =
   | Q _ -> 
      None
 
+let unpack_owned global (ct, init) pointer (O o) =
+  let open Sctypes in
+  match ct with
+  | (Void | Integer _ | Pointer _ | Function _) -> 
+     None
+  | Array (ict, olength) ->
+    Some [(unfolded_array init (ict, olength) pointer, O o)]
+  | Struct tag ->
+    let layout = SymMap.find tag global.Global.struct_decls in
+    let res =
+      List.fold_right (fun {offset; size; member_or_padding} res ->
+        match member_or_padding with
+        | Some (member, mct) ->
+          let mresource = 
+            (P {
+              name = Owned (mct, init);
+              pointer = memberShift_ (pointer, tag, member);
+              iargs = [];
+            }, 
+            O (member_ ~member_bt:(BT.of_sct mct) (tag, o, member)))
+          in
+          (mresource :: res)
+        | None ->
+          let padding_ct = Sctypes.Array (Integer Char, Some size) in
+          let mresource = 
+            (P {
+              name = Owned (padding_ct, Uninit);
+              pointer = pointer_offset_ (pointer, int_ offset);
+              iargs = [];
+            }, O (default_ (BT.of_sct padding_ct)))
+          in
+          (mresource :: res)
+        ) layout []
+    in
+    Some res
+     
+
 
 let unpack loc global provable (ret, O o) = 
-  match packing_ft loc global provable ret with
-  | None -> None
-  | Some packing_ft -> Some (ResourcePredicates.clause_lrt o packing_ft)
+  match ret with
+  | P {name = Owned (ct, init); pointer; iargs = []} ->
+    begin match unpack_owned global (ct, init) pointer (O o) with
+    | None -> None
+    | Some re -> Some (`RES re)
+    end
+  | _ ->
+    begin match packing_ft loc global provable ret with
+    | None -> None
+    | Some packing_ft -> Some (`LRT (ResourcePredicates.clause_lrt o packing_ft))
+    end
       
 
 
@@ -137,3 +183,4 @@ let extractable_multiple loc provable =
   fun movable_indices re -> aux movable_indices (re, [])
 
 
+
diff --git a/backend/cn/typing.ml b/backend/cn/typing.ml
index bfb1b2303..3f1d8dbf2 100644
--- a/backend/cn/typing.ml
+++ b/backend/cn/typing.ml
@@ -409,7 +409,7 @@ let get_movable_indices () =
   
 
 (* copying and adjusting map_and_fold_resources *)
-let unfold_resources () = 
+let unfold_resources loc = 
   let rec aux () =
     let@ s = get () in
     let@ movable_indices = get_movable_indices () in
@@ -421,13 +421,13 @@ let unfold_resources () =
     | `False ->
     let keep, unpack, extract =
       List.fold_right (fun (re, i) (keep, unpack, extract) ->
-          match Pack.unpack Loc.unknown s.global provable_f re with
+          match Pack.unpack loc s.global provable_f re with
           | Some unpackable -> 
               let pname = RET.pp_predicate_name (RET.predicate_name (fst re)) in
               (keep, (i, pname, unpackable) :: unpack, extract)
           | None -> 
               let re_reduced, extracted =
-                Pack.extractable_multiple Loc.unknown provable_f movable_indices re in
+                Pack.extractable_multiple loc provable_f movable_indices re in
               let keep' = match extracted with
                | [] -> (re_reduced, i) :: keep
                | _ ->
@@ -439,15 +439,15 @@ let unfold_resources () =
         ) resources ([], [], [])
     in
     let@ () = set {s with resources = (keep, orig_ix)} in
-    let rec do_unpacks = function
-      | [] -> return ()
-      | (_i, pname, lrt) :: rest ->
-          let@ _, members = make_return_record Loc.unknown ("unpack_" ^ Pp.plain pname) (LogicalReturnTypes.binders lrt) in
-          let@ () = bind_logical_return_internal Loc.unknown members lrt in
-          do_unpacks rest
+    let do_unpack = function
+      | (_i, pname, `LRT lrt) ->
+          let@ _, members = make_return_record loc ("unpack_" ^ Pp.plain pname) (LogicalReturnTypes.binders lrt) in
+          bind_logical_return_internal loc members lrt
+      | (_i, _pname, `RES res) ->
+          iterM (add_r_internal loc) res
     in
-    let@ () = do_unpacks unpack in
-    let@ () = iterM (add_r_internal Loc.unknown) extract in
+    let@ () = iterM do_unpack unpack in
+    let@ () = iterM (add_r_internal loc) extract in
     match unpack, extract with
     | [], [] -> return ()
     | _ -> 
@@ -658,30 +658,30 @@ let add_movable_index_internal e : unit m =
   Ok ((), {s with movable_indices = e :: s.movable_indices})
 
 
-let add_movable_index e = 
+let add_movable_index loc e = 
   let@ () = add_movable_index_internal e in
-  unfold_resources ()
+  unfold_resources loc
 
 let add_r loc re = 
    let@ () = add_r_internal loc re in
-   unfold_resources ()
+   unfold_resources loc
 
 let add_rs loc rs =
   let@ () = iterM (add_r_internal loc) rs in
-  unfold_resources ()
+  unfold_resources loc
 
-let add_c c =
+let add_c loc c =
   let@ () = add_c_internal c in
-  unfold_resources ()
+  unfold_resources loc
 
-let add_cs cs = 
+let add_cs loc cs = 
   let@ () = iterM add_c_internal cs in
-  unfold_resources ()
+  unfold_resources loc
   
 
 let bind_logical_return loc members lrt = 
   let@ () = bind_logical_return_internal loc members lrt in
-  unfold_resources ()
+  unfold_resources loc
 
 (* Same for return types *)
 let bind_return loc members (rt : ReturnTypes.t) =
diff --git a/backend/cn/typing.mli b/backend/cn/typing.mli
index 222016de7..59425b816 100644
--- a/backend/cn/typing.mli
+++ b/backend/cn/typing.mli
@@ -33,8 +33,8 @@ val add_a_value : Sym.t -> IndexTerms.t -> Context.l_info -> unit m
 val add_l : Sym.t -> BaseTypes.t -> Context.l_info -> (unit) m
 val add_l_value : Sym.t -> IndexTerms.t -> Context.l_info -> unit m
 val add_ls : (Sym.t * BaseTypes.t * Context.l_info) list -> (unit) m
-val add_c : LogicalConstraints.t -> (unit) m
-val add_cs : LogicalConstraints.t list -> (unit) m
+val add_c : Locations.t -> LogicalConstraints.t -> (unit) m
+val add_cs : Locations.t -> LogicalConstraints.t list -> (unit) m
 val add_r : Locations.t -> Resources.t -> unit m
 val add_rs : Locations.t -> Resources.t list -> unit m
 val get_loc_trace : unit -> (Locations.loc list) m
@@ -118,6 +118,7 @@ val bind_return:
 
 
 val add_movable_index:
+    Locations.t ->
     (ResourceTypes.predicate_name * IndexTerms.t) ->
     unit m
 
diff --git a/backend/cn/wellTyped.ml b/backend/cn/wellTyped.ml
index cde84fe77..10c84a285 100644
--- a/backend/cn/wellTyped.ml
+++ b/backend/cn/wellTyped.ml
@@ -585,7 +585,7 @@ module WIT = struct
          let@ t1 = infer loc t1 in
          pure begin
             let@ () = add_l name (IT.bt t1) (loc, lazy (Pp.string "let-var")) in
-            let@ () = add_c (LC.t_ (IT.def_ name t1)) in
+            let@ () = add_c loc (LC.t_ (IT.def_ name t1)) in
             let@ t2 = infer loc t2 in
             return (IT (Let ((name, t1), t2), IT.bt t2))
             end
@@ -759,7 +759,7 @@ module WLRT = struct
          (* let s, lrt = LRT.alpha_rename (s, IT.bt it) lrt in *)
          let@ it = WIT.infer loc it in
          let@ () = add_l s (IT.bt it) (loc, lazy (Pp.string "let-var")) in
-         let@ () = add_c (LC.t_ (IT.def_ s it)) in
+         let@ () = add_c (fst info) (LC.t_ (IT.def_ s it)) in
          let@ lrt = aux lrt in
          return (Define ((s, it), info, lrt))
       | Resource ((s, (re, re_oa_spec)), info, lrt) -> 
@@ -773,7 +773,7 @@ module WLRT = struct
          return (Resource ((s, (re, re_oa_spec)), info, lrt))
       | Constraint (lc, info, lrt) ->
          let@ lc = WLC.welltyped (fst info) lc in
-         let@ () = add_c lc in
+         let@ () = add_c (fst info) lc in
          let@ lrt = aux lrt in
          return (Constraint (lc, info, lrt))
       | I -> 
@@ -831,7 +831,7 @@ module WLAT = struct
          (* let s, at = LAT.alpha_rename i_subst (s, IT.bt it) at in *)
          let@ it = WIT.infer loc it in
          let@ () = add_l s (IT.bt it) (loc, lazy (Pp.string "let-var")) in
-         let@ () = add_c (LC.t_ (IT.def_ s it)) in
+         let@ () = add_c (fst info) (LC.t_ (IT.def_ s it)) in
          let@ at = aux at in
          return (LAT.Define ((s, it), info, at))
       | LAT.Resource ((s, (re, re_oa_spec)), info, at) -> 
@@ -845,7 +845,7 @@ module WLAT = struct
          return (LAT.Resource ((s, (re, re_oa_spec)), info, at))
       | LAT.Constraint (lc, info, at) ->
          let@ lc = WLC.welltyped (fst info) lc in
-         let@ () = add_c lc in
+         let@ () = add_c (fst info) lc in
          let@ at = aux at in
          return (LAT.Constraint (lc, info, at))
       | LAT.I i -> 
@@ -929,7 +929,7 @@ module WLArgs = struct
          (* let s, at = LAT.alpha_rename i_subst (s, IT.bt it) at in *)
          let@ it = WIT.infer loc it in
          let@ () = add_l s (IT.bt it) (loc, lazy (Pp.string "let-var")) in
-         let@ () = add_c (LC.t_ (IT.def_ s it)) in
+         let@ () = add_c (fst info) (LC.t_ (IT.def_ s it)) in
          let@ at, typ = aux at in
          return (Mu.M_Define ((s, it), info, at), 
                  LAT.Define ((s, it), info, typ))
@@ -945,7 +945,7 @@ module WLArgs = struct
                  LAT.Resource ((s, (re, re_oa_spec)), info, typ))
       | Mu.M_Constraint (lc, info, at) ->
          let@ lc = WLC.welltyped (fst info) lc in
-         let@ () = add_c lc in
+         let@ () = add_c (fst info) lc in
          let@ at, typ = aux at in
          return (Mu.M_Constraint (lc, info, at),
                  LAT.Constraint (lc, info, typ))
@@ -1042,8 +1042,8 @@ module WRPD = struct
                    let@ guard = WIT.check loc BT.Bool guard in
                    let negated_guards = List.map (fun clause -> IT.not_ clause.guard) acc in
                    pure begin 
-                       let@ () = add_c (LC.t_ guard) in
-                       let@ () = add_c (LC.t_ (IT.and_ negated_guards)) in
+                       let@ () = add_c loc (LC.t_ guard) in
+                       let@ () = add_c loc (LC.t_ (IT.and_ negated_guards)) in
                        let@ packing_ft = 
                          WLAT.welltyped IT.subst (fun loc it -> WIT.check loc pd.oarg_bt it)
                            "clause" loc packing_ft