diff --git a/src/dune b/src/dune
index 9893c20b5..92c2c7a87 100644
--- a/src/dune
+++ b/src/dune
@@ -95,7 +95,9 @@
    -g
    ;-dsource
    -warn-error
-   -3-5@8-11-14-33-20-21-26-27-39))
+   -3-5@8-11-14-33-20-21-26-27-39
+   -w
+   -30))
  (release
   (flags
    :standard
@@ -103,4 +105,6 @@
    -g
    ;-dsource
    -warn-error
-   -3-5@8-11-14-33-20-21-26-27-39)))
+   -3-5@8-11-14-33-20-21-26-27-39
+   -w
+   -30)))
diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index fe2933dc4..bdd8bfdd5 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -230,18 +230,23 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
-    List.map (fun ty -> mk_fresh_symbolic_value span ty) inst_sg.inputs
+    List.map
+      (fun ty -> mk_fresh_symbolic_value span (erase_regions ty))
+      inst_sg.inputs
   in
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let call_id = fresh_fun_call_id () in
   sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) span;
-  let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
+  let compute_abs_avalues (regions : region_id_set) (ctx : eval_ctx) :
       eval_ctx * typed_avalue list =
     (* Project over the values - we use *loan* projectors, as explained above *)
     let avalues =
       List.map
         (fun (sv : symbolic_value) ->
-          mk_aproj_loans_value_from_symbolic_value abs.regions.owned sv sv.sv_ty)
+          let proj_ty =
+            InterpreterBorrowsCore.normalize_proj_ty regions sv.sv_ty
+          in
+          mk_aproj_loans_value_from_symbolic_value sv proj_ty)
         input_svs
     in
     (ctx, avalues)
@@ -338,11 +343,14 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   let ctx =
     if is_regular_return then (
       let ret_value = Option.get ret_value in
-      let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
+      let compute_abs_avalues (regions : region_id_set) (ctx : eval_ctx) :
           eval_ctx * typed_avalue list =
+        (* Normalize the projection type *)
+        let ret_rty =
+          InterpreterBorrowsCore.normalize_proj_ty regions ret_rty
+        in
         let ctx, avalue =
-          apply_proj_borrows_on_input_value config span ctx abs.regions.owned
-            abs.regions.ancestors ret_value ret_rty
+          apply_proj_borrows_on_input_value config span ctx ret_value ret_rty
         in
         (ctx, [ avalue ])
       in
diff --git a/src/interp/InterpreterBorrows.ml b/src/interp/InterpreterBorrows.ml
index e827191f5..749fa63aa 100644
--- a/src/interp/InterpreterBorrows.ml
+++ b/src/interp/InterpreterBorrows.ml
@@ -200,8 +200,7 @@ let end_borrow_get_borrow (span : Meta.span)
                * of the two cases described above *)
               ABottom)
             else super#visit_ABorrow outer bc
-        | AIgnoredMutBorrow (_, _)
-        | AEndedMutBorrow _
+        | AIgnoredMutBorrow _ | AEndedMutBorrow _
         | AEndedIgnoredMutBorrow
             { given_back = _; child = _; given_back_meta = _ }
         | AEndedSharedBorrow ->
@@ -252,7 +251,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
     (not (concrete_loans_in_value nv))
     span "Can not end a borrow because the value to give back contains bottom";
   exec_assert __FILE__ __LINE__
-    (not (bottom_in_value ctx.ended_regions nv))
+    (not (bottom_in_value span ctx nv))
     span "Can not end a borrow because the value to give back contains bottom";
   (* Debug *)
   log#ltrace
@@ -326,7 +325,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
 
       (** We need to inspect ignored mutable borrows, to insert loan projectors
           if necessary. *)
-      method visit_typed_ABorrow (opt_abs : abs option) (ty : rty)
+      method visit_typed_ABorrow (opt_abs : abs option) (ty : proj_ty)
           (bc : aborrow_content) : avalue =
         match bc with
         | AIgnoredMutBorrow (bid', child) ->
@@ -336,7 +335,6 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
                * and the given back value is thus a symbolic value *)
               match nv.value with
               | VSymbolic sv ->
-                  let abs = Option.get opt_abs in
                   (* Remember the given back value as a meta-value
                    * TODO: it is a bit annoying to have to deconstruct
                    * the value... Think about a more elegant way. *)
@@ -344,8 +342,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
                   (* The loan projector *)
                   let _, ty, _ = ty_as_ref ty in
                   let given_back =
-                    mk_aproj_loans_value_from_symbolic_value abs.regions.owned
-                      sv ty
+                    mk_aproj_loans_value_from_symbolic_value sv ty
                   in
                   (* Continue giving back in the child value *)
                   let child = super#visit_typed_avalue opt_abs child in
@@ -363,20 +360,12 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
 
       (** We are not specializing an already existing method, but adding a new
           method (for projections, we need type information) *)
-      method visit_typed_ALoan (opt_abs : abs option) (ty : rty)
+      method visit_typed_ALoan (opt_abs : abs option) (ty : proj_ty)
           (lc : aloan_content) : avalue =
-        (* Preparing a bit *)
-        let regions, ancestors_regions =
-          match opt_abs with
-          | None -> craise __FILE__ __LINE__ span "Unreachable"
-          | Some abs -> (abs.regions.owned, abs.regions.ancestors)
-        in
         (* Rk.: there is a small issue with the types of the aloan values.
          * See the comment at the level of definition of {!typed_avalue} *)
-        let borrowed_value_aty =
-          let _, ty, _ = ty_get_ref ty in
-          ty
-        in
+        let _, borrowed_value_aty, _ = ty_get_ref ty in
+
         match lc with
         | AMutLoan (pm, bid', child) ->
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
@@ -391,7 +380,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
               (* Apply the projection *)
               let given_back =
                 apply_proj_borrows span check_symbolic_no_ended ctx
-                  fresh_reborrow regions ancestors_regions nv borrowed_value_aty
+                  fresh_reborrow nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
@@ -419,7 +408,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
                * (i.e., we don't call {!set_replaced}) *)
               let given_back =
                 apply_proj_borrows span check_symbolic_no_ended ctx
-                  fresh_reborrow regions ancestors_regions nv borrowed_value_aty
+                  fresh_reborrow nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
@@ -453,90 +442,69 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
     Because doing this introduces a fresh symbolic value which may contain
     borrows, we may need to update the proj_borrows to introduce loan projectors
     over those borrows. *)
-let end_aproj_borrows (span : Meta.span) (ended_regions : RegionId.Set.t)
-    (proj_ty : rty) (sv_id : symbolic_value_id) (nsv : symbolic_value)
-    (ctx : eval_ctx) : eval_ctx =
+let end_aproj_borrows (span : Meta.span) (proj : symbolic_proj)
+    (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
-  sanity_check __FILE__ __LINE__ (sv_id <> nsv.sv_id && ty_is_rty proj_ty) span;
+  sanity_check __FILE__ __LINE__ (proj.sv_id <> nsv.sv_id) span;
   log#ltrace
     (lazy
-      ("end_aproj_borrows:" ^ "\n- ended regions: "
-      ^ RegionId.Set.to_string None ended_regions
-      ^ "\n- projection type: " ^ ty_to_string ctx proj_ty ^ "\n- sv: "
-      ^ symbolic_value_id_to_pretty_string sv_id
+      ("end_aproj_borrows:" ^ "\n- projection type: "
+      ^ ty_to_string ctx proj.proj_ty
+      ^ "\n- sv: "
+      ^ symbolic_value_id_to_pretty_string proj.sv_id
       ^ "\n- nsv: "
       ^ symbolic_value_to_string ctx nsv
       ^ "\n- ctx: " ^ eval_ctx_to_string ctx));
   (* Substitution functions, to replace the borrow projectors over symbolic values *)
-  (* We need to handle two cases:
-     - If the regions ended in the symbolic value intersect with the owned
-       regions of the abstraction (not the ancestor ones): we can simply end the
-       borrow projector, there is nothing left to track anymore.
-
-       Ex.: we are ending abs1 below:
-       {[
-         abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
-         abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
-       ]}
-     - if the regions ended in the symbolic value intersect with the ancestors
-       regions of the abstraction, we have to introduce a projection
-       (because it means we ended ancestor "outer" borrows, and so we need
-       to project the given back inner loans into the abstraction).
-
-       Ex.: we are ending abs2 below, and considering abs1: we have to project
-       the inner loans inside of abs3. However we do not project anything
-       into abs2 (see the case above).
-       {[
-         abs0 {'a} { AProjLoans (s0 : &'a mut &'b mut T) [] }
-         abs1 {'b} { AProjLoans (s0 : &'a mut &'b mut T) [] }
-         abs2 {'c} { AProjBorrows (s0 : &'a mut &'b mut T <: &'c mut T &'d mut T) }
-         abs3 {'d} { AProjBorrows (s0 : &'a mut &'b mut T <: &'c mut T &'d mut T) }
-       ]}
-
-     We proceed in two steps:
-     - we first update when intersecting with ancestors regions
-     - then we update when intersecting with owned regions
+  (* See the comments about [AProjLoans], we have to update in two situations:
+     - if the projection over the symbolic value intersects the borrow projector:
+       this is because we are ending exactly this borrow projector, so we need
+       to end it.
+     - if the *outlive* projection intersects the borrow projector: we need to
+       project the inner loans of the given back value.
   *)
-  let update_ancestors (_abs : abs) (abs_sv_id : symbolic_value_id)
-      (abs_proj_ty : rty) (local_given_back : (msymbolic_value_id * aproj) list)
-      : aproj =
-    (* Compute the projection over the given back value *)
-    let child_proj = AProjLoans (nsv.sv_id, abs_proj_ty, []) in
-    AProjBorrows
-      (abs_sv_id, abs_proj_ty, (sv_id, child_proj) :: local_given_back)
-  in
-  let ctx =
-    update_intersecting_aproj_borrows span ~fail_if_unchanged:false
-      ~include_ancestors:true ~include_owned:false ~update_shared:None
-      ~update_mut:update_ancestors ended_regions sv_id proj_ty ctx
-  in
-  let update_owned (_abs : abs) (_abs_sv_id : symbolic_value_id)
-      (_abs_proj_ty : rty)
-      (local_given_back : (msymbolic_value_id * aproj) list) : aproj =
-    (* There is nothing to project *)
-    let mvalues = { consumed = sv_id; given_back = nsv } in
-    AEndedProjBorrows (mvalues, local_given_back)
+  let update_mut ~owned ~outlive (_abs : abs) (aproj : aproj_borrows) : aproj =
+    (* We can be in one case, or the other, but not both *)
+    sanity_check __FILE__ __LINE__ ((not owned) || not outlive) span;
+
+    if owned then
+      (* There is nothing to project *)
+      let mvalues = { consumed = proj.sv_id; given_back = nsv } in
+      AEndedProjBorrows { mvalues; loans = aproj.loans }
+    else
+      (* Compute the projection over the given back value (we project the loans) *)
+      let loan =
+        AProjLoans
+          {
+            proj = { aproj.proj with sv_id = nsv.sv_id };
+            consumed = [];
+            borrows = [];
+          }
+      in
+      let consumed : mconsumed_symb =
+        { sv_id = nsv.sv_id; proj_ty = proj.proj_ty }
+      in
+      AProjBorrows { proj; loans = (consumed, loan) :: aproj.loans }
   in
   update_intersecting_aproj_borrows span ~fail_if_unchanged:true
-    ~include_ancestors:false ~include_owned:true ~update_shared:None
-    ~update_mut:update_owned ended_regions sv_id proj_ty ctx
+    ~include_owned:true ~include_outlive:true ~update_shared:None ~update_mut
+    proj ctx
 
 (** Give back a *modified* symbolic value. *)
 let give_back_symbolic_value (_config : config) (span : Meta.span)
-    (ended_regions : RegionId.Set.t) (proj_ty : rty) (sv_id : symbolic_value_id)
-    (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
+    (proj : symbolic_proj) (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
-  sanity_check __FILE__ __LINE__ (sv_id <> nsv.sv_id && ty_is_rty proj_ty) span;
+  sanity_check __FILE__ __LINE__ (proj.sv_id <> nsv.sv_id) span;
   (* Substitution functions, to replace the borrow projectors over symbolic values *)
   (* We need to handle two cases:
      - If the regions ended in the symbolic value intersect with the owned
        regions of the abstraction (not the ancestor ones): we can simply end the
-       loan, there is nothing left to track anymore.
+       loan as there is nothing left to track anymore.
 
        Ex.: we are ending abs1 below:
        {[
          abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
-         abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+         abs1 {'b} { AProjBorrows (s0 : &'b mut T) }
        ]}
      - if the regions ended in the symbolic value intersect with the ancestors
        regions of the abstraction, we have to introduce a projection
@@ -547,35 +515,41 @@ let give_back_symbolic_value (_config : config) (span : Meta.span)
        Ex.: we are ending abs2 below, and considering abs1: we have to project
        the inner borrows inside of abs1. However we do not project anything
        into abs0 (see the case above).
+
        {[
-         abs0 {'a} { AProjLoans (s0 : &'a mut &'b mut T) [] }
-         abs1 {'b} { AProjLoans (s0 : &'a mut &'b mut T) [] }
-         abs2 {'c} { AProjBorrows (s0 : &'a mut &'b mut T <: &'c mut T &'d mut T) }
-         abs3 {'d} { AProjBorrows (s0 : &'a mut &'b mut T <: &'c mut T &'d mut T) }
+         abs0 {'a} { AProjLoans (s0 : &'a mut &'_ mut T) [] }
+         abs1 {'b} { AProjLoans (s0 : &'_ mut &'b mut T) [] }
+         abs2 {'c} { AProjBorrows (s0 : &'c mut &'_ mut T) }
+         abs3 {'d} { AProjBorrows (s0 : &'_ mut &'d mut T) }
        ]}
 
      We proceed in two steps:
      - we first update when intersecting with ancestors regions
      - then we update when intersecting with owned regions
   *)
-  let subst_ancestors (_abs : abs) abs_sv abs_proj_ty local_given_back =
-    (* Compute the projection over the given back value *)
-    let child_proj = AProjBorrows (nsv.sv_id, abs_proj_ty, []) in
-    AProjLoans (abs_sv, abs_proj_ty, (sv_id, child_proj) :: local_given_back)
-  in
-  let ctx =
-    update_intersecting_aproj_loans span ~fail_if_unchanged:false
-      ~include_ancestors:true ~include_owned:false ended_regions proj_ty sv_id
-      subst_ancestors ctx
-  in
-  let subst_owned (_abs : abs) abs_sv abs_proj_ty local_given_back =
-    (* There is nothing to project *)
-    let child_proj = AEmpty in
-    AProjLoans (abs_sv, abs_proj_ty, (nsv.sv_id, child_proj) :: local_given_back)
+  let subst ~owned ~outlive (_abs : abs) (aproj : aproj_loans) =
+    sanity_check __FILE__ __LINE__ ((not owned) || not outlive) span;
+    if owned then
+      (* There is nothing to project *)
+      let child_proj = AEmpty in
+      let consumed : mconsumed_symb =
+        { sv_id = nsv.sv_id; proj_ty = aproj.proj.proj_ty }
+      in
+      AProjLoans
+        { aproj with consumed = (consumed, child_proj) :: aproj.consumed }
+    else
+      (* Compute the projection over the given back value *)
+      let borrow =
+        AProjBorrows
+          { proj = { aproj.proj with sv_id = nsv.sv_id }; loans = [] }
+      in
+      let consumed : mconsumed_symb =
+        { sv_id = nsv.sv_id; proj_ty = proj.proj_ty }
+      in
+      AProjLoans { aproj with borrows = (consumed, borrow) :: aproj.borrows }
   in
   update_intersecting_aproj_loans span ~fail_if_unchanged:true
-    ~include_ancestors:false ~include_owned:true ended_regions proj_ty sv_id
-    subst_owned ctx
+    ~include_owned:true ~include_outlive:true proj subst ctx
 
 (** Auxiliary function to end borrows. See {!give_back}.
 
@@ -1147,16 +1121,6 @@ and end_abstraction_aux (config : config) (span : Meta.span)
         comp cc (end_abstraction_borrows config span chain abs_id ctx)
       in
 
-      (* End the regions owned by the abstraction - note that we don't need to
-         relookup the abstraction: the set of regions in an abstraction never
-         changes... *)
-      let ctx =
-        let ended_regions =
-          RegionId.Set.union ctx.ended_regions abs.regions.owned
-        in
-        { ctx with ended_regions }
-      in
-
       (* Remove all the references to the id of the current abstraction, and remove
          the abstraction itself.
          **Rk.**: this is where we synthesize the updated symbolic AST *)
@@ -1222,13 +1186,10 @@ and end_abstraction_loans (config : config) (span : Meta.span)
       in
       (* Reexplore, looking for loans *)
       comp cc (end_abstraction_loans config span chain abs_id ctx)
-  | Some (SymbolicValue (sv, proj_ty)) ->
+  | Some (SymbolicValue proj) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
          which intersect this proj_loans, then end the proj_loans itself *)
-      let ctx, cc =
-        end_proj_loans_symbolic config span chain abs_id abs.regions.owned sv
-          proj_ty ctx
-      in
+      let ctx, cc = end_proj_loans_symbolic config span chain abs_id proj ctx in
       (* Reexplore, looking for loans *)
       comp cc (end_abstraction_loans config span chain abs_id ctx)
 
@@ -1289,8 +1250,7 @@ and end_abstraction_borrows (config : config) (span : Meta.span)
       method! visit_aproj env sproj =
         (match sproj with
         | AProjLoans _ -> craise __FILE__ __LINE__ span "Unexpected"
-        | AProjBorrows (sv, proj_ty, given_back) ->
-            raise (FoundAProjBorrows (sv, proj_ty, given_back))
+        | AProjBorrows aproj_borrows -> raise (FoundAProjBorrows aproj_borrows)
         | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ());
         super#visit_aproj env sproj
 
@@ -1344,7 +1304,7 @@ and end_abstraction_borrows (config : config) (span : Meta.span)
                 (fun asb ->
                   match asb with
                   | AsbBorrow bid -> Some bid
-                  | AsbProjReborrows (_, _) -> None)
+                  | AsbProjReborrows _ -> None)
                 asb
             in
             (* There should be at least one borrow identifier in the set, which we
@@ -1368,20 +1328,19 @@ and end_abstraction_borrows (config : config) (span : Meta.span)
       (* Reexplore *)
       end_abstraction_borrows config span chain abs_id ctx
   (* There are symbolic borrows: end them, then reexplore *)
-  | FoundAProjBorrows (sv, proj_ty, given_back) ->
+  | FoundAProjBorrows aproj ->
       log#ltrace
         (lazy
           ("end_abstraction_borrows: found aproj borrows: "
-          ^ aproj_to_string ctx (AProjBorrows (sv, proj_ty, given_back))));
+          ^ aproj_to_string ctx (AProjBorrows aproj)));
       (* Generate a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_value span proj_ty in
+      let nsv =
+        mk_fresh_symbolic_value span (erase_regions aproj.proj.proj_ty)
+      in
       (* Replace the proj_borrows - there should be exactly one *)
-      let ctx = end_aproj_borrows span abs.regions.owned proj_ty sv nsv ctx in
+      let ctx = end_aproj_borrows span aproj.proj nsv ctx in
       (* Give back the symbolic value *)
-      let ctx =
-        give_back_symbolic_value config span abs.regions.owned proj_ty sv nsv
-          ctx
-      in
+      let ctx = give_back_symbolic_value config span aproj.proj nsv ctx in
       (* Reexplore *)
       end_abstraction_borrows config span chain abs_id ctx
   (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
@@ -1444,34 +1403,29 @@ and end_abstraction_remove_from_context (_config : config) (span : Meta.span)
       here. *)
 and end_proj_loans_symbolic (config : config) (span : Meta.span)
     (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id)
-    (regions : RegionId.Set.t) (sv_id : symbolic_value_id) (proj_ty : rty) :
-    cm_fun =
+    (proj : symbolic_proj) : cm_fun =
  fun ctx ->
   log#ltrace
     (lazy
       ("end_proj_loans_symbolic:" ^ "\n- abs_id: "
       ^ AbstractionId.to_string abs_id
-      ^ "\n- regions: "
-      ^ RegionId.Set.to_string None regions
       ^ "\n- sv: "
-      ^ symbolic_value_id_to_pretty_string sv_id
-      ^ "\n- projection type: " ^ ty_to_string ctx proj_ty ^ "\n- ctx:\n"
-      ^ eval_ctx_to_string ctx));
+      ^ symbolic_value_id_to_pretty_string proj.sv_id
+      ^ "\n- projection type: "
+      ^ ty_to_string ctx proj.proj_ty
+      ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx));
   (* Small helpers for sanity checks *)
-  let check ctx = no_aproj_over_symbolic_in_context span sv_id ctx in
+  let check ctx = no_aproj_over_symbolic_in_context span proj.sv_id ctx in
   (* Find the first proj_borrows which intersects the proj_loans *)
   let explore_shared = true in
-  match
-    lookup_intersecting_aproj_borrows_opt span explore_shared regions sv_id
-      proj_ty ctx
-  with
+  match lookup_intersecting_aproj_borrows_opt span explore_shared proj ctx with
   | None ->
       (* We couldn't find any in the context: it means that the symbolic value
          is in the concrete environment (or that we dropped it, in which case
          it is completely absent). We thus simply need to replace the loans
          projector with an ended projector.
       *)
-      let ctx = update_aproj_loans_to_ended span abs_id sv_id ctx in
+      let ctx = update_aproj_loans_to_ended span abs_id proj.sv_id ctx in
       (* Sanity check *)
       check ctx;
       (* Continue *)
@@ -1520,11 +1474,11 @@ and end_proj_loans_symbolic (config : config) (span : Meta.span)
       let ctx =
         (* All the proj_borrows are owned: simply erase them *)
         let ctx =
-          remove_intersecting_aproj_borrows_shared span ~include_ancestors:false
-            ~include_owned:true regions sv_id proj_ty ctx
+          remove_intersecting_aproj_borrows_shared ~include_owned:true
+            ~include_outlive:false span proj ctx
         in
         (* End the loan itself *)
-        update_aproj_loans_to_ended span abs_id sv_id ctx
+        update_aproj_loans_to_ended span abs_id proj.sv_id ctx
       in
       (* Sanity check *)
       check ctx;
@@ -1572,9 +1526,7 @@ and end_proj_loans_symbolic (config : config) (span : Meta.span)
         let ctx, cc = end_abstraction_aux config span chain abs_id' ctx in
         (* Retry ending the projector of loans *)
         let ctx, cc =
-          comp cc
-            (end_proj_loans_symbolic config span chain abs_id regions sv_id
-               proj_ty ctx)
+          comp cc (end_proj_loans_symbolic config span chain abs_id proj ctx)
         in
         (* Sanity check *)
         check ctx;
@@ -1644,7 +1596,7 @@ let promote_shared_loan_to_mut_loan (span : Meta.span) (l : BorrowId.id)
       sanity_check __FILE__ __LINE__ (not (concrete_loans_in_value sv)) span;
       (* Check there isn't {!Bottom} (this is actually an invariant *)
       cassert __FILE__ __LINE__
-        (not (bottom_in_value ctx.ended_regions sv))
+        (not (bottom_in_value span ctx sv))
         span "There shouldn't be a bottom";
       (* Check there aren't reserved borrows *)
       cassert __FILE__ __LINE__
@@ -1718,7 +1670,7 @@ let rec promote_reserved_mut_borrow (config : config) (span : Meta.span)
               ^ typed_value_to_string ~span:(Some span) ctx sv));
           sanity_check __FILE__ __LINE__ (not (concrete_loans_in_value sv)) span;
           sanity_check __FILE__ __LINE__
-            (not (bottom_in_value ctx.ended_regions sv))
+            (not (bottom_in_value span ctx sv))
             span;
           sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) span;
           (* End the borrows which borrow from the value, at the exception of
@@ -1883,22 +1835,30 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
     | ASymbolic (_, aproj) -> (
         (* *)
         match aproj with
-        | AProjLoans (_, _, children) ->
+        | AProjLoans { proj = _; consumed; borrows } ->
             (* There can be children in the presence of nested borrows: we
                don't handle those for now. *)
-            sanity_check __FILE__ __LINE__ (children = []) span;
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
             push av
-        | AProjBorrows (_, _, children) ->
+        | AProjBorrows { proj = _; loans } ->
             (* For now, we fore all symbolic values containing borrows to be eagerly
                expanded *)
             (* There can be children in the presence of nested borrows: we
                don't handle those for now. *)
-            sanity_check __FILE__ __LINE__ (children = []) span;
+            sanity_check __FILE__ __LINE__ (loans = []) span;
             push av
-        | AEndedProjLoans (_, children) | AEndedProjBorrows (_, children) ->
+        | AEndedProjLoans { proj = _; consumed; borrows } ->
             (* There can be children in the presence of nested borrows: we
                don't handle those for now. *)
-            sanity_check __FILE__ __LINE__ (children = []) span;
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
+            (* Just ignore *)
+            ()
+        | AEndedProjBorrows { mvalues = _; loans } ->
+            (* There can be children in the presence of nested borrows: we
+               don't handle those for now. *)
+            sanity_check __FILE__ __LINE__ (loans = []) span;
             (* Just ignore *)
             ()
         | AEmpty -> ())
@@ -1942,6 +1902,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                   visitor#visit_typed_value () v
                 in
                 let sv = mk_value_with_fresh_sids sv in
+
                 (* Create the new avalue *)
                 let value =
                   ALoan
@@ -1949,11 +1910,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                 in
                 (* We need to update the type of the value: abstract shared loans
                    have the type `& ...` - TODO: this is annoying and not very clean... *)
-                let ty =
-                  (* Take the first region of the abstraction - this doesn't really matter *)
-                  let r = RegionId.Set.min_elt abs0.regions.owned in
-                  TRef (RVar (Free r), ty, RShared)
-                in
+                let ty = TRef (RVar (Free RegionId.zero), ty, RShared) in
                 { value; ty }
               in
               let avl = List.append [ av ] avl in
@@ -1997,7 +1954,7 @@ let find_first_endable_loan_proj_in_abs (span : Meta.span) (ctx : eval_ctx)
 
       method! visit_aproj env proj =
         match proj with
-        | AProjLoans (sv_id, proj_ty, _) ->
+        | AProjLoans proj ->
             (* Check if there are borrow projectors in the context
                or symbolic values with the same id *)
             let explore_shared = false in
@@ -2007,7 +1964,7 @@ let find_first_endable_loan_proj_in_abs (span : Meta.span) (ctx : eval_ctx)
                 inherit [_] iter_eval_ctx
 
                 method! visit_VSymbolic _ sv' =
-                  if sv'.sv_id = sv_id then raise Found else ()
+                  if sv'.sv_id = proj.proj.sv_id then raise Found else ()
               end
             in
             begin
@@ -2018,14 +1975,14 @@ let find_first_endable_loan_proj_in_abs (span : Meta.span) (ctx : eval_ctx)
                    borrow projectors *)
                 match
                   lookup_intersecting_aproj_borrows_opt span explore_shared
-                    abs.regions.owned sv_id proj_ty ctx
+                    proj.proj ctx
                 with
                 | None ->
                     (* No intersecting projections: we can end this loan projector *)
-                    raise (FoundAbsProj (abs.abs_id, sv_id))
+                    raise (FoundAbsProj (abs.abs_id, proj.proj.sv_id))
                 | Some _ ->
                     (* There are intersecting projections: we can't end this loan projector *)
-                    super#visit_aproj env proj
+                    super#visit_aproj env (AProjLoans proj)
               with Found -> ()
             end
         | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
@@ -2043,7 +2000,7 @@ let find_first_endable_loan_proj_in_abs (span : Meta.span) (ctx : eval_ctx)
 let abs_borrows_loans_in_fixed span (ctx : eval_ctx)
     (fixed_abs_ids : AbstractionId.Set.t) (abs : abs) : bool =
   (* Iterate through the loan projectors which intersect a given borrow projector *)
-  let visit_proj_loans (sid : symbolic_value_id) (proj_ty : rty) =
+  let visit_proj_loans (proj : symbolic_proj) =
     object
       inherit [_] iter_eval_ctx as super
 
@@ -2051,13 +2008,12 @@ let abs_borrows_loans_in_fixed span (ctx : eval_ctx)
         sanity_check __FILE__ __LINE__ (env = None) span;
         super#visit_abs (Some abs) abs
 
-      method! visit_AProjLoans env sid' proj_ty' children =
+      method! visit_AProjLoans env proj' =
         if
-          sid = sid'
-          && projections_intersect span proj_ty abs.regions.owned proj_ty'
-               (Option.get env).regions.owned
+          proj.sv_id = proj'.proj.sv_id
+          && norm_projections_intersect span proj.proj_ty proj'.proj.proj_ty
         then raise Found
-        else super#visit_AProjLoans env sid' proj_ty' children
+        else super#visit_AProjLoans env proj'
     end
   in
 
@@ -2096,8 +2052,8 @@ let abs_borrows_loans_in_fixed span (ctx : eval_ctx)
       method! visit_aproj env proj =
         super#visit_aproj env proj;
         match proj with
-        | AProjBorrows (sid, proj_ty, _) ->
-            (visit_proj_loans sid proj_ty)#visit_eval_ctx None ctx
+        | AProjBorrows proj ->
+            (visit_proj_loans proj.proj)#visit_eval_ctx None ctx
         | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ()
     end
   in
@@ -2244,7 +2200,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
   log#ltrace (lazy (__FUNCTION__ ^ ": " ^ typed_value_to_string ctx v));
   (* Convert the value to a list of avalues *)
   let absl = ref [] in
-  let push_abs (r_id : RegionId.id) (avalues : typed_avalue list) : unit =
+  let push_abs (avalues : typed_avalue list) : unit =
     if avalues = [] then ()
     else begin
       (* Create the abs - note that we keep the order of the avalues as it is
@@ -2264,11 +2220,6 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
           can_end;
           parents = AbstractionId.Set.empty;
           original_parents = [];
-          regions =
-            {
-              owned = RegionId.Set.singleton r_id;
-              ancestors = RegionId.Set.empty;
-            };
           avalues;
         }
       in
@@ -2281,6 +2232,9 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
     end
   in
 
+  (* The projection types are normalized, so we project following the region 0 *)
+  let r_id = RegionId.zero in
+
   (* [group]: group in one abstraction (because we dived into a borrow/loan)
 
      We return one typed-value for the shared values: when we encounter a shared
@@ -2288,8 +2242,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
      is [true], this shared value will be stripped of its shared loans.
   *)
   let rec to_avalues ~(allow_borrows : bool) ~(inside_borrowed : bool)
-      ~(group : bool) (r_id : RegionId.id) (v : typed_value) :
-      typed_avalue list * typed_value =
+      ~(group : bool) (v : typed_value) : typed_avalue list * typed_value =
     (* Debug *)
     log#ldebug
       (lazy
@@ -2312,7 +2265,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             let avl, field_values =
               List.split
                 (List.map
-                   (to_avalues ~allow_borrows ~inside_borrowed ~group r_id)
+                   (to_avalues ~allow_borrows ~inside_borrowed ~group)
                    adt.field_values)
             in
             (List.concat avl, field_values)
@@ -2321,11 +2274,10 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             let field_values =
               List.map
                 (fun fv ->
-                  let r_id = fresh_region_id () in
                   let avl, fv =
-                    to_avalues ~allow_borrows ~inside_borrowed ~group r_id fv
+                    to_avalues ~allow_borrows ~inside_borrowed ~group fv
                   in
-                  push_abs r_id avl;
+                  push_abs avl;
                   fv)
                 (* Slightly tricky: pay attention to the order in which the
                    abstractions are pushed (i.e.: the [List.rev] is important
@@ -2364,7 +2316,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
                because we don't support nested borrows for now) *)
             let avl, bv =
               to_avalues ~allow_borrows:false ~inside_borrowed:true ~group:true
-                r_id bv
+                bv
             in
             let value = { v with value = VBorrow (VMutBorrow (bid, bv)) } in
             (av :: avl, value)
@@ -2374,7 +2326,6 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
-            let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
             cassert __FILE__ __LINE__
               (not (value_has_borrows (Some span) ctx sv.value))
@@ -2385,11 +2336,12 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* We use [AIgnore] for the inner value *)
             let ignored = mk_aignored span ty None in
             (* For avalues, a loan has the type borrow (see the comments in [avalue]) *)
-            let ty = mk_ref_ty (RVar (Free r_id)) ty RShared in
+            let ref_ty = ty in
+            let ty = mk_ref_ty (RVar (Free r_id)) ref_ty RShared in
             (* Rem.: the shared value might contain loans *)
             let avl, sv =
               to_avalues ~allow_borrows:false ~inside_borrowed:true ~group:true
-                r_id sv
+                sv
             in
             let av = ALoan (ASharedLoan (PNone, bids, sv, ignored)) in
             let av = { value = av; ty } in
@@ -2408,7 +2360,8 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* We use [AIgnore] for the inner value *)
             let ignored = mk_aignored span ty in
             (* For avalues, a loan has the type borrow (see the comments in [avalue]) *)
-            let ty = mk_ref_ty (RVar (Free r_id)) ty RMut in
+            let ref_ty = ty in
+            let ty = mk_ref_ty (RVar (Free r_id)) ref_ty RMut in
             let av = ALoan (AMutLoan (PNone, bid, ignored None)) in
             let av = { value = av; ty } in
             ([ av ], v))
@@ -2424,7 +2377,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
            symbolic value is inside a mutable borrow for instance) check that
            none of the regions used by the symbolic value have ended. *)
         sanity_check __FILE__ __LINE__
-          (group || not (symbolic_value_has_ended_regions ctx.ended_regions sv))
+          (group || not (symbolic_value_contains_bottom span ctx sv))
           span;
 
         (* If we group the borrows: simply introduce a projector.
@@ -2446,28 +2399,29 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
               end
             in
             let ty = visitor#visit_ty () sv.sv_ty in
-            let nv = ASymbolic (PNone, AProjBorrows (sv.sv_id, ty, [])) in
+            let proj : symbolic_proj = { sv_id = sv.sv_id; proj_ty = ty } in
+            let nv = ASymbolic (PNone, AProjBorrows { proj; loans = [] }) in
             let nv : typed_avalue = { value = nv; ty } in
             ([ nv ], v)
         else
           (* Introduce one abstraction per live region *)
-          let regions, ty = refresh_live_regions_in_ty span ctx sv.sv_ty in
-          RegionId.Map.iter
-            (fun _ rid ->
-              let nv = ASymbolic (PNone, AProjBorrows (sv.sv_id, ty, [])) in
+          let tys = make_projections_for_erased_regions_in_ty span sv.sv_ty in
+          List.iter
+            (fun ty ->
+              let proj : symbolic_proj = { sv_id = sv.sv_id; proj_ty = ty } in
+              let nv = ASymbolic (PNone, AProjBorrows { proj; loans = [] }) in
               let nv : typed_avalue = { value = nv; ty } in
-              push_abs rid [ nv ])
-            regions;
+              push_abs [ nv ])
+            tys;
           ([], v)
   in
 
   (* Generate the avalues *)
-  let r_id = fresh_region_id () in
   let values, _ =
-    to_avalues ~allow_borrows:true ~inside_borrowed:false ~group:false r_id v
+    to_avalues ~allow_borrows:true ~inside_borrowed:false ~group:false v
   in
   (* Introduce an abstraction for the returned values *)
-  push_abs r_id values;
+  push_abs values;
   (* Return *)
   List.rev !absl
 
@@ -2505,8 +2459,7 @@ type merge_abstraction_info = {
     - all the borrows are destructured (for instance, shared loans can't contain
       shared loans). *)
 let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
-    (owned_regions : RegionId.Set.t) (avalues : typed_avalue list) :
-    merge_abstraction_info =
+    (avalues : typed_avalue list) : merge_abstraction_info =
   let loans : MarkedBorrowId.Set.t ref = ref MarkedBorrowId.Set.empty in
   let borrows : MarkedBorrowId.Set.t ref = ref MarkedBorrowId.Set.empty in
   let loan_projs = ref MarkedNormSymbProj.Set.empty in
@@ -2550,15 +2503,13 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
   let module PushSymbolic =
     Push (MarkedNormSymbProj.Set) (MarkedNormSymbProj.Map)
   in
-  let push_loan_proj pm sv_id proj_ty lc =
-    let norm_proj_ty = normalize_proj_ty owned_regions proj_ty in
-    let proj = { pm; sv_id; norm_proj_ty } in
+  let push_loan_proj pm (proj : symbolic_proj) lc =
+    let proj = { pm; sv_id = proj.sv_id; norm_proj_ty = proj.proj_ty } in
     PushSymbolic.push loan_projs lc loan_proj_to_content false borrow_loan_projs
       proj
   in
-  let push_borrow_proj pm sv_id proj_ty bc =
-    let norm_proj_ty = normalize_proj_ty owned_regions proj_ty in
-    let proj = { pm; sv_id; norm_proj_ty } in
+  let push_borrow_proj pm (proj : symbolic_proj) bc =
+    let proj = { pm; sv_id = proj.sv_id; norm_proj_ty = proj.proj_ty } in
     PushSymbolic.push borrow_projs bc borrow_proj_to_content true
       borrow_loan_projs proj
   in
@@ -2647,12 +2598,13 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
           | Abstract ty -> ty
         in
         match proj with
-        | AProjLoans (sv_id, proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
-            push_loan_proj pm sv_id proj_ty (ty, pm, proj)
-        | AProjBorrows (sv_id, proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
-            push_borrow_proj pm sv_id proj_ty (ty, pm, proj)
+        | AProjLoans { proj = proj'; consumed; borrows } ->
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
+            push_loan_proj pm proj' (ty, pm, proj)
+        | AProjBorrows { proj = proj'; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span;
+            push_borrow_proj pm proj' (ty, pm, proj)
         | AEndedProjLoans _ | AEndedProjBorrows _ ->
             craise __FILE__ __LINE__ span "Unreachable"
         | AEmpty -> ()
@@ -2745,44 +2697,34 @@ type merge_duplicates_funcs = {
   merge_aborrow_projs :
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_borrows ->
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_borrows ->
     typed_avalue;
       (** Parameters:
           - [ty0]
           - [pm0]
-          - [sv0]
-          - [proj_ty0]
-          - [children0]
+          - [proj0]
+          - [loans0]
           - [ty1]
           - [pm1]
-          - [sv1]
-          - [proj_ty1]
-          - [children1] *)
+          - [proj1]
+          - [loans1] *)
   merge_aloan_projs :
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_loans ->
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_loans ->
     typed_avalue;
       (** Parameters:
           - [ty0]
           - [pm0]
-          - [sv0]
-          - [proj_ty0]
-          - [children0]
+          - [proj0]
+          - [consumed0]
+          - [borrows0]
           - [ty1]
           - [pm1]
           - [sv1]
@@ -2839,8 +2781,13 @@ let typed_avalue_split_marker (span : Meta.span) (ctx : eval_ctx)
       if pm <> PNone then [ av ]
       else
         match proj with
-        | AProjLoans (_, _, children) | AProjBorrows (_, _, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
+        | AProjBorrows { proj = _; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span;
+            let mk_value pm = { av with value = ASymbolic (pm, proj) } in
+            mk_split mk_value
+        | AProjLoans { proj = _; consumed; borrows } ->
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
             let mk_value pm = { av with value = ASymbolic (pm, proj) } in
             mk_split mk_value
         | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
@@ -2912,7 +2859,7 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span)
     borrow_to_content = borrow_to_content0;
     borrow_proj_to_content = borrow_proj_to_content0;
   } =
-    compute_merge_abstraction_info span ctx abs0.regions.owned abs0.avalues
+    compute_merge_abstraction_info span ctx abs0.avalues
   in
 
   let {
@@ -2927,7 +2874,7 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span)
     borrow_to_content = borrow_to_content1;
     borrow_proj_to_content = borrow_proj_to_content1;
   } =
-    compute_merge_abstraction_info span ctx abs1.regions.owned abs1.avalues
+    compute_merge_abstraction_info span ctx abs1.avalues
   in
 
   (* Sanity check: no markers appear unless we allow merging duplicates.
@@ -3173,7 +3120,12 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span)
               (* This can happen only in case of nested borrows - a concrete
                  borrow can only happen inside a shared loan *)
               craise __FILE__ __LINE__ span "Unreachable"
-          | Abstract (ty, bc) -> { value = ABorrow bc; ty }
+          | Abstract (ty, bc) ->
+              cassert __FILE__ __LINE__
+                (not
+                   (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
+                span "Nested borrows are not supported yet";
+              { value = ABorrow bc; ty }
 
         let make_loan_value _ lc : marked_borrow_id list * typed_avalue =
           match lc with
@@ -3196,8 +3148,16 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span)
                     List.map (fun bid -> (pm, bid)) (BorrowId.Set.elements bids)
                   in
                   let lc = ASharedLoan (pm, bids, sv, child) in
+                  cassert __FILE__ __LINE__
+                    (not
+                       (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty))
+                    span "Nested borrows are not supported yet";
                   (marked_bids, { value = ALoan lc; ty })
               | AMutLoan (pm, bid, _) ->
+                  cassert __FILE__ __LINE__
+                    (not
+                       (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty))
+                    span "Nested borrows are not supported yet";
                   ([ (pm, bid) ], { value = ALoan lc; ty })
               | AEndedMutLoan _
               | AEndedSharedLoan _
@@ -3232,9 +3192,15 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span)
         let set_loan_as_merged = set_loan_proj_as_merged
 
         let make_borrow_value _ (ty, pm, proj) =
+          cassert __FILE__ __LINE__
+            (not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
+            span "Nested borrows are not supported yet";
           { value = ASymbolic (pm, proj); ty }
 
         let make_loan_value marked (ty, pm, proj) =
+          cassert __FILE__ __LINE__
+            (not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
+            span "Nested borrows are not supported yet";
           ([ marked ], { value = ASymbolic (pm, proj); ty })
       end)
   in
@@ -3259,8 +3225,7 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span)
     ]} *)
 let merge_abstractions_merge_markers (span : Meta.span)
     (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx)
-    (owned_regions : RegionId.Set.t) (avalues : typed_avalue list) :
-    typed_avalue list =
+    (avalues : typed_avalue list) : typed_avalue list =
   log#ltrace
     (lazy
       (__FUNCTION__ ^ ":\n- avalues:\n"
@@ -3281,7 +3246,7 @@ let merge_abstractions_merge_markers (span : Meta.span)
     loan_proj_to_content;
     borrow_proj_to_content;
   } =
-    compute_merge_abstraction_info span ctx owned_regions avalues
+    compute_merge_abstraction_info span ctx avalues
   in
 
   (* Utilities to accumulate the list of values resulting from the merge *)
@@ -3344,7 +3309,11 @@ let merge_abstractions_merge_markers (span : Meta.span)
     | Concrete (_, _) ->
         (* This can happen only in case of nested borrows, and should have been filtered during phase 1 *)
         craise __FILE__ __LINE__ span "Unreachable"
-    | Abstract (ty, bc) -> { value = ABorrow bc; ty }
+    | Abstract (ty, bc) ->
+        cassert __FILE__ __LINE__
+          (not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
+          span "Nested borrows are not supported yet";
+        { value = ABorrow bc; ty }
   in
 
   (* Recreates an avalue from a loan_content, and adds the set of loan ids as merged.
@@ -3359,12 +3328,18 @@ let merge_abstractions_merge_markers (span : Meta.span)
         | AMutLoan (_, id, _) -> set_loan_as_merged id
         | ASharedLoan (_, ids, _, _) -> set_loans_as_merged ids
         | _ -> craise __FILE__ __LINE__ span "Unreachable");
+        cassert __FILE__ __LINE__
+          (not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty))
+          span "Nested borrows are not supported yet";
         { value = ALoan bc; ty }
   in
 
   (* Recreates an avalue from a borrow projector. *)
   let avalue_from_borrow_proj ((ty, pm, proj) : ty * proj_marker * aproj) :
       typed_avalue =
+    cassert __FILE__ __LINE__
+      (not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
+      span "Nested borrows are not supported yet";
     { value = ASymbolic (pm, proj); ty }
   in
 
@@ -3372,6 +3347,9 @@ let merge_abstractions_merge_markers (span : Meta.span)
      See the comment in the loop below for a detailed explanation *)
   let avalue_from_loan_proj ((ty, pm, proj) : ty * proj_marker * aproj) :
       typed_avalue =
+    cassert __FILE__ __LINE__
+      (not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty))
+      span "Nested borrows are not supported yet";
     { value = ASymbolic (pm, proj); ty }
   in
 
@@ -3480,13 +3458,13 @@ let merge_abstractions_merge_markers (span : Meta.span)
       ((ty1, pm1, proj1) : ty * proj_marker * aproj) : typed_avalue =
     sanity_check __FILE__ __LINE__ (complementary_markers pm0 pm1) span;
     match (proj0, proj1) with
-    | AProjBorrows (sv0, proj_ty0, child0), AProjBorrows (sv1, proj_ty1, child1)
-      ->
+    | AProjBorrows proj0, AProjBorrows proj1 ->
         (* Sanity-check of the precondition *)
-        sanity_check __FILE__ __LINE__ (sv0 = sv1) span;
+        sanity_check __FILE__ __LINE__
+          (proj0.proj.sv_id = proj1.proj.sv_id)
+          span;
         (* Merge *)
-        (Option.get merge_funs).merge_aborrow_projs ty0 pm0 sv0 proj_ty0 child0
-          ty1 pm1 sv1 proj_ty1 child1
+        (Option.get merge_funs).merge_aborrow_projs ty0 pm0 proj0 ty1 pm1 proj1
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
@@ -3497,12 +3475,13 @@ let merge_abstractions_merge_markers (span : Meta.span)
       ((ty1, pm1, proj1) : ty * proj_marker * aproj) : typed_avalue =
     sanity_check __FILE__ __LINE__ (complementary_markers pm0 pm1) span;
     match (proj0, proj1) with
-    | AProjLoans (sv0, proj_ty0, child0), AProjLoans (sv1, proj_ty1, child1) ->
+    | AProjLoans proj0, AProjLoans proj1 ->
         (* Sanity-check of the precondition *)
-        sanity_check __FILE__ __LINE__ (sv0 = sv1) span;
+        sanity_check __FILE__ __LINE__
+          (proj0.proj.sv_id = proj1.proj.sv_id)
+          span;
         (* Merge *)
-        (Option.get merge_funs).merge_aloan_projs ty0 pm0 sv0 proj_ty0 child0
-          ty1 pm1 sv1 proj_ty1 child1
+        (Option.get merge_funs).merge_aloan_projs ty0 pm0 proj0 ty1 pm1 proj1
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
@@ -3683,9 +3662,8 @@ let merge_abstractions_merge_markers (span : Meta.span)
         let loan_content_to_ids ((_, pm, proj) : ty * proj_marker * aproj) :
             marked_norm_symb_proj =
           match proj with
-          | AProjLoans (sv_id, proj_ty, _) ->
-              let norm_proj_ty = normalize_proj_ty owned_regions proj_ty in
-              { pm; sv_id; norm_proj_ty }
+          | AProjLoans { proj; _ } ->
+              { pm; sv_id = proj.sv_id; norm_proj_ty = proj.proj_ty }
           | _ -> internal_error __FILE__ __LINE__ span
 
         let avalue_from_bc = avalue_from_borrow_proj
@@ -3745,15 +3723,6 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
       (AbstractionId.Set.of_list [ abs0.abs_id; abs1.abs_id ])
   in
   let original_parents = AbstractionId.Set.elements parents in
-  let regions =
-    let owned = RegionId.Set.union abs0.regions.owned abs1.regions.owned in
-    let ancestors =
-      RegionId.Set.diff
-        (RegionId.Set.union abs0.regions.ancestors abs1.regions.ancestors)
-        owned
-    in
-    { owned; ancestors }
-  in
 
   (* Phase 1: simplify the loans coming from the left abstraction with
      the borrows coming from the right abstraction. *)
@@ -3764,22 +3733,12 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
   (* Phase 2: we now remove markers, by merging pairs of the same element with
      different markers into one element. To do so, we linearly traverse the list
      of avalues created through the first phase. *)
-  let avalues =
-    merge_abstractions_merge_markers span merge_funs ctx regions.owned avalues
-  in
+  let avalues = merge_abstractions_merge_markers span merge_funs ctx avalues in
 
   (* Create the new abstraction *)
   let abs_id = fresh_abstraction_id () in
   let abs =
-    {
-      abs_id;
-      kind = abs_kind;
-      can_end;
-      parents;
-      original_parents;
-      regions;
-      avalues;
-    }
+    { abs_id; kind = abs_kind; can_end; parents; original_parents; avalues }
   in
 
   (* Sanity check *)
@@ -3787,13 +3746,6 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
   (* Return *)
   abs
 
-(** Merge the regions in a context to a single region *)
-let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id)
-    (rids : RegionId.Set.t) : eval_ctx =
-  let rsubst x = if RegionId.Set.mem x rids then rid else x in
-  let env = Substitute.env_subst_rids rsubst ctx.env in
-  { ctx with env }
-
 let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind)
     (can_end : bool) (merge_funs : merge_duplicates_funcs option)
     (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
@@ -3816,23 +3768,6 @@ let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind)
   let ctx = fst (ctx_subst_abs span ctx abs_id0 nabs) in
   let ctx = fst (ctx_remove_abs span ctx abs_id1) in
 
-  (* Merge all the regions from the abstraction into one (the first - i.e., the
-     one with the smallest id). Note that we need to do this in the whole
-     environment, as those regions may be referenced as ancestor regions by
-     the other abstractions, and may be present in symbolic values, etc. (this
-     is not the case if there are no nested borrows, but we anticipate).
-  *)
-  let ctx =
-    let regions = nabs.regions.owned in
-    (* Pick the first region id (this is the smallest) *)
-    let rid = RegionId.Set.min_elt regions in
-    (* If there is only one region, do nothing *)
-    if RegionId.Set.cardinal regions = 1 then ctx
-    else
-      let rids = RegionId.Set.remove rid regions in
-      ctx_merge_regions ctx rid rids
-  in
-
   (* Return *)
   (ctx, nabs.abs_id)
 
@@ -3896,7 +3831,7 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) (allow_markers : bool)
       | ASymbolic (pm, aproj) -> begin
           sanity_check __FILE__ __LINE__ (allow_markers || pm = PNone) span;
           match aproj with
-          | AProjLoans (sv_id, _, _) | AProjBorrows (sv_id, _, _) -> sv_id
+          | AProjLoans { proj; _ } | AProjBorrows { proj; _ } -> proj.sv_id
           | _ -> craise __FILE__ __LINE__ span "Unexpected"
         end
       | _ -> craise __FILE__ __LINE__ span "Unexpected"
diff --git a/src/interp/InterpreterBorrows.mli b/src/interp/InterpreterBorrows.mli
index db5e3a1a4..6b6d1eefa 100644
--- a/src/interp/InterpreterBorrows.mli
+++ b/src/interp/InterpreterBorrows.mli
@@ -159,10 +159,6 @@ val convert_value_to_abstractions :
   typed_value ->
   abs list
 
-(** See {!merge_into_abstraction}.
-
-    Rem.: it may be more idiomatic to have a functor, but this seems a bit
-    heavyweight, though. *)
 type merge_duplicates_funcs = {
   merge_amut_borrows :
     borrow_id ->
@@ -234,44 +230,34 @@ type merge_duplicates_funcs = {
   merge_aborrow_projs :
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_borrows ->
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_borrows ->
     typed_avalue;
       (** Parameters:
           - [ty0]
           - [pm0]
-          - [sv0]
-          - [proj_ty0]
-          - [children0]
+          - [proj0]
+          - [loans0]
           - [ty1]
           - [pm1]
-          - [sv1]
-          - [proj_ty1]
-          - [children1] *)
+          - [proj1]
+          - [loans1] *)
   merge_aloan_projs :
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_loans ->
     ty ->
     proj_marker ->
-    symbolic_value_id ->
-    ty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_loans ->
     typed_avalue;
       (** Parameters:
           - [ty0]
           - [pm0]
-          - [sv0]
-          - [proj_ty0]
-          - [children0]
+          - [proj0]
+          - [consumed0]
+          - [borrows0]
           - [ty1]
           - [pm1]
           - [sv1]
diff --git a/src/interp/InterpreterBorrowsCore.ml b/src/interp/InterpreterBorrowsCore.ml
index fc6882dde..edc2f44c7 100644
--- a/src/interp/InterpreterBorrowsCore.ml
+++ b/src/interp/InterpreterBorrowsCore.ml
@@ -34,7 +34,7 @@ type borrow_ids = Borrows of BorrowId.Set.t | Borrow of BorrowId.id
 
 type borrow_ids_or_proj_symbolic_value =
   | BorrowIds of borrow_ids
-  | SymbolicValue of symbolic_value_id * rty
+  | SymbolicValue of symbolic_proj
 [@@deriving show]
 
 exception FoundBorrowIds of borrow_ids
@@ -183,6 +183,12 @@ let projections_intersect (span : Meta.span) (ty1 : rty)
   in
   compare_rtys span default combine compare_regions ty1 ty2
 
+(** Check whether two normalized projection types intersect. *)
+let norm_projections_intersect (span : Meta.span) (ty1 : rty) (ty2 : rty) : bool
+    =
+  let regions = RegionId.Set.singleton RegionId.zero in
+  projections_intersect span ty1 regions ty2 regions
+
 (** Check if the first projection contains the second projection. We use this
     function when checking invariants.
 
@@ -266,8 +272,7 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
               raise (FoundGLoanContent (Abstract lc))
             else super#visit_ASharedLoan env pm bids v av
         | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-        | AEndedSharedLoan (_, _)
-        | AIgnoredMutLoan (_, _)
+        | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan
             { given_back = _; child = _; given_back_meta = _ }
         | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc
@@ -405,8 +410,7 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
             if BorrowId.Set.mem l bids then update ()
             else super#visit_ASharedLoan env pm bids v av
         | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-        | AEndedSharedLoan (_, _)
-        | AIgnoredMutLoan (_, _)
+        | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan
             { given_back = _; child = _; given_back_meta = _ }
         | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc
@@ -465,8 +469,7 @@ let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind)
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
             else super#visit_ASharedBorrow env pm bid
-        | AIgnoredMutBorrow (_, _)
-        | AEndedMutBorrow _
+        | AIgnoredMutBorrow _ | AEndedMutBorrow _
         | AEndedIgnoredMutBorrow
             { given_back = _; child = _; given_back_meta = _ }
         | AEndedSharedBorrow -> super#visit_aborrow_content env bc
@@ -677,13 +680,11 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool)
   | FoundBorrowContent bc -> Some (BorrowContent bc)
 
 let proj_borrows_intersects_proj_loans (span : Meta.span)
-    (proj_borrows : RegionId.Set.t * symbolic_value_id * rty)
-    (proj_loans : RegionId.Set.t * symbolic_value_id * rty) : bool =
-  let b_regions, b_sv_id, b_ty = proj_borrows in
-  let l_regions, l_sv_id, l_ty = proj_loans in
-  if b_sv_id = l_sv_id then
-    projections_intersect span l_ty l_regions b_ty b_regions
-  else false
+    (proj_borrows : symbolic_value_id * rty)
+    (proj_loans : symbolic_value_id * rty) : bool =
+  let b_sv_id, b_ty = proj_borrows in
+  let l_sv_id, l_ty = proj_loans in
+  if b_sv_id = l_sv_id then norm_projections_intersect span l_ty b_ty else false
 
 (** Result of looking up aproj_borrows which intersect a given aproj_loans in
     the context.
@@ -703,15 +704,14 @@ type looked_up_aproj_borrows =
   | SharedProjs of (AbstractionId.id * rty) list
 
 (** Lookup the aproj_borrows (including aproj_shared_borrows) over a symbolic
-    value which intersect a given set of regions.
+    value which intersect a given projection.
 
     [lookup_shared]: if [true] also explore projectors over shared values,
     otherwise ignore.
 
     This is a helper function. *)
 let lookup_intersecting_aproj_borrows_opt (span : Meta.span)
-    (lookup_shared : bool) (regions : RegionId.Set.t)
-    (sv_id : symbolic_value_id) (proj_ty : rty) (ctx : eval_ctx) :
+    (lookup_shared : bool) (proj : symbolic_proj) (ctx : eval_ctx) :
     looked_up_aproj_borrows option =
   let found : looked_up_aproj_borrows option ref = ref None in
   let set_non_shared ((id, ty) : AbstractionId.id * rty) : unit =
@@ -725,13 +725,13 @@ let lookup_intersecting_aproj_borrows_opt (span : Meta.span)
     | Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl))
     | Some (NonSharedProj _) -> craise __FILE__ __LINE__ span "Unreachable"
   in
-  let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty' =
+  let check_add_proj_borrows (is_shared : bool) abs proj' =
     if
       proj_borrows_intersects_proj_loans span
-        (abs.regions.owned, sv', proj_ty')
-        (regions, sv_id, proj_ty)
+        (proj'.sv_id, proj'.proj_ty)
+        (proj.sv_id, proj.proj_ty)
     then
-      let x = (abs.abs_id, proj_ty) in
+      let x = (abs.abs_id, proj.proj_ty) in
       if is_shared then add_shared x else set_non_shared x
     else ()
   in
@@ -750,18 +750,18 @@ let lookup_intersecting_aproj_borrows_opt (span : Meta.span)
           let abs = Option.get abs in
           match asb with
           | AsbBorrow _ -> ()
-          | AsbProjReborrows (sv_id', proj_ty) ->
+          | AsbProjReborrows proj' ->
               let is_shared = true in
-              check_add_proj_borrows is_shared abs sv_id' proj_ty
+              check_add_proj_borrows is_shared abs proj'
         else ()
 
       method! visit_aproj abs sproj =
         (let abs = Option.get abs in
          match sproj with
          | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ()
-         | AProjBorrows (sv', proj_rty, _) ->
+         | AProjBorrows { proj = proj'; _ } ->
              let is_shared = false in
-             check_add_proj_borrows is_shared abs sv' proj_rty);
+             check_add_proj_borrows is_shared abs proj');
         super#visit_aproj abs sproj
     end
   in
@@ -780,37 +780,28 @@ let lookup_intersecting_aproj_borrows_opt (span : Meta.span)
     Returns the id of the owning abstraction, and the projection type used in
     this abstraction. *)
 let lookup_intersecting_aproj_borrows_not_shared_opt (span : Meta.span)
-    (regions : RegionId.Set.t) (sv_id : symbolic_value_id) (proj_ty : rty)
-    (ctx : eval_ctx) : (AbstractionId.id * rty) option =
+    (proj : symbolic_proj) (ctx : eval_ctx) : (AbstractionId.id * rty) option =
   let lookup_shared = false in
-  match
-    lookup_intersecting_aproj_borrows_opt span lookup_shared regions sv_id
-      proj_ty ctx
-  with
+  match lookup_intersecting_aproj_borrows_opt span lookup_shared proj ctx with
   | None -> None
   | Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty)
   | _ -> craise __FILE__ __LINE__ span "Unexpected"
 
 (** Similar to {!lookup_intersecting_aproj_borrows_opt}, but updates the values.
 
-    This is a helper function: **it might break invariants**.
-
-    [include_ancestors]: when exploring an abstraction and computing projection
-    intersections, use the ancestor regions. [include_owned]: when exploring an
-    abstraction and computing projection intersections, use the owned regions.
-*)
+    This is a helper function: **it might break invariants**. *)
 let update_intersecting_aproj_borrows (span : Meta.span)
-    ~(fail_if_unchanged : bool) ~(include_ancestors : bool)
-    ~(include_owned : bool)
+    ~(fail_if_unchanged : bool) ~(include_owned : bool)
+    ~(include_outlive : bool)
     ~(update_shared :
-       (abs -> symbolic_value_id -> rty -> abstract_shared_borrows) option)
-    ~(update_mut :
+       (owned:bool ->
+       outlive:bool ->
        abs ->
-       symbolic_value_id ->
-       rty ->
-       (msymbolic_value_id * aproj) list ->
-       aproj) (proj_regions : RegionId.Set.t) (sv_id : symbolic_value_id)
-    (proj_ty : rty) (ctx : eval_ctx) : eval_ctx =
+       symbolic_proj ->
+       abstract_shared_borrows)
+       option)
+    ~(update_mut : owned:bool -> outlive:bool -> abs -> aproj_borrows -> aproj)
+    (proj : symbolic_proj) (ctx : eval_ctx) : eval_ctx =
   (* Small helpers for sanity checks *)
   let shared = ref None in
   let add_shared () =
@@ -825,23 +816,49 @@ let update_intersecting_aproj_borrows (span : Meta.span)
         craise __FILE__ __LINE__ span
           "Found unexpected intersecting proj_borrows"
   in
-  let check_proj_borrows is_shared abs sv' proj_ty' =
-    let intersect_regions =
-      let intersect_regions =
-        if include_ancestors then abs.regions.ancestors else RegionId.Set.empty
+  let check_proj_borrows is_shared (proj' : symbolic_proj) : bool * bool =
+    if proj.sv_id = proj'.sv_id then (
+      let intersects_owned =
+        norm_projections_intersect span proj'.proj_ty proj.proj_ty
       in
-      if include_owned then
-        RegionId.Set.union abs.regions.owned intersect_regions
-      else intersect_regions
-    in
-    if
-      proj_borrows_intersects_proj_loans span
-        (intersect_regions, sv', proj_ty')
-        (proj_regions, sv_id, proj_ty)
-    then (
-      if is_shared then add_shared () else set_non_shared ();
-      true)
-    else false
+
+      (* Sanity check: if the projectors use the same symbolic id and the projections
+         do not intersect, then the loan projector must intersect the outlive
+         projection type of the borrow projector.
+
+         For example:
+          1. Ex.: we are ending [abs1] below:
+          {[
+            abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+            abs1 {'b} { AProjBorrows (s0 : &'b mut T) }
+          ]}
+          we can end the loan projector in [abs0].
+
+          2. Ex.: we are ending [abs2] below, and considering [abs1]: we have to
+          project the inner borrows inside of [abs1]. However we do not project
+          anything into [abs0] (see the case above).
+          {[
+            abs0 {'a} { AProjLoans (s0 : &'a mut &'_ mut T) [] }
+            abs1 {'b} { AProjLoans (s0 : &'_ mut &'b mut T) [] }
+            abs2 {'c} { AProjBorrows (s0 : &'c mut &'_ mut T) }
+            abs3 {'d} { AProjBorrows (s0 : &'_ mut &'d mut T) }
+          ]}
+      *)
+      (if !Config.sanity_checks && not intersects_owned then
+         let outlive_proj_ty =
+           TypesAnalysis.compute_outlive_proj_ty (Some span)
+             ctx.type_ctx.type_decls proj.proj_ty
+         in
+         sanity_check __FILE__ __LINE__
+           (norm_projections_intersect span proj'.proj_ty outlive_proj_ty)
+           span);
+
+      let intersects_outlive = include_outlive && not intersects_owned in
+      let intersects_owned = include_owned && intersects_owned in
+      let intersects = intersects_owned || intersects_outlive in
+      if intersects then if is_shared then add_shared () else set_non_shared ();
+      (intersects_owned, intersects_outlive))
+    else (false, false)
   in
   (* The visitor *)
   let obj =
@@ -862,10 +879,11 @@ let update_intersecting_aproj_borrows (span : Meta.span)
                 =
               match asb with
               | AsbBorrow _ -> [ asb ]
-              | AsbProjReborrows (sv', proj_ty) ->
+              | AsbProjReborrows proj' ->
                   let is_shared = true in
-                  if check_proj_borrows is_shared abs sv' proj_ty then
-                    update_shared abs sv' proj_ty
+                  let owned, outlive = check_proj_borrows is_shared proj' in
+                  if owned || outlive then
+                    update_shared ~owned ~outlive abs proj'
                   else [ asb ]
             in
             List.concat (List.map update asb)
@@ -875,11 +893,11 @@ let update_intersecting_aproj_borrows (span : Meta.span)
         match sproj with
         | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
             super#visit_aproj abs sproj
-        | AProjBorrows (sv', proj_rty, given_back) ->
+        | AProjBorrows proj' ->
             let abs = Option.get abs in
             let is_shared = true in
-            if check_proj_borrows is_shared abs sv' proj_rty then
-              update_mut abs sv' proj_rty given_back
+            let owned, outlive = check_proj_borrows is_shared proj'.proj in
+            if owned || outlive then update_mut ~owned ~outlive abs proj'
             else super#visit_aproj (Some abs) sproj
     end
   in
@@ -899,12 +917,11 @@ let update_intersecting_aproj_borrows (span : Meta.span)
 
     This is a helper function: it might break invariants. *)
 let update_intersecting_aproj_borrows_mut (span : Meta.span)
-    ~(include_ancestors : bool) ~(include_owned : bool)
-    (proj_regions : RegionId.Set.t) (sv_id : symbolic_value_id) (proj_ty : rty)
+    ~(include_owned : bool) ~(include_outlive : bool) (proj : symbolic_proj)
     (nv : aproj) (ctx : eval_ctx) : eval_ctx =
   (* Small helpers *)
   let updated = ref false in
-  let update_mut _ _ _ _ =
+  let update_mut ~owned:_ ~outlive:_ _ _ =
     (* We can update more than one borrow! *)
     updated := true;
     nv
@@ -912,8 +929,7 @@ let update_intersecting_aproj_borrows_mut (span : Meta.span)
   (* Update *)
   let ctx =
     update_intersecting_aproj_borrows span ~fail_if_unchanged:true
-      ~include_ancestors ~include_owned ~update_shared:None ~update_mut
-      proj_regions sv_id proj_ty ctx
+      ~include_owned ~include_outlive ~update_shared:None ~update_mut proj ctx
   in
   (* Check that we updated at least once *)
   sanity_check __FILE__ __LINE__ !updated span;
@@ -925,16 +941,16 @@ let update_intersecting_aproj_borrows_mut (span : Meta.span)
 
     This is a helper function: it might break invariants. *)
 let remove_intersecting_aproj_borrows_shared (span : Meta.span)
-    ~(include_ancestors : bool) ~(include_owned : bool)
-    (regions : RegionId.Set.t) (sv_id : symbolic_value_id) (proj_ty : rty)
+    ~(include_owned : bool) ~(include_outlive : bool) (proj : symbolic_proj)
     (ctx : eval_ctx) : eval_ctx =
   (* Small helpers *)
-  let update_shared = Some (fun _ _ _ -> []) in
-  let update_mut _ _ = craise __FILE__ __LINE__ span "Unexpected" in
+  let update_shared = Some (fun ~owned:_ ~outlive:_ _ _ -> []) in
+  let update_mut ~owned:_ ~outlive:_ _ =
+    craise __FILE__ __LINE__ span "Unexpected"
+  in
   (* Update *)
-  update_intersecting_aproj_borrows span ~fail_if_unchanged:true
-    ~include_ancestors ~include_owned ~update_shared ~update_mut regions sv_id
-    proj_ty ctx
+  update_intersecting_aproj_borrows span ~include_owned ~include_outlive
+    ~fail_if_unchanged:true ~update_shared ~update_mut proj ctx
 
 (** Updates the proj_loans intersecting some projection.
 
@@ -959,36 +975,25 @@ let remove_intersecting_aproj_borrows_shared (span : Meta.span)
     Note that for sanity, this function checks that we update *at least* one
     projector of loans.
 
-    [proj_ty]: shouldn't contain erased regions.
-
     [subst]: takes as parameters the abstraction in which we perform the
-    substitution and the list of given back values at the projector of loans
-    where we perform the substitution (see the fields in {!Values.AProjLoans}).
-    Note that the symbolic value at this place is necessarily equal to [sv],
-    which is why we don't give it as parameters.
-
-    [include_ancestors]: when exploring an abstraction and computing projection
-    intersections, use the ancestor regions. [include_owned]: when exploring an
-    abstraction and computing projection intersections, use the owned regions.
-*)
+    substitution and the [aproj_loans].
+
+    [include_owned]: when exploring an abstraction and computing projection
+    intersections, use the owned regions.
+
+    [include_outlive]: when exploring an abstraction and computing projection
+    intersections, use the (inner) outlive regions. *)
 let update_intersecting_aproj_loans (span : Meta.span)
-    ~(fail_if_unchanged : bool) ~(include_ancestors : bool)
-    ~(include_owned : bool) (proj_regions : RegionId.Set.t) (proj_ty : rty)
-    (sv_id : symbolic_value_id)
-    (subst :
-      abs ->
-      symbolic_value_id ->
-      rty ->
-      (msymbolic_value_id * aproj) list ->
-      aproj) (ctx : eval_ctx) : eval_ctx =
-  (* *)
-  sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) span;
+    ~(fail_if_unchanged : bool) ~(include_owned : bool)
+    ~(include_outlive : bool) (proj : symbolic_proj)
+    (subst : owned:bool -> outlive:bool -> abs -> aproj_loans -> aproj)
+    (ctx : eval_ctx) : eval_ctx =
   (* Small helpers for sanity checks *)
   let updated = ref false in
-  let update abs abs_sv abs_proj_ty local_given_back : aproj =
+  let update ~owned ~outlive abs aproj_loans : aproj =
     (* Note that we can update more than once! *)
     updated := true;
-    subst abs abs_sv abs_proj_ty local_given_back
+    subst ~owned ~outlive abs aproj_loans
   in
   (* The visitor *)
   let obj =
@@ -1000,25 +1005,31 @@ let update_intersecting_aproj_loans (span : Meta.span)
         match sproj with
         | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
             super#visit_aproj abs sproj
-        | AProjLoans (abs_sv, abs_proj_ty, given_back) ->
+        | AProjLoans aproj_loans ->
             let abs = Option.get abs in
-            if sv_id = abs_sv then
-              let abs_regions = RegionId.Set.empty in
-              let abs_regions =
-                if include_ancestors then
-                  RegionId.Set.union abs.regions.ancestors abs_regions
-                else abs_regions
+            if proj.sv_id = aproj_loans.proj.sv_id then (
+              let owned =
+                norm_projections_intersect span proj.proj_ty
+                  aproj_loans.proj.proj_ty
               in
-              let abs_regions =
-                if include_owned then
-                  RegionId.Set.union abs.regions.owned abs_regions
-                else abs_regions
-              in
-              if
-                projections_intersect span proj_ty proj_regions abs_proj_ty
-                  abs_regions
-              then update abs abs_sv abs_proj_ty given_back
-              else super#visit_aproj (Some abs) sproj
+
+              (* Sanity check: if the symbolic ids are the same and the projection
+                 types don't intersect, then the borrow projection must intersect
+                 the outlive loan projection *)
+              (if !Config.sanity_checks && not owned then
+                 let outlive_proj_ty =
+                   TypesAnalysis.compute_outlive_proj_ty (Some span)
+                     ctx.type_ctx.type_decls proj.proj_ty
+                 in
+                 sanity_check __FILE__ __LINE__
+                   (norm_projections_intersect span outlive_proj_ty
+                      aproj_loans.proj.proj_ty)
+                   span);
+
+              let outlive = include_outlive && not owned in
+              let owned = include_owned && owned in
+
+              update ~owned ~outlive abs aproj_loans)
             else super#visit_aproj (Some abs) sproj
     end
   in
@@ -1040,7 +1051,7 @@ let update_intersecting_aproj_loans (span : Meta.span)
     corresponds to the couple (abstraction id, symbolic value). *)
 let lookup_aproj_loans_opt (span : Meta.span) (abs_id : AbstractionId.id)
     (sv_id : symbolic_value_id) (ctx : eval_ctx) :
-    (msymbolic_value_id * aproj) list option =
+    ((mconsumed_symb * aproj) list * (mconsumed_symb * aproj) list) option =
   (* Small helpers for sanity checks *)
   let found = ref None in
   let set_found x =
@@ -1060,10 +1071,10 @@ let lookup_aproj_loans_opt (span : Meta.span) (abs_id : AbstractionId.id)
         (match sproj with
         | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
             super#visit_aproj abs sproj
-        | AProjLoans (abs_sv, _, given_back) ->
+        | AProjLoans { proj = abs_proj; consumed; borrows } ->
             let abs = Option.get abs in
             sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span;
-            if abs_sv = sv_id then set_found given_back else ());
+            if abs_proj.sv_id = sv_id then set_found (consumed, borrows) else ());
         super#visit_aproj abs sproj
     end
   in
@@ -1074,7 +1085,7 @@ let lookup_aproj_loans_opt (span : Meta.span) (abs_id : AbstractionId.id)
 
 let lookup_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id)
     (sv_id : symbolic_value_id) (ctx : eval_ctx) :
-    (msymbolic_value_id * aproj) list =
+    (mconsumed_symb * aproj) list * (mconsumed_symb * aproj) list =
   Option.get (lookup_aproj_loans_opt span abs_id sv_id ctx)
 
 (** Helper function: might break invariants.
@@ -1106,10 +1117,10 @@ let update_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id)
         match sproj with
         | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
             super#visit_aproj abs sproj
-        | AProjLoans (abs_sv, _, _) ->
+        | AProjLoans { proj = abs_proj; _ } ->
             let abs = Option.get abs in
             sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span;
-            if abs_sv = sv_id then update ()
+            if abs_proj.sv_id = sv_id then update ()
             else super#visit_aproj (Some abs) sproj
     end
   in
@@ -1151,10 +1162,10 @@ let update_aproj_borrows (span : Meta.span) (abs_id : AbstractionId.id)
         match sproj with
         | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
             super#visit_aproj abs sproj
-        | AProjBorrows (abs_sv, _proj_ty, _given_back) ->
+        | AProjBorrows { proj = abs_proj; _ } ->
             let abs = Option.get abs in
             sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span;
-            if abs_sv = sv.sv_id then update ()
+            if abs_proj.sv_id = sv.sv_id then update ()
             else super#visit_aproj (Some abs) sproj
     end
   in
@@ -1177,9 +1188,9 @@ let update_aproj_loans_to_ended (span : Meta.span) (abs_id : AbstractionId.id)
     (sv_id : symbolic_value_id) (ctx : eval_ctx) : eval_ctx =
   (* Lookup the projector of loans *)
   match lookup_aproj_loans_opt span abs_id sv_id ctx with
-  | Some given_back ->
+  | Some (consumed, borrows) ->
       (* Create the new value for the projector *)
-      let nproj = AEndedProjLoans (sv_id, given_back) in
+      let nproj = AEndedProjLoans { proj = sv_id; consumed; borrows } in
       (* Insert it *)
       let ctx = update_aproj_loans span abs_id sv_id nproj ctx in
       (* Return *)
@@ -1198,8 +1209,9 @@ let no_aproj_over_symbolic_in_context (span : Meta.span)
       method! visit_aproj env sproj =
         (match sproj with
         | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ()
-        | AProjLoans (abs_sv, _, _) | AProjBorrows (abs_sv, _, _) ->
-            if abs_sv = sv_id then raise Found else ());
+        | AProjLoans { proj = abs_proj; _ }
+        | AProjBorrows { proj = abs_proj; _ } ->
+            if abs_proj.sv_id = sv_id then raise Found else ());
         super#visit_aproj env sproj
     end
   in
@@ -1232,8 +1244,8 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             raise (FoundBorrowIds (Borrows bids))
         | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-        | AEndedSharedLoan (_, _) -> super#visit_aloan_content env lc
-        | AIgnoredMutLoan (_, _) ->
+        | AEndedSharedLoan _ -> super#visit_aloan_content env lc
+        | AIgnoredMutLoan _ ->
             (* Ignore *)
             super#visit_aloan_content env lc
         | AEndedIgnoredMutLoan
@@ -1253,10 +1265,10 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
 
       method! visit_aproj env sproj =
         (match sproj with
-        | AProjBorrows (_, _, _)
-        | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ()
-        | AProjLoans (sv, ty, given_back) ->
-            raise (FoundAProjLoans (sv, ty, given_back)));
+        | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty ->
+            ()
+        | AProjLoans { proj; consumed; borrows } ->
+            raise (FoundAProjLoans { proj; consumed; borrows }));
         super#visit_aproj env sproj
     end
   in
@@ -1268,9 +1280,9 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
   with
   (* There are loans *)
   | FoundBorrowIds bids -> Some (BorrowIds bids)
-  | FoundAProjLoans (sv, proj_ty, _) ->
+  | FoundAProjLoans { proj; _ } ->
       (* There are loan projections over symbolic values *)
-      Some (SymbolicValue (sv, proj_ty))
+      Some (SymbolicValue proj)
 
 let lookup_shared_value_opt (span : Meta.span) (ctx : eval_ctx)
     (bid : BorrowId.id) : typed_value option =
@@ -1341,6 +1353,8 @@ type marked_norm_symb_proj = {
   pm : proj_marker;
   sv_id : symbolic_value_id;
   norm_proj_ty : ty;
+      (** TODO: rename to [proj_ty] (we are now using projection types
+          everywhere *)
 }
 [@@deriving show, ord]
 
@@ -1540,32 +1554,189 @@ let norm_proj_ty_contains span (ty1 : rty) (ty2 : rty) : bool =
   let set = RegionId.Set.singleton RegionId.zero in
   projection_contains span ty1 set ty2 set
 
-(** Refresh the live region ids appearing in a type, and return the new type
-    with the map from old regions to fresh regions. *)
-let refresh_live_regions_in_ty (span : Meta.span) (ctx : eval_ctx) (ty : rty) :
-    RegionId.id RegionId.Map.t * rty =
-  let regions = ref RegionId.Map.empty in
-
-  let get_region rid =
-    (* Introduce a fresh region, if the region is alive *)
-    if not (RegionId.Set.mem rid ctx.ended_regions) then (
-      match RegionId.Map.find_opt rid !regions with
-      | Some rid -> rid
-      | None ->
-          let nrid = fresh_region_id () in
-          regions := RegionId.Map.add rid nrid !regions;
-          nrid)
-    else rid
+(** Collect all the borrow projectors over a symbolic value and make their
+    union.
+
+    If there are no such borrow projectors in the context, we return [None]. *)
+let collect_symbolic_value_borrow_projectors (span : Meta.span) (ctx : eval_ctx)
+    (sv : symbolic_value) : ty option =
+  (* Collect the type projections *)
+  let types = ref [] in
+  let visitor =
+    object
+      inherit [_] iter_eval_ctx as super
+
+      method! visit_AProjBorrows env { proj; loans } =
+        if proj.sv_id = sv.sv_id then types := proj.proj_ty :: !types;
+        super#visit_AProjBorrows env { proj; loans }
+    end
   in
+  visitor#visit_eval_ctx () ctx;
+
+  (* Make the union of the types *)
+  match !types with
+  | [] -> None
+  | ty :: types ->
+      let ty = ref ty in
+      List.iter (fun ty' -> ty := norm_proj_tys_union span !ty ty') types;
+      (* *)
+      Some !ty
+
+(** Check whether a symbolic value contains bottom values or not (it can contain
+    bottom values if some of the borrows it contains have ended). *)
+let symbolic_value_contains_bottom (span : Meta.span) (ctx : eval_ctx)
+    (sv : symbolic_value) : bool =
+  (* Case disjunction on whether the symbolic value contains borrows or not *)
+  if not (symbolic_value_has_borrows (Some span) ctx sv) then false
+  else
+    (* We check this the following manner: we lookup all the borrow projectors
+       (the projectors in the region abstractions which project the borrows
+       contained in the symbolic value and not yet revealed) and join their projection
+       types. If the resulting type projects all the regions contained in the value
+       (i.e., there are no erased regions) it means that no borrows were ended
+       (because no borrow projector was ended) and thus the value doesn't contain
+       bottoms.
+    *)
+    (* Make the union of the borrow projectors *)
+    let ty = collect_symbolic_value_borrow_projectors span ctx sv in
+    (* Make the union of the types *)
+    match ty with
+    | None ->
+        (* The symbolic value contains borrows and we found no borrow projectors:
+           it means all the borrows have ended *)
+        true
+    | Some ty -> ty_has_erased_regions ty
+
+(** Check whether a symbolic value contains non ended borrows. *)
+let symbolic_value_contains_non_ended_borrows (span : Meta.span)
+    (ctx : eval_ctx) (sv : symbolic_value) : bool =
+  (* Case disjunction on whether the symbolic value contains borrows or not *)
+  if not (symbolic_value_has_borrows (Some span) ctx sv) then false
+  else
+    (* This is similar to [symbolic_value_contains_bottom] *)
+    (* Make the union of the borrow projectors *)
+    let ty = collect_symbolic_value_borrow_projectors span ctx sv in
+    match ty with
+    | None ->
+        (* The symbolic value contains borrows and we found no borrow projectors:
+         it means all the borrows have ended *)
+        false
+    | Some ty -> ty_has_free_regions ty
+
+let bottom_in_value_visitor (span : Meta.span) (ctx : eval_ctx) =
+  object
+    inherit [_] iter_typed_value
+    method! visit_VBottom _ = raise Found
+
+    method! visit_symbolic_value _ s =
+      if symbolic_value_contains_bottom span ctx s then raise Found else ()
+  end
+
+(** Check if a {!type:Values.value} contains [⊥].
+
+    Note that this function is very general: it also checks wether symbolic
+    values contain already ended regions. *)
+let bottom_in_value span ctx (v : typed_value) : bool =
+  let obj = bottom_in_value_visitor span ctx in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true
+
+let bottom_in_adt_value span ctx (v : adt_value) : bool =
+  let obj = bottom_in_value_visitor span ctx in
+  (* We use exceptions *)
+  try
+    obj#visit_adt_value () v;
+    false
+  with Found -> true
+
+let value_has_non_ended_borrows_or_loans span (ctx : eval_ctx) (v : value) :
+    bool =
+  let value_visitor =
+    object
+      inherit [_] iter_typed_value
+      method! visit_borrow_content _ _ = raise Found
+      method! visit_loan_content _ _ = raise Found
+
+      method! visit_symbolic_value _ sv =
+        if symbolic_value_contains_non_ended_borrows span ctx sv then
+          raise Found
+        else ()
+    end
+  in
+  (* We use exceptions *)
+  try
+    value_visitor#visit_value () v;
+    false
+  with Found -> true
+
+(** Auxiliary helper.
+
+    Given a type, introduce a list of projections over a subset of regions in
+    the type.
+
+    We handle two cases, controled by the option [erased]:
+    - if [erased] is [true], it means the type only has erased regions, in which
+      case we introduce a projection for every such region
+    - otherwise, it means we should introduce projections for all the *marked*
+      regions in the projection type *)
+let make_projections_for_ty_aux (span : Meta.span) (erased : bool) (ty : rty) :
+    ty list =
+  (* First, introduce one fresh free region per region to mask *)
+  let regions = ref RegionId.Set.empty in
+  let fresh_rid () =
+    let nrid = fresh_region_id () in
+    regions := RegionId.Set.add nrid !regions;
+    nrid
+  in
+
   let visitor =
     object
       inherit [_] map_ty
 
-      method! visit_RVar _ var =
-        match var with
-        | Free rid -> RVar (Free (get_region rid))
-        | Bound _ -> internal_error __FILE__ __LINE__ span
+      method! visit_region _ r =
+        match r with
+        | RErased -> if erased then RVar (Free (fresh_rid ())) else RErased
+        | RStatic -> RStatic
+        | RVar (Free _) ->
+            if erased then internal_error __FILE__ __LINE__ span
+            else RVar (Free (fresh_rid ()))
+        | RVar (Bound _) -> internal_error __FILE__ __LINE__ span
     end
   in
   let ty = visitor#visit_ty () ty in
-  (!regions, ty)
+
+  (* Introduce one projection type per region *)
+  let tys = ref [] in
+  RegionId.Set.iter
+    (fun rid ->
+      let subst_visitor =
+        object
+          inherit [_] map_ty
+
+          method! visit_region _ r =
+            match r with
+            | RErased ->
+                if erased then internal_error __FILE__ __LINE__ span
+                else RErased
+            | RVar (Bound _) -> internal_error __FILE__ __LINE__ span
+            | RStatic -> RStatic
+            | RVar (Free rid') ->
+                if rid = rid' then RVar (Free RegionId.zero) else RErased
+        end
+      in
+      let ty = subst_visitor#visit_ty () ty in
+      tys := ty :: !tys)
+    !regions;
+
+  !tys
+
+let make_projections_for_erased_regions_in_ty (span : Meta.span) (ty : rty) :
+    ty list =
+  make_projections_for_ty_aux span true ty
+
+let make_projections_for_marked_regions_in_ty (span : Meta.span) (ty : rty) :
+    ty list =
+  make_projections_for_ty_aux span false ty
diff --git a/src/interp/InterpreterExpansion.ml b/src/interp/InterpreterExpansion.ml
index 0c48bf44f..6e96bf49b 100644
--- a/src/interp/InterpreterExpansion.ml
+++ b/src/interp/InterpreterExpansion.ml
@@ -74,16 +74,16 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
           never happen *)
       method! visit_aproj current_abs aproj =
         (match aproj with
-        | AProjLoans (sv_id, _, _) | AProjBorrows (sv_id, _, _) ->
-            sanity_check __FILE__ __LINE__ (sv_id <> original_sv.sv_id) span
+        | AProjLoans { proj; _ } | AProjBorrows { proj; _ } ->
+            sanity_check __FILE__ __LINE__
+              (proj.sv_id <> original_sv.sv_id)
+              span
         | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ());
         super#visit_aproj current_abs aproj
 
       method! visit_ASymbolic current_abs pm aproj =
         sanity_check __FILE__ __LINE__ (pm = PNone) span;
         let current_abs = Option.get current_abs in
-        let proj_regions = current_abs.regions.owned in
-        let ancestors_regions = current_abs.regions.ancestors in
         (* Explore in depth first - we won't update anything: we simply
          * want to check we don't have to expand inner symbolic value *)
         match (aproj, proj_kind) with
@@ -92,30 +92,33 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
             (* Explore the given back values to make sure we don't have to expand
              * anything in there *)
             ASymbolic (pm, self#visit_aproj (Some current_abs) aproj)
-        | AProjLoans (sv_id, proj_ty, given_back), LoanProj ->
+        | AProjLoans { proj; consumed; borrows }, LoanProj ->
             (* Check if this is the symbolic value we are looking for *)
-            if sv_id = original_sv.sv_id then (
+            if proj.sv_id = original_sv.sv_id then (
               (* There mustn't be any given back values *)
-              sanity_check __FILE__ __LINE__ (given_back = []) span;
+              sanity_check __FILE__ __LINE__ (consumed = []) span;
+              (* Not sure what to do if the borrows are non empty: leaving
+                 this as a TODO *)
+              cassert __FILE__ __LINE__ (borrows = []) span "Unimplemented";
               (* Apply the projector *)
               let projected_value =
-                apply_proj_loans_on_symbolic_expansion span proj_regions
-                  ancestors_regions expansion original_sv.sv_ty proj_ty ctx
+                apply_proj_loans_on_symbolic_expansion span expansion
+                  proj.proj_ty ctx
               in
               (* Replace *)
               projected_value.value)
             else
               (* Not the searched symbolic value: nothing to do *)
               super#visit_ASymbolic (Some current_abs) pm aproj
-        | AProjBorrows (sv_id, proj_ty, given_back), BorrowProj ->
+        | AProjBorrows { proj; loans }, BorrowProj ->
             (* We should never expand a symbolic value which has consumed given
                back values (because then it means the symbolic value was consumed
                by region abstractions, and is thus inaccessible: such a value can't
                be expanded)
             *)
-            cassert __FILE__ __LINE__ (given_back = []) span "Unreachable";
+            cassert __FILE__ __LINE__ (loans = []) span "Unreachable";
             (* Check if this is the symbolic value we are looking for *)
-            if sv_id = original_sv.sv_id then
+            if proj.sv_id = original_sv.sv_id then
               (* Convert the symbolic expansion to a value on which we can
                * apply a projector (if the expansion is a reference expansion,
                * convert it to a borrow) *)
@@ -128,17 +131,14 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
               (* Apply the projector *)
               let projected_value =
                 apply_proj_borrows span check_symbolic_no_ended ctx
-                  fresh_reborrow proj_regions ancestors_regions expansion
-                  proj_ty
+                  fresh_reborrow expansion proj.proj_ty
               in
               (* Replace *)
               projected_value.value
             else
               (* Not the searched symbolic value: nothing to do *)
               super#visit_ASymbolic (Some current_abs) pm aproj
-        | AProjLoans _, BorrowProj
-        | AProjBorrows (_, _, _), LoanProj
-        | AEmpty, _ ->
+        | AProjLoans _, BorrowProj | AProjBorrows _, LoanProj | AEmpty, _ ->
             (* Nothing to do *)
             ASymbolic (pm, aproj)
     end
@@ -165,7 +165,7 @@ let apply_symbolic_expansion_to_avalues (config : config) (span : Meta.span)
 
     Simply replace the symbolic values (*not avalues*) in the context with a
     given value. Will break invariants if not used properly. *)
-let replace_symbolic_values (span : Meta.span) (at_most_once : bool)
+let replace_symbolic_values (span : Meta.span) ~(at_most_once : bool)
     (original_sv : symbolic_value) (nv : value) (ctx : eval_ctx) : eval_ctx =
   (* Count *)
   let replaced = ref false in
@@ -194,9 +194,8 @@ let apply_symbolic_expansion_non_borrow (config : config) (span : Meta.span)
     (expansion : symbolic_expansion) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
   let nv = symbolic_expansion_non_borrow_to_value span original_sv expansion in
-  let at_most_once = false in
   let ctx =
-    replace_symbolic_values span at_most_once original_sv nv.value ctx
+    replace_symbolic_values span ~at_most_once:false original_sv nv.value ctx
   in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
@@ -233,7 +232,7 @@ let compute_expanded_symbolic_non_builtin_adt_value (span : Meta.span)
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
     let field_values =
-      List.map (fun (ty : rty) -> mk_fresh_symbolic_value span ty) field_types
+      List.map (fun (ty : ty) -> mk_fresh_symbolic_value span ty) field_types
     in
     let see = SeAdt (variant_id, field_values) in
     see
@@ -242,7 +241,7 @@ let compute_expanded_symbolic_non_builtin_adt_value (span : Meta.span)
   List.map initialize variants_fields_types
 
 let compute_expanded_symbolic_tuple_value (span : Meta.span)
-    (field_types : rty list) : symbolic_expansion =
+    (field_types : ty list) : symbolic_expansion =
   (* Generate the field values *)
   let field_values =
     List.map (fun sv_ty -> mk_fresh_symbolic_value span sv_ty) field_types
@@ -251,8 +250,8 @@ let compute_expanded_symbolic_tuple_value (span : Meta.span)
   let see = SeAdt (variant_id, field_values) in
   see
 
-let compute_expanded_symbolic_box_value (span : Meta.span) (boxed_ty : rty) :
-    symbolic_expansion =
+let compute_expanded_symbolic_box_value (span : Meta.span) (boxed_ty : proj_ty)
+    : symbolic_expansion =
   (* Introduce a fresh symbolic value *)
   let boxed_value = mk_fresh_symbolic_value span boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
@@ -283,12 +282,25 @@ let compute_expanded_symbolic_adt_value (span : Meta.span)
 
 let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
-    (ref_ty : rty) : cm_fun =
+    (ref_ty : proj_ty) : cm_fun =
  fun ctx ->
   (* First, replace the projectors on borrows.
-   * The important point is that the symbolic value to expand may appear
-   * several times, if it has been copied. In this case, we need to introduce
-   * one fresh borrow id per instance.
+     The important point is that the symbolic value to expand may appear
+     several times, if it has been copied. In this case, we need to introduce
+     one fresh borrow id per instance.
+
+     Ex.:
+     {[
+       abs { proj_loans (s0 : &T) }
+       x -> s0
+       y -> s0
+
+         ~>
+
+       abs { SL {l0, l1} s1 }
+       x -> SB l0
+       y -> SB l1
+     ]}
    *)
   let borrows = ref BorrowId.Set.empty in
   let fresh_borrow () =
@@ -296,19 +308,22 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
     borrows := BorrowId.Set.add bid' !borrows;
     bid'
   in
+  (* The fresh symbolic value for the shared value *)
+  let shared_sv = mk_fresh_symbolic_value span ref_ty in
   (* Small utility used on shared borrows in abstractions (regular borrow
-   * projector and asb).
-   * Returns [Some] if the symbolic value has been expanded to an asb list,
-   * [None] otherwise *)
-  let reborrow_ashared proj_regions (sv_id : symbolic_value_id) (proj_ty : rty)
-      : abstract_shared_borrows option =
-    if sv_id = original_sv.sv_id then
-      match proj_ty with
+     projector and asb).
+     Returns [Some] if the symbolic value has been expanded to an asb list,
+     [None] otherwise *)
+  let reborrow_ashared (proj : symbolic_proj) : abstract_shared_borrows option =
+    if proj.sv_id = original_sv.sv_id then
+      match proj.proj_ty with
       | TRef (r, ref_ty, RShared) ->
           (* Projector over the shared value *)
-          let shared_asb = AsbProjReborrows (sv_id, ref_ty) in
+          let shared_asb =
+            AsbProjReborrows { sv_id = shared_sv.sv_id; proj_ty = ref_ty }
+          in
           (* Check if the region is in the set of projected regions *)
-          if region_in_set r proj_regions then
+          if region_is_free r then
             (* In the set: we need to reborrow *)
             let bid = fresh_borrow () in
             Some [ AsbBorrow bid; shared_asb ]
@@ -317,8 +332,6 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
       | _ -> craise __FILE__ __LINE__ span "Unexpected"
     else None
   in
-  (* The fresh symbolic value for the shared value *)
-  let shared_sv = mk_fresh_symbolic_value span ref_ty in
   (* Visitor to replace the projectors on borrows *)
   let obj =
     object (self)
@@ -330,20 +343,13 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
           VBorrow (VSharedBorrow bid)
         else super#visit_VSymbolic env sv
 
-      method! visit_EAbs proj_regions abs =
-        sanity_check __FILE__ __LINE__ (Option.is_none proj_regions) span;
-        let proj_regions = Some abs.regions.owned in
-        super#visit_EAbs proj_regions abs
-
-      method! visit_AProjSharedBorrow proj_regions asb =
+      method! visit_AProjSharedBorrow _ asb =
         let expand_asb (asb : abstract_shared_borrow) : abstract_shared_borrows
             =
           match asb with
           | AsbBorrow _ -> [ asb ]
-          | AsbProjReborrows (sv_id, proj_ty) -> (
-              match
-                reborrow_ashared (Option.get proj_regions) sv_id proj_ty
-              with
+          | AsbProjReborrows proj -> (
+              match reborrow_ashared proj with
               | None -> [ asb ]
               | Some asb -> asb)
         in
@@ -357,8 +363,10 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
           never happen *)
       method! visit_aproj proj_regions aproj =
         (match aproj with
-        | AProjLoans (sv_id, _, _) | AProjBorrows (sv_id, _, _) ->
-            sanity_check __FILE__ __LINE__ (sv_id <> original_sv.sv_id) span
+        | AProjLoans { proj; _ } | AProjBorrows { proj; _ } ->
+            sanity_check __FILE__ __LINE__
+              (proj.sv_id <> original_sv.sv_id)
+              span
         | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ());
         super#visit_aproj proj_regions aproj
 
@@ -370,15 +378,15 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
         | AProjLoans _ ->
             (* Loans are handled later *)
             ASymbolic (pm, aproj)
-        | AProjBorrows (sv, proj_ty, given_back) -> (
+        | AProjBorrows { proj; loans } -> (
             (* We should never expand a symbolic value which has consumed given
                back values (because then it means the symbolic value was consumed
                by region abstractions, and is thus inaccessible: such a value can't
                be expanded)
             *)
-            cassert __FILE__ __LINE__ (given_back = []) span "Unreachable";
+            cassert __FILE__ __LINE__ (loans = []) span "Unreachable";
             (* Check if we need to reborrow *)
-            match reborrow_ashared (Option.get proj_regions) sv proj_ty with
+            match reborrow_ashared proj with
             | None -> super#visit_ASymbolic proj_regions pm aproj
             | Some asb -> ABorrow (AProjSharedBorrow asb))
         | AEndedProjLoans _ ->
@@ -406,29 +414,43 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
 (** TODO: simplify and merge with the other expansion function *)
 let expand_symbolic_value_borrow (config : config) (span : Meta.span)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
-    (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
+    (ref_ty : ty) (rkind : ref_kind) : cm_fun =
  fun ctx ->
-  sanity_check __FILE__ __LINE__ (region <> RErased) span;
-  (* Check that we are allowed to expand the reference *)
-  sanity_check __FILE__ __LINE__
-    (not (region_in_set region ctx.ended_regions))
-    span;
+  (* Check that we are allowed to expand the reference: we need to check that
+     there is at least one loan projector which projects the region corresponding
+     to the borrow (otherwise, it means we have ended the loan projector, and thus
+     the borrows it captures). We do this by collecting the projectors in the
+     environment and joining their projection: we can then check that the joined
+     projection is of the shape [&'r (mut) ...], where [r] is a free region (i.e.,
+     a region marked for projection).
+  *)
+  let proj_ty =
+    InterpreterBorrowsCore.collect_symbolic_value_borrow_projectors span ctx
+      original_sv
+  in
+  cassert __FILE__ __LINE__
+    (match proj_ty with
+    | Some (TRef (r, _, _)) -> region_is_free r
+    | _ -> false)
+    span
+    "Could not expand a borrow symbolic value: the borrow has already ended";
+
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
-       * borrow id *)
+         borrow id *)
       let sv = mk_fresh_symbolic_value span ref_ty in
       let bid = fresh_borrow_id () in
       let see = SeMutRef (bid, sv) in
+
       (* Expand the symbolic values - we simply perform a substitution (and
-       * check that we perform exactly one substitution) *)
+         check that we perform exactly one substitution) *)
       let nv =
         symbolic_expansion_non_shared_borrow_to_value span original_sv see
       in
-      let at_most_once = true in
       let ctx =
-        replace_symbolic_values span at_most_once original_sv nv.value ctx
+        replace_symbolic_values span ~at_most_once:true original_sv nv.value ctx
       in
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
@@ -453,8 +475,8 @@ let expand_symbolic_bool (config : config) (span : Meta.span)
  fun ctx ->
   (* Compute the expanded value *)
   let original_sv = sv in
-  let rty = original_sv.sv_ty in
-  sanity_check __FILE__ __LINE__ (rty = TLiteral TBool) span;
+  let ty = original_sv.sv_ty in
+  sanity_check __FILE__ __LINE__ (ty = TLiteral TBool) span;
   (* Expand the symbolic value to true or false and continue execution *)
   let see_true = SeLiteral (VBool true) in
   let see_false = SeLiteral (VBool false) in
@@ -485,9 +507,9 @@ let expand_symbolic_value_no_branching (config : config) (span : Meta.span)
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sv in
   let original_sv_place = sv_place in
-  let rty = original_sv.sv_ty in
+  let ty = original_sv.sv_ty in
   let ctx, cc =
-    match rty with
+    match ty with
     (* ADTs *)
     | TAdt { id = adt_id; generics } ->
         (* Compute the expanded value *)
@@ -509,12 +531,14 @@ let expand_symbolic_value_no_branching (config : config) (span : Meta.span)
             original_sv_place see )
     (* Borrows *)
     | TRef (region, ref_ty, rkind) ->
+        (* The region should have been erased *)
+        sanity_check __FILE__ __LINE__ (region_is_erased region) span;
         expand_symbolic_value_borrow config span original_sv original_sv_place
-          region ref_ty rkind ctx
+          ref_ty rkind ctx
     | _ ->
         craise __FILE__ __LINE__ span
           ("expand_symbolic_value_no_branching: unexpected type: "
-         ^ show_rty rty)
+         ^ ty_to_string ctx ty)
   in
   (* Debug *)
   log#ltrace
diff --git a/src/interp/InterpreterExpressions.ml b/src/interp/InterpreterExpressions.ml
index 957feba32..7d11c9720 100644
--- a/src/interp/InterpreterExpressions.ml
+++ b/src/interp/InterpreterExpressions.ml
@@ -9,6 +9,7 @@ open ValuesUtils
 open SynthesizeSymbolic
 open Cps
 open InterpreterUtils
+open InterpreterBorrowsCore
 open InterpreterExpansion
 open InterpreterPaths
 open Errors
@@ -54,7 +55,7 @@ let read_place_check (span : Meta.span) (access : access_kind) (p : place)
   let v = read_place span access p ctx in
   (* Check that there are no bottoms in the value *)
   cassert __FILE__ __LINE__
-    (not (bottom_in_value ctx.ended_regions v))
+    (not (bottom_in_value span ctx v))
     span "There should be no bottoms in the value";
   (* Check that there are no reserved borrows in the value *)
   cassert __FILE__ __LINE__
@@ -112,9 +113,9 @@ let literal_to_typed_value (span : Meta.span) (ty : literal_type) (cv : literal)
   (* Remaining cases (invalid) *)
   | _, _ -> craise __FILE__ __LINE__ span "Improperly typed constant value"
 
-(** Copy a value, and return the: the original value (we may have need to update
-    it - see the remark about the symbolic values with borrows) and the
-    resulting value.
+(** Copy a value, and return: the original value (we may have need to update it
+    \- see the remark about the symbolic values with borrows) and the resulting
+    value.
 
     Note that copying values might update the context. For instance, when
     copying shared borrows, we need to insert new shared borrows in the context.
@@ -235,20 +236,26 @@ let rec copy_value (span : Meta.span) (allow_adt_copy : bool) (config : config)
         (ty_is_copyable (Substitute.erase_regions sp.sv_ty))
         span "Not primitively copyable";
       (* Check if the symbolic value contains borrows: if it does, we need to
-         introduce au auxiliary region abstraction (see document of the function) *)
+         introduce au auxiliary region abstraction (see comments about the function) *)
       if not (ty_has_borrows (Some span) ctx.type_ctx.type_infos v.ty) then
         (* No borrows: do nothing *)
         (v, v, ctx, fun e -> e)
       else
         let ctx0 = ctx in
+        (* We need to check that bottom does not appear in the value *)
+        cassert __FILE__ __LINE__
+          (not (symbolic_value_contains_bottom span ctx sp))
+          span "Can not copy a symbolic value containing bottom values";
+
         (* There are borrows: we need to introduce one region abstraction per live
            region present in the type *)
-        let regions, ty =
-          InterpreterBorrowsCore.refresh_live_regions_in_ty span ctx sp.sv_ty
+        let proj_tys =
+          InterpreterBorrowsCore.make_projections_for_erased_regions_in_ty span
+            sp.sv_ty
         in
-        let updated_sv = mk_fresh_symbolic_value span ty in
-        let copied_sv = mk_fresh_symbolic_value span ty in
-        let mk_abs (r_id : RegionId.id) (avalues : typed_avalue list) : abs =
+        let updated_sv = mk_fresh_symbolic_value span sp.sv_ty in
+        let copied_sv = mk_fresh_symbolic_value span sp.sv_ty in
+        let mk_abs (avalues : typed_avalue list) : abs =
           let abs =
             {
               abs_id = fresh_abstraction_id ();
@@ -256,11 +263,6 @@ let rec copy_value (span : Meta.span) (allow_adt_copy : bool) (config : config)
               can_end = true;
               parents = AbstractionId.Set.empty;
               original_parents = [];
-              regions =
-                {
-                  owned = RegionId.Set.singleton r_id;
-                  ancestors = RegionId.Set.empty;
-                };
               avalues;
             }
           in
@@ -271,20 +273,21 @@ let rec copy_value (span : Meta.span) (allow_adt_copy : bool) (config : config)
 
         let abs =
           List.map
-            (fun rid ->
+            (fun proj_ty ->
               let mk_proj (is_borrows : bool) sv_id : typed_avalue =
+                let proj : symbolic_proj = { sv_id; proj_ty } in
                 let proj =
-                  if is_borrows then AProjBorrows (sv_id, ty, [])
-                  else AProjLoans (sv_id, ty, [])
+                  if is_borrows then AProjBorrows { proj; loans = [] }
+                  else AProjLoans { proj; consumed = []; borrows = [] }
                 in
                 let value = ASymbolic (PNone, proj) in
-                { value; ty }
+                { value; ty = proj_ty }
               in
               let sv = mk_proj true sp.sv_id in
               let updated_sv = mk_proj false updated_sv.sv_id in
               let copied_sv = mk_proj false copied_sv.sv_id in
-              mk_abs rid [ sv; updated_sv; copied_sv ])
-            (RegionId.Map.values regions)
+              mk_abs [ sv; updated_sv; copied_sv ])
+            proj_tys
         in
         let abs = List.map (fun a -> EAbs a) (List.rev abs) in
         let ctx = { ctx with env = abs @ ctx.env } in
@@ -459,7 +462,7 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
       let v = read_place_check span access p ctx in
       (* Sanity checks *)
       exec_assert __FILE__ __LINE__
-        (not (bottom_in_value ctx.ended_regions v))
+        (not (bottom_in_value span ctx v))
         span "Can not copy a value containing bottom";
       sanity_check __FILE__ __LINE__
         (Option.is_none
@@ -481,7 +484,7 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
       let v = read_place_check span access p ctx in
       (* Check that there are no bottoms in the value we are about to move *)
       exec_assert __FILE__ __LINE__
-        (not (bottom_in_value ctx.ended_regions v))
+        (not (bottom_in_value span ctx v))
         span "There should be no bottoms in the value we are about to move";
       (* Move the value *)
       let bottom : typed_value = { value = VBottom; ty = v.ty } in
@@ -1084,6 +1087,6 @@ let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun =
     access_rplace_reorganize_and_read config span greedy_expand Read p ctx
   in
   cassert __FILE__ __LINE__
-    (not (bottom_in_value ctx.ended_regions v))
+    (not (bottom_in_value span ctx v))
     span "Fake read: the value contains bottom";
   (ctx, cc)
diff --git a/src/interp/InterpreterLoops.ml b/src/interp/InterpreterLoops.ml
index 25f15dbf3..1eccf47ca 100644
--- a/src/interp/InterpreterLoops.ml
+++ b/src/interp/InterpreterLoops.ml
@@ -179,10 +179,10 @@ let eval_loop_symbolic_synthesize_fun_end (config : config) (span : span)
       List.filter_map
         (fun (av : typed_avalue) ->
           match av.value with
-          | ASymbolic (pm, AProjBorrows (sv_id, _proj_ty, children)) ->
+          | ASymbolic (pm, AProjBorrows { proj; loans }) ->
               sanity_check __FILE__ __LINE__ (pm = PNone) span;
-              sanity_check __FILE__ __LINE__ (children = []) span;
-              Some sv_id
+              sanity_check __FILE__ __LINE__ (loans = []) span;
+              Some proj.sv_id
           | _ -> None)
         borrows
     in
@@ -207,10 +207,11 @@ let eval_loop_symbolic_synthesize_fun_end (config : config) (span : span)
       List.filter_map
         (fun (av : typed_avalue) ->
           match av.value with
-          | ASymbolic (pm, AProjLoans (sv_id, _proj_ty, children)) ->
+          | ASymbolic (pm, AProjLoans { proj; consumed; borrows }) ->
               sanity_check __FILE__ __LINE__ (pm = PNone) span;
-              sanity_check __FILE__ __LINE__ (children = []) span;
-              Some sv_id
+              sanity_check __FILE__ __LINE__ (consumed = []) span;
+              sanity_check __FILE__ __LINE__ (borrows = []) span;
+              Some proj.sv_id
           | _ -> None)
         loans
     in
@@ -332,7 +333,9 @@ let eval_loop_symbolic (config : config) (span : span)
   let fresh_sids, input_svalues =
     compute_fp_ctx_symbolic_values span ctx fp_ctx
   in
-  let fp_input_svalues = List.map (fun sv -> sv.sv_id) input_svalues in
+  let fp_input_svalues =
+    List.map (fun (sv : symbolic_value) -> sv.sv_id) input_svalues
+  in
 
   (* Synthesize the end of the function - we simply match the context at the
      loop entry with the fixed point: in the synthesized code, the function
@@ -403,7 +406,9 @@ let eval_loop_symbolic (config : config) (span : span)
         (fun (av : typed_avalue) ->
           SymbolicToPure.translate_back_ty (Some span) ctx.type_ctx.type_infos
             (function
-              | RVar (Free rid) -> RegionId.Set.mem rid abs.regions.owned
+              | RVar (Free rid) ->
+                  sanity_check __FILE__ __LINE__ (rid = RegionId.zero) span;
+                  true
               | _ -> false)
             false av.ty)
         borrows
diff --git a/src/interp/InterpreterLoopsCore.ml b/src/interp/InterpreterLoopsCore.ml
index d7f0d38d3..89d5e5896 100644
--- a/src/interp/InterpreterLoopsCore.ml
+++ b/src/interp/InterpreterLoopsCore.ml
@@ -148,8 +148,16 @@ module type PrimMatcher = sig
     rty ->
     typed_avalue
 
-  (** Parameters: [ctx0] [ctx1] [ty0] [pm0] [bid0] [ty1] [pm1] [bid1] [ty]:
-      result of matching ty0 and ty1 *)
+  (** Parameters:
+      - [ctx0]
+      - [ctx1]
+      - [ty0]
+      - [pm0]
+      - [bid0]
+      - [ty1]
+      - [pm1]
+      - [bid1]
+      - [ty]: result of matching ty0 and ty1 *)
   val match_ashared_borrows :
     eval_ctx ->
     eval_ctx ->
@@ -162,9 +170,19 @@ module type PrimMatcher = sig
     rty ->
     typed_avalue
 
-  (** Parameters: [ctx0] [ctx1] [ty0] [pm0] [bid0] [av0] [ty1] [pm1] [bid1]
-      [av1] [ty]: result of matching ty0 and ty1 [av]: result of matching av0
-      and av1 *)
+  (** Parameters:
+      - [ctx0]
+      - [ctx1]
+      - [ty0]
+      - [pm0]
+      - [bid0]
+      - [av0]
+      - [ty1]
+      - [pm1]
+      - [bid1]
+      - [av1]
+      - [ty]: result of matching ty0 and ty1
+      - [av]: result of matching av0 and av1 *)
   val match_amut_borrows :
     eval_ctx ->
     eval_ctx ->
@@ -180,9 +198,22 @@ module type PrimMatcher = sig
     typed_avalue ->
     typed_avalue
 
-  (** Parameters: [ctx0] [ctx1] [ty0] [pm0] [ids0] [v0] [av0] [ty1] [pm1] [ids1]
-      [v1] [av1] [ty]: result of matching ty0 and ty1 [v]: result of matching v0
-      and v1 [av]: result of matching av0 and av1 *)
+  (** Parameters:
+      - [ctx0]
+      - [ctx1]
+      - [ty0]
+      - [pm0]
+      - [ids0]
+      - [v0]
+      - [av0]
+      - [ty1]
+      - [pm1]
+      - [ids1]
+      - [v1]
+      - [av1]
+      - [ty]: result of matching ty0 and ty1
+      - [v]: result of matching v0 and v1
+      - [av]: result of matching av0 and av1 *)
   val match_ashared_loans :
     eval_ctx ->
     eval_ctx ->
@@ -201,9 +232,19 @@ module type PrimMatcher = sig
     typed_avalue ->
     typed_avalue
 
-  (** Parameters: [ctx0] [ctx1] [ty0] [pm0] [id0] [av0] [ty1] [pm1] [id1] [av1]
-      [ty]: result of matching ty0 and ty1 [av]: result of matching av0 and av1
-  *)
+  (** Parameters:
+      - [ctx0]
+      - [ctx1]
+      - [ty0]
+      - [pm0]
+      - [id0]
+      - [av0]
+      - [ty1]
+      - [pm1]
+      - [id1]
+      - [av1]
+      - [ty]: result of matching ty0 and ty1
+      - [av]: result of matching av0 and av1 *)
   val match_amut_loans :
     eval_ctx ->
     eval_ctx ->
@@ -219,42 +260,50 @@ module type PrimMatcher = sig
     typed_avalue ->
     typed_avalue
 
-  (** Parameters: [ctx0] [ctx1] [ty0] [pm0] [sv0] [proj_ty0] [children0] [ty1]
-      [pm1] [sv1] [proj_ty1] [children1] [ty]: result of matching ty0 and ty1
-      [proj_ty]: result of matching proj_ty0 and proj_ty1 *)
+  (** Parameters:
+      - [ctx0]
+      - [ctx1]
+      - [ty0]
+      - [pm0]
+      - [proj0]
+      - [ty1]
+      - [pm1]
+      - [proj1]
+      - [ty]: result of matching ty0 and ty1
+      - [proj_ty]: result of matching proj_ty0 and proj_ty1 *)
   val match_aproj_borrows :
     eval_ctx ->
     eval_ctx ->
     rty ->
     proj_marker ->
-    symbolic_value_id ->
-    rty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_borrows ->
     rty ->
     proj_marker ->
-    symbolic_value_id ->
-    rty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_borrows ->
     rty ->
     rty ->
     typed_avalue
 
-  (** Parameters: [ctx0] [ctx1] [ty0] [pm0] [sv0] [proj_ty0] [children0] [ty1]
-      [pm1] [sv1] [proj_ty1] [children1] [ty]: result of matching ty0 and ty1
-      [proj_ty]: result of matching proj_ty0 and proj_ty1 *)
+  (** Parameters:
+      - [ctx0]
+      - [ctx1]
+      - [ty0]
+      - [pm0]
+      - [proj0]
+      - [ty1]
+      - [pm1]
+      - [proj1]
+      - [ty]: result of matching ty0 and ty1
+      - [proj_ty]: result of matching proj_ty0 and proj_ty1 *)
   val match_aproj_loans :
     eval_ctx ->
     eval_ctx ->
     rty ->
     proj_marker ->
-    symbolic_value_id ->
-    rty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_loans ->
     rty ->
     proj_marker ->
-    symbolic_value_id ->
-    rty ->
-    (msymbolic_value_id * aproj) list ->
+    aproj_loans ->
     rty ->
     rty ->
     typed_avalue
@@ -294,8 +343,6 @@ module type MatchCheckEquivState = sig
       source context with a target context. *)
   val check_equiv : bool
 
-  val rid_map : RegionId.InjSubst.t ref
-
   (** Substitution for the loan and borrow ids - used only if [check_equiv] is
       true *)
   val blid_map : BorrowId.InjSubst.t ref
@@ -324,8 +371,6 @@ module type CheckEquivMatcher = sig
   val match_aids :
     abstraction_id_set -> abstraction_id_set -> abstraction_id_set
 
-  val match_rid : region_id -> region_id -> region_id
-  val match_rids : region_id_set -> region_id_set -> region_id_set
   val match_borrow_id : borrow_id -> borrow_id -> borrow_id
   val match_borrow_idl : borrow_id list -> borrow_id list -> borrow_id list
   val match_borrow_ids : borrow_id_set -> borrow_id_set -> borrow_id_set
@@ -341,7 +386,6 @@ type ids_maps = {
       (** Substitution for the loan and borrow ids *)
   borrow_id_map : BorrowId.InjSubst.t;  (** Substitution for the borrow ids *)
   loan_id_map : BorrowId.InjSubst.t;  (** Substitution for the loan ids *)
-  rid_map : RegionId.InjSubst.t;
   sid_map : SymbolicValueId.InjSubst.t;
   sid_to_value_map : typed_value SymbolicValueId.Map.t;
 }
@@ -353,7 +397,6 @@ let ids_maps_to_string (ctx : eval_ctx) (m : ids_maps) : string =
     blid_map;
     borrow_id_map;
     loan_id_map;
-    rid_map;
     sid_map;
     sid_to_value_map;
   } =
@@ -368,8 +411,6 @@ let ids_maps_to_string (ctx : eval_ctx) (m : ids_maps) : string =
   ^ BorrowId.InjSubst.to_string indent borrow_id_map
   ^ "\n  loan_id_map = "
   ^ BorrowId.InjSubst.to_string indent loan_id_map
-  ^ "\n  rid_map = "
-  ^ RegionId.InjSubst.to_string indent rid_map
   ^ "\n  sid_map = "
   ^ SymbolicValueId.InjSubst.to_string indent sid_map
   ^ "\n  sid_to_value_map = "
@@ -443,20 +484,10 @@ let ctx_split_fixed_new (span : Meta.span) (fixed_ids : ids_sets)
   (filt_env, new_absl, new_dummyl)
 
 let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
-  let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } =
-    ids
-  in
+  let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; sids } = ids in
   let empty = BorrowId.Set.empty in
   let ids =
-    {
-      aids;
-      blids = empty;
-      borrow_ids = empty;
-      loan_ids = empty;
-      dids;
-      rids;
-      sids;
-    }
+    { aids; blids = empty; borrow_ids = empty; loan_ids = empty; dids; sids }
   in
   ids
 
diff --git a/src/interp/InterpreterLoopsFixedPoint.ml b/src/interp/InterpreterLoopsFixedPoint.ml
index e6513782e..0a7187d12 100644
--- a/src/interp/InterpreterLoopsFixedPoint.ml
+++ b/src/interp/InterpreterLoopsFixedPoint.ml
@@ -41,15 +41,13 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
      - the region ids found in the value and belonging to the set [rids] have
        been substituted with [nrid]
   *)
-  let mk_value_with_fresh_sids_no_shared_loans (rids : RegionId.Set.t)
-      (nrid : RegionId.id) (v : typed_value) : typed_value =
+  let mk_value_with_fresh_sids_no_shared_loans (v : typed_value) : typed_value =
     (* Remove the shared loans *)
     let v = value_remove_shared_loans v in
     (* Substitute the symbolic values and the region *)
     Substitute.typed_value_subst_ids
       {
         (Substitute.no_abs_id_subst span) with
-        r_subst = (fun r -> if RegionId.Set.mem r rids then nrid else r);
         ssubst =
           (fun id ->
             let nid = fresh_symbolic_value_id () in
@@ -97,9 +95,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     let nrid = fresh_region_id () in
 
     (* Prepare the shared value *)
-    let nsv =
-      mk_value_with_fresh_sids_no_shared_loans abs.regions.owned nrid sv
-    in
+    let nsv = mk_value_with_fresh_sids_no_shared_loans sv in
 
     (* Save the borrow substitution, to apply it to the context later *)
     borrow_substs := (lid, nlid) :: !borrow_substs;
@@ -107,9 +103,6 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     (* Rem.: the below sanity checks are not really necessary *)
     sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) span;
     sanity_check __FILE__ __LINE__ (abs.original_parents = []) span;
-    sanity_check __FILE__ __LINE__
-      (RegionId.Set.is_empty abs.regions.ancestors)
-      span;
 
     (* Introduce the new abstraction for the shared values *)
     cassert __FILE__ __LINE__ (ty_no_regions sv.ty) span
@@ -140,9 +133,6 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
       | None -> Identity
     in
     let can_end = true in
-    let regions : abs_regions =
-      { owned = RegionId.Set.singleton nrid; ancestors = RegionId.Set.empty }
-    in
     let fresh_abs =
       {
         abs_id = fresh_abstraction_id ();
@@ -150,7 +140,6 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
         can_end;
         parents = AbstractionId.Set.empty;
         original_parents = [];
-        regions;
         avalues;
       }
     in
@@ -365,7 +354,7 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
      of new environments *)
   let compute_fixed_ids (ctxl : eval_ctx list) : ids_sets =
     let fixed_ids, _ = compute_ctx_ids ctx0 in
-    let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in
+    let { aids; blids; borrow_ids; loan_ids; dids; sids } = fixed_ids in
     let sids = ref sids in
     List.iter
       (fun ctx ->
@@ -373,7 +362,7 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
         sids := SymbolicValueId.Set.inter !sids fixed_ids.sids)
       ctxl;
     let sids = !sids in
-    let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; rids; sids } in
+    let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; sids } in
     fixed_ids
   in
   (* Check if two contexts are equivalent - modulo alpha conversion on the
@@ -858,18 +847,19 @@ let compute_fixed_point_id_correspondance (span : Meta.span)
 
       method! visit_aproj _ proj =
         match proj with
-        | AProjLoans (_sv, _proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
+        | AProjLoans { proj = _; consumed; borrows } ->
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
             ()
-        | AProjBorrows (sv_id, _proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
+        | AProjBorrows { proj; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span;
             (* Find the target borrow *)
             let tgt_borrow_id =
-              SymbolicValueId.Map.find sv_id src_to_tgt_sid_map
+              SymbolicValueId.Map.find proj.sv_id src_to_tgt_sid_map
             in
             (* Update the map *)
             tgt_borrow_to_loan_proj :=
-              SymbolicValueId.InjSubst.add sv_id tgt_borrow_id
+              SymbolicValueId.InjSubst.add proj.sv_id tgt_borrow_id
                 !tgt_borrow_to_loan_proj
         | AEndedProjBorrows _ | AEndedProjLoans _ | AEmpty ->
             (* We shouldn't get there *)
@@ -944,14 +934,24 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx)
           self#visit_typed_value true sv;
           self#visit_typed_avalue register child_av
 
-        method! visit_AProjLoans register sv_id proj_ty children =
+        method! visit_AProjLoans register proj =
+          let { proj = { sv_id; proj_ty }; consumed; borrows } : aproj_loans =
+            proj
+          in
           self#visit_symbolic_value_id true sv_id;
           self#visit_ty register proj_ty;
+          sanity_check __FILE__ __LINE__ (consumed = []) span;
+          sanity_check __FILE__ __LINE__ (borrows = []) span
+        (*self#visit_list
+            (fun register ((s, p) : mconsumed_symb * _) ->
+              self#visit_msymbolic_value_id register s.sv_id;
+              self#visit_aproj register p)
+            register consumed;
           self#visit_list
-            (fun register (s, p) ->
-              self#visit_msymbolic_value_id register s;
+            (fun register ((s, p) : mconsumed_symb * _) ->
+              self#visit_msymbolic_value_id register s.sv_id;
               self#visit_aproj register p)
-            register children
+            register borrows*)
 
         method! visit_symbolic_value_id register sid =
           if register then sids := SymbolicValueId.Set.add sid !sids
diff --git a/src/interp/InterpreterLoopsJoinCtxs.ml b/src/interp/InterpreterLoopsJoinCtxs.ml
index 14e271c7b..fdbdbd684 100644
--- a/src/interp/InterpreterLoopsJoinCtxs.ml
+++ b/src/interp/InterpreterLoopsJoinCtxs.ml
@@ -1,4 +1,3 @@
-open Types
 open Values
 open Contexts
 open Utils
@@ -735,16 +734,14 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
      Note that the join matcher doesn't implement match functions for avalues
      (see the comments in {!MakeJoinMatcher}.
   *)
-  let merge_amut_borrows id ty0 _pm0 child0 _ty1 _pm1 child1 =
+  let merge_amut_borrows id ty0 _pm0 child0 ty1 _pm1 child1 =
     (* Sanity checks *)
     sanity_check __FILE__ __LINE__ (is_aignored child0.value) span;
     sanity_check __FILE__ __LINE__ (is_aignored child1.value) span;
+    sanity_check __FILE__ __LINE__ (ty0 = ty1) span;
 
-    (* We need to pick a type for the avalue. The types on the left and on the
-       right may use different regions: it doesn't really matter (here, we pick
-       the one from the left), because we will merge those regions together
-       anyway (see the comments for {!merge_into_first_abstraction}).
-    *)
+    (* We need to pick a type for the avalue: it can be the one from the left
+       or from the right: it doesn't really matter. *)
     let ty = ty0 in
     let child = child0 in
     let value = ABorrow (AMutBorrow (PNone, id, child)) in
@@ -804,32 +801,57 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span)
     let value = ALoan (ASharedLoan (PNone, ids, sv, child)) in
     { value; ty }
   in
-  let merge_aborrow_projs ty0 _pm0 (sv0 : symbolic_value_id) proj_ty0 children0
-      _ty1 _pm1 (sv1 : symbolic_value_id) _proj_ty1 children1 =
+  let merge_aborrow_projs ty0 _pm0 (proj0 : aproj_borrows) _ty1 _pm1
+      (proj1 : aproj_borrows) =
+    let { proj = { sv_id = sv0; proj_ty = proj_ty0 }; loans = loans0 } =
+      proj0
+    in
+    let { proj = { sv_id = sv1; proj_ty = proj_ty1 }; loans = loans1 } =
+      proj1
+    in
     (* Sanity checks *)
-    sanity_check __FILE__ __LINE__ (children0 = []) span;
-    sanity_check __FILE__ __LINE__ (children1 = []) span;
+    sanity_check __FILE__ __LINE__ (loans0 = []) span;
+    sanity_check __FILE__ __LINE__ (loans1 = []) span;
+    sanity_check __FILE__ __LINE__ (proj_ty0 = proj_ty1) span;
     (* Same remarks as for [merge_amut_borrows]. *)
     let ty = ty0 in
     let proj_ty = proj_ty0 in
-    let children = [] in
+    let loans = [] in
     sanity_check __FILE__ __LINE__ (sv0 = sv1) span;
-    let sv = sv0 in
-    let value = ASymbolic (PNone, AProjBorrows (sv, proj_ty, children)) in
+    let sv_id = sv0 in
+    let proj : symbolic_proj = { sv_id; proj_ty } in
+    let value = ASymbolic (PNone, AProjBorrows { proj; loans }) in
     { value; ty }
   in
-  let merge_aloan_projs ty0 _pm0 (sv0 : symbolic_value_id) proj_ty0 children0
-      _ty1 _pm1 (sv1 : symbolic_value_id) _proj_ty1 children1 =
+  let merge_aloan_projs ty0 _pm0 (proj0 : aproj_loans) _ty1 _pm1
+      (proj1 : aproj_loans) =
+    let {
+      proj = { sv_id = sv0; proj_ty = proj_ty0 };
+      consumed = consumed0;
+      borrows = borrows0;
+    } : aproj_loans =
+      proj0
+    in
+    let {
+      proj = { sv_id = sv1; proj_ty = proj_ty1 };
+      consumed = consumed1;
+      borrows = borrows1;
+    } : aproj_loans =
+      proj1
+    in
     (* Sanity checks *)
-    sanity_check __FILE__ __LINE__ (children0 = []) span;
-    sanity_check __FILE__ __LINE__ (children1 = []) span;
+    sanity_check __FILE__ __LINE__ (consumed0 = [] && borrows0 = []) span;
+    sanity_check __FILE__ __LINE__ (consumed1 = [] && borrows1 = []) span;
+    sanity_check __FILE__ __LINE__ (proj_ty0 = proj_ty1) span;
     (* Same remarks as for [merge_amut_borrows]. *)
     let ty = ty0 in
     let proj_ty = proj_ty0 in
-    let children = [] in
+    let consumed = [] in
+    let borrows = [] in
     sanity_check __FILE__ __LINE__ (sv0 = sv1) span;
-    let sv = sv0 in
-    let value = ASymbolic (PNone, AProjLoans (sv, proj_ty, children)) in
+    let sv_id = sv0 in
+    let proj = { sv_id; proj_ty } in
+    let value = ASymbolic (PNone, AProjLoans { proj; consumed; borrows }) in
     { value; ty }
   in
   {
@@ -1035,7 +1057,6 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
       const_generic_vars_map;
       norm_trait_types;
       env = _;
-      ended_regions = ended_regions0;
     } =
       ctx0
     in
@@ -1049,11 +1070,9 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
       const_generic_vars_map = _;
       norm_trait_types = _;
       env = _;
-      ended_regions = ended_regions1;
     } =
       ctx1
     in
-    let ended_regions = RegionId.Set.union ended_regions0 ended_regions1 in
     Ok
       {
         crate;
@@ -1065,7 +1084,6 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
         const_generic_vars_map;
         norm_trait_types;
         env;
-        ended_regions;
       }
   with ValueMatchFailure e -> Error e
 
diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml
index aafb47065..dc2ad323a 100644
--- a/src/interp/InterpreterLoopsMatchCtxs.ml
+++ b/src/interp/InterpreterLoopsMatchCtxs.ml
@@ -87,17 +87,19 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool)
     RAbsBorrow.register_mapping false abs_to_loans abs.abs_id (pm, bid);
     RBorrowAbs.register_mapping true loan_to_abs (pm, bid) abs.abs_id
   in
-  let register_borrow_proj abs pm (sv_id : symbolic_value_id) (proj_ty : ty) =
-    let norm_proj_ty = normalize_proj_ty abs.regions.owned proj_ty in
-    let proj : marked_norm_symb_proj = { pm; sv_id; norm_proj_ty } in
+  let register_borrow_proj abs pm (proj : symbolic_proj) =
+    let proj : marked_norm_symb_proj =
+      { pm; sv_id = proj.sv_id; norm_proj_ty = proj.proj_ty }
+    in
     RAbsSymbProj.register_mapping false abs_to_borrow_projs abs.abs_id proj;
     (* This mapping is *actually* injective because we refresh symbolic values
        with borrows when copying them. See [InterpreterExpressions.copy_value]. *)
     RSymbProjAbs.register_mapping true borrow_proj_to_abs proj abs.abs_id
   in
-  let register_loan_proj abs pm (sv_id : symbolic_value_id) (proj_ty : ty) =
-    let norm_proj_ty = normalize_proj_ty abs.regions.owned proj_ty in
-    let proj : marked_norm_symb_proj = { pm; sv_id; norm_proj_ty } in
+  let register_loan_proj abs pm (proj : symbolic_proj) =
+    let proj : marked_norm_symb_proj =
+      { pm; sv_id = proj.sv_id; norm_proj_ty = proj.proj_ty }
+    in
     RAbsSymbProj.register_mapping false abs_to_loan_projs abs.abs_id proj;
     RSymbProjAbs.register_mapping true loan_proj_to_abs proj abs.abs_id
   in
@@ -160,14 +162,18 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool)
 
       method! visit_ASymbolic (abs, _) pm proj =
         match proj with
-        | AProjLoans (sv, proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
-            register_loan_proj abs pm sv proj_ty
-        | AProjBorrows (sv, proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
-            register_borrow_proj abs pm sv proj_ty
-        | AEndedProjLoans (_, children) | AEndedProjBorrows (_, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span
+        | AProjLoans { proj; consumed; borrows } ->
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
+            register_loan_proj abs pm proj
+        | AProjBorrows { proj; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span;
+            register_borrow_proj abs pm proj
+        | AEndedProjLoans { proj = _; consumed; borrows } ->
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span
+        | AEndedProjBorrows { mvalues = _; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span
         | AEmpty -> ()
     end
   in
@@ -478,16 +484,16 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
         | _ -> craise __FILE__ __LINE__ M.span "Unreachable")
     | ASymbolic (pm0, proj0), ASymbolic (pm1, proj1) -> begin
         match (proj0, proj1) with
-        | ( AProjBorrows (sv0, proj_ty0, children0),
-            AProjBorrows (sv1, proj_ty1, children1) ) ->
-            let proj_ty = M.match_rtys ctx0 ctx1 proj_ty0 proj_ty1 in
-            M.match_aproj_borrows ctx0 ctx1 v0.ty pm0 sv0 proj_ty0 children0
-              v1.ty pm1 sv1 proj_ty1 children1 ty proj_ty
-        | ( AProjLoans (sv0, proj_ty0, children0),
-            AProjLoans (sv1, proj_ty1, children1) ) ->
-            let proj_ty = M.match_rtys ctx0 ctx1 proj_ty0 proj_ty1 in
-            M.match_aproj_loans ctx0 ctx1 v0.ty pm0 sv0 proj_ty0 children0 v1.ty
-              pm1 sv1 proj_ty1 children1 ty proj_ty
+        | ( AProjBorrows ({ proj = proj0; _ } as pborrows0),
+            AProjBorrows ({ proj = proj1; _ } as pborrows1) ) ->
+            let proj_ty = M.match_rtys ctx0 ctx1 proj0.proj_ty proj1.proj_ty in
+            M.match_aproj_borrows ctx0 ctx1 v0.ty pm0 pborrows0 v1.ty pm1
+              pborrows1 ty proj_ty
+        | ( AProjLoans ({ proj = proj0; _ } as ploans0),
+            AProjLoans ({ proj = proj1; _ } as ploans1) ) ->
+            let proj_ty = M.match_rtys ctx0 ctx1 proj0.proj_ty proj1.proj_ty in
+            M.match_aproj_loans ctx0 ctx1 v0.ty pm0 ploans0 v1.ty pm1 ploans1 ty
+              proj_ty
         | _ -> craise __FILE__ __LINE__ M.span "Unreachable"
       end
     | _ -> M.match_avalues ctx0 ctx1 v0 v1
@@ -544,8 +550,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
     (* If there is a bottom in one of the two values, return bottom: *)
     if
-      bottom_in_adt_value ctx0.ended_regions adt0
-      || bottom_in_adt_value ctx1.ended_regions adt1
+      bottom_in_adt_value S.span ctx0 adt0
+      || bottom_in_adt_value S.span ctx1 adt1
     then mk_bottom span ty
     else
       (* No borrows, no loans, no bottoms: we can introduce a symbolic value *)
@@ -567,7 +573,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
            { SB bid0, SB bid1, SL {bid2} }
          ]}
       *)
-      let rid = fresh_region_id () in
+      let rid = RegionId.zero in
       let bid2 = fresh_borrow_id () in
 
       (* Update the type of the shared loan to use the fresh region *)
@@ -598,11 +604,6 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
           can_end = true;
           parents = AbstractionId.Set.empty;
           original_parents = [];
-          regions =
-            {
-              owned = RegionId.Set.singleton rid;
-              ancestors = RegionId.Set.empty;
-            };
           avalues;
         }
       in
@@ -681,7 +682,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
         sanity_check __FILE__ __LINE__ (bv0 = bv) span;
         (bid0, bv))
       else
-        let rid = fresh_region_id () in
+        let rid = RegionId.zero in
         let nbid = fresh_borrow_id () in
 
         let kind = RMut in
@@ -716,11 +717,6 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
             can_end = true;
             parents = AbstractionId.Set.empty;
             original_parents = [];
-            regions =
-              {
-                owned = RegionId.Set.singleton rid;
-                ancestors = RegionId.Set.empty;
-              };
             avalues;
           }
         in
@@ -736,7 +732,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
            { |MB bid0|, ︙MB bid1︙, ML bid2 }
          ]}
       *)
-      let rid = fresh_region_id () in
+      let rid = RegionId.zero in
       let bid2 = fresh_borrow_id () in
 
       (* Generate a fresh symbolic value for the borrowed value *)
@@ -772,11 +768,6 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
           can_end = true;
           parents = AbstractionId.Set.empty;
           original_parents = [];
-          regions =
-            {
-              owned = RegionId.Set.singleton rid;
-              ancestors = RegionId.Set.empty;
-            };
           avalues;
         }
       in
@@ -838,8 +829,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          A more general approach would be to introduce a symbolic value
          with some ended regions. *)
       sanity_check __FILE__ __LINE__
-        ((not (symbolic_value_has_ended_regions ctx0.ended_regions sv0))
-        && not (symbolic_value_has_ended_regions ctx1.ended_regions sv1))
+        ((not (symbolic_value_contains_bottom span ctx0 sv0))
+        && not (symbolic_value_contains_bottom span ctx1 sv1))
         span;
       (* If the symbolic values contain regions, we need to introduce abstractions *)
       if ty_has_borrows (Some span) ctx0.type_ctx.type_infos sv0.sv_ty then (
@@ -849,8 +840,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
              s1 : S<'2, '3>
            ]}
 
-           We introduce a fresh symbolic value with fresh regions, as well as
-           one abstraction per region. It looks like so:
+           We introduce a fresh symbolic value, as well as one abstraction per region
+           appearing in the symbolic value. It looks like so:
            {[
              join s0 s1 ~> s2 : S<'a, 'b>,
                A0('a) {
@@ -866,16 +857,19 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
            ]}
         *)
         (* Introduce one region abstraction per region appearing in the symbolic value *)
-        let fresh_regions, proj_ty =
-          ty_refresh_regions (Some span) fresh_region_id sv0.sv_ty
+        let proj_tys =
+          InterpreterBorrowsCore.make_projections_for_erased_regions_in_ty
+            S.span sv0.sv_ty
+        in
+        let svj = mk_fresh_symbolic_value span sv0.sv_ty in
+        let proj_s0 proj_ty = mk_aproj_borrows PLeft sv0.sv_id proj_ty in
+        let proj_s1 proj_ty = mk_aproj_borrows PRight sv1.sv_id proj_ty in
+        let proj_svj proj_ty = mk_aproj_loans PNone svj.sv_id proj_ty in
+        let avalues proj_ty =
+          [ proj_s0 proj_ty; proj_s1 proj_ty; proj_svj proj_ty ]
         in
-        let svj = mk_fresh_symbolic_value span proj_ty in
-        let proj_s0 = mk_aproj_borrows PLeft sv0.sv_id proj_ty in
-        let proj_s1 = mk_aproj_borrows PRight sv1.sv_id proj_ty in
-        let proj_svj = mk_aproj_loans PNone svj.sv_id proj_ty in
-        let avalues = [ proj_s0; proj_s1; proj_svj ] in
         List.iter
-          (fun rid ->
+          (fun proj_ty ->
             let abs =
               {
                 abs_id = fresh_abstraction_id ();
@@ -883,16 +877,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
                 can_end = true;
                 parents = AbstractionId.Set.empty;
                 original_parents = [];
-                regions =
-                  {
-                    owned = RegionId.Set.singleton rid;
-                    ancestors = RegionId.Set.empty;
-                  };
-                avalues;
+                avalues = avalues proj_ty;
               }
             in
             push_abs abs)
-          fresh_regions;
+          proj_tys;
         svj)
       else
         (* Otherwise we simply introduce a fresh symbolic value *)
@@ -927,8 +916,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
        value contains bottom) the result of the join is bottom. Otherwise,
        we generate a fresh symbolic value. *)
     if
-      symbolic_value_has_ended_regions ctx0.ended_regions sv
-      || bottom_in_value ctx1.ended_regions v
+      symbolic_value_contains_bottom span ctx0 sv || bottom_in_value span ctx1 v
     then mk_bottom span sv.sv_ty
     else mk_fresh_symbolic_typed_value span sv.sv_ty
 
@@ -987,10 +975,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
   let match_amut_loans _ _ _ _ _ _ _ _ _ _ =
     craise __FILE__ __LINE__ span "Unreachable"
 
-  let match_aproj_borrows _ _ _ _ _ _ _ _ _ _ _ _ _ _ =
+  let match_aproj_borrows _ _ _ _ _ _ _ _ _ _ =
     craise __FILE__ __LINE__ span "Unreachable"
 
-  let match_aproj_loans _ _ _ _ _ _ _ _ _ _ _ _ _ _ =
+  let match_aproj_loans _ _ _ _ _ _ _ _ _ _ =
     craise __FILE__ __LINE__ span "Unreachable"
 
   let match_avalues _ _ _ _ = craise __FILE__ __LINE__ span "Unreachable"
@@ -1079,8 +1067,7 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
     (* We're being conservative for now: if any of the two values contains
        a bottom, the join is bottom *)
     if
-      symbolic_value_has_ended_regions ctx0.ended_regions sv
-      || bottom_in_value ctx1.ended_regions v
+      symbolic_value_contains_bottom span ctx0 sv || bottom_in_value span ctx1 v
     then mk_bottom span sv.sv_ty
     else if left then v
     else mk_typed_value_from_symbolic_value sv
@@ -1134,10 +1121,10 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
 
   let match_avalues _ _ _ _ = craise __FILE__ __LINE__ span "Unreachable"
 
-  let match_aproj_borrows _ _ _ _ _ _ _ _ _ _ _ _ _ _ =
+  let match_aproj_borrows _ _ _ _ _ _ _ _ _ _ =
     craise __FILE__ __LINE__ span "Unreachable"
 
-  let match_aproj_loans _ _ _ _ _ _ _ _ _ _ _ _ _ _ =
+  let match_aproj_loans _ _ _ _ _ _ _ _ _ _ =
     craise __FILE__ __LINE__ span "Unreachable"
 end
 
@@ -1186,11 +1173,6 @@ struct
         (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1))
   end
 
-  module GetSetRid = MkGetSetM (RegionId)
-
-  let match_rid = GetSetRid.match_e "match_rid: " S.rid_map
-  let match_rids = GetSetRid.match_es "match_rids: " S.rid_map
-
   module GetSetBid = MkGetSetM (BorrowId)
 
   let match_blid msg = GetSetBid.match_e msg S.blid_map
@@ -1238,8 +1220,10 @@ struct
       match (r0, r1) with
       | RStatic, RStatic -> r1
       | RVar (Free rid0), RVar (Free rid1) ->
-          let rid = match_rid rid0 rid1 in
-          RVar (Free rid)
+          (* The projection types should have been normalized *)
+          sanity_check __FILE__ __LINE__ (rid0 = RegionId.zero) span;
+          sanity_check __FILE__ __LINE__ (rid1 = RegionId.zero) span;
+          RVar (Free RegionId.zero)
       | _ -> raise (Distinct "match_rtys")
     in
     match_types span ctx0 ctx1 match_distinct_types match_regions ty0 ty1
@@ -1417,27 +1401,41 @@ struct
     let value = ALoan (AMutLoan (PNone, id, av)) in
     { value; ty }
 
-  let match_aproj_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0 sv_id0
-      proj_ty0 children0 _ty1 pm1 sv_id1 proj_ty1 children1 ty proj_ty =
+  let match_aproj_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0
+      (proj0 : aproj_borrows) _ty1 pm1 (proj1 : aproj_borrows) ty proj_ty =
     sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-    sanity_check __FILE__ __LINE__ (children0 = [] && children1 = []) span;
+    let { proj = proj0; loans = loans0 } = proj0 in
+    let { proj = proj1; loans = loans1 } = proj1 in
+    sanity_check __FILE__ __LINE__ (loans0 = [] && loans1 = []) span;
     (* We only want to match the ids of the symbolic values, but in order
        to call [match_symbolic_values] we need to have types... *)
-    let sv0 = { sv_id = sv_id0; sv_ty = proj_ty0 } in
-    let sv1 = { sv_id = sv_id1; sv_ty = proj_ty1 } in
+    let sv0 = { sv_id = proj0.sv_id; sv_ty = proj0.proj_ty } in
+    let sv1 = { sv_id = proj1.sv_id; sv_ty = proj1.proj_ty } in
     let sv = match_symbolic_values ctx0 ctx1 sv0 sv1 in
-    { value = ASymbolic (PNone, AProjBorrows (sv.sv_id, proj_ty, [])); ty }
+    let proj : symbolic_proj = { sv_id = sv.sv_id; proj_ty } in
+    { value = ASymbolic (PNone, AProjBorrows { proj; loans = [] }); ty }
 
-  let match_aproj_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0 sv_id0
-      proj_ty0 children0 _ty1 pm1 sv_id1 proj_ty1 children1 ty proj_ty =
+  let match_aproj_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0
+      (proj0 : aproj_loans) _ty1 pm1 (proj1 : aproj_loans) ty proj_ty =
     sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
-    sanity_check __FILE__ __LINE__ (children0 = [] && children1 = []) span;
+    let { proj = proj0; consumed = consumed0; borrows = borrows0 } : aproj_loans
+        =
+      proj0
+    in
+    let { proj = proj1; consumed = consumed1; borrows = borrows1 } : aproj_loans
+        =
+      proj1
+    in
+    sanity_check __FILE__ __LINE__ (consumed0 = [] && consumed1 = []) span;
+    sanity_check __FILE__ __LINE__ (borrows0 = [] && borrows1 = []) span;
     (* We only want to match the ids of the symbolic values, but in order
        to call [match_symbolic_values] we need to have types... *)
-    let sv0 = { sv_id = sv_id0; sv_ty = proj_ty0 } in
-    let sv1 = { sv_id = sv_id1; sv_ty = proj_ty1 } in
+    let sv0 = { sv_id = proj0.sv_id; sv_ty = proj0.proj_ty } in
+    let sv1 = { sv_id = proj1.sv_id; sv_ty = proj1.proj_ty } in
     let sv = match_symbolic_values ctx0 ctx1 sv0 sv1 in
-    { value = ASymbolic (PNone, AProjLoans (sv.sv_id, proj_ty, [])); ty }
+    let proj : symbolic_proj = { sv_id = sv.sv_id; proj_ty } in
+    let proj = AProjLoans { proj; consumed = []; borrows = [] } in
+    { value = ASymbolic (PNone, proj); ty }
 
   let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 =
     log#ldebug
@@ -1468,10 +1466,6 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
       ref
         (Id.InjSubst.of_list (List.map (fun x -> (x, x)) (Id.Set.elements ids)))
   end in
-  let rid_map =
-    let module IdMap = IdMap (RegionId) in
-    IdMap.mk_map_ref fixed_ids.rids
-  in
   let blid_map =
     let module IdMap = IdMap (BorrowId) in
     IdMap.mk_map_ref fixed_ids.blids
@@ -1503,7 +1497,6 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
   let module S : MatchCheckEquivState = struct
     let span = span
     let check_equiv = check_equiv
-    let rid_map = rid_map
     let blid_map = blid_map
     let borrow_id_map = borrow_id_map
     let loan_id_map = loan_id_map
@@ -1520,12 +1513,11 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
 
   (* Small utility: check that ids are fixed/mapped to themselves *)
   let ids_are_fixed (ids : ids_sets) : bool =
-    let { aids; blids = _; borrow_ids; loan_ids; dids; rids; sids } = ids in
+    let { aids; blids = _; borrow_ids; loan_ids; dids; sids } = ids in
     AbstractionId.Set.subset aids fixed_ids.aids
     && BorrowId.Set.subset borrow_ids fixed_ids.borrow_ids
     && BorrowId.Set.subset loan_ids fixed_ids.loan_ids
     && DummyVarId.Set.subset dids fixed_ids.dids
-    && RegionId.Set.subset rids fixed_ids.rids
     && SymbolicValueId.Set.subset sids fixed_ids.sids
   in
 
@@ -1537,7 +1529,6 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
       can_end = can_end0;
       parents = parents0;
       original_parents = original_parents0;
-      regions = { owned = regions0; ancestors = ancestors_regions0 };
       avalues = avalues0;
     } =
       abs0
@@ -1549,7 +1540,6 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
       can_end = can_end1;
       parents = parents1;
       original_parents = original_parents1;
-      regions = { owned = regions1; ancestors = ancestors_regions1 };
       avalues = avalues1;
     } =
       abs1
@@ -1560,8 +1550,6 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
       raise (Distinct "match_abstractions: kind or can_end");
     let _ = CEM.match_aids parents0 parents1 in
     let _ = CEM.match_aidl original_parents0 original_parents1 in
-    let _ = CEM.match_rids regions0 regions1 in
-    let _ = CEM.match_rids ancestors_regions0 ancestors_regions1 in
 
     log#ldebug (lazy "match_abstractions: matching values");
     let _ =
@@ -1582,9 +1570,7 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
     log#ldebug
       (lazy
         ("match_ctxs: match_envs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
-       ^ "\n\n- rid_map: "
-        ^ RegionId.InjSubst.show_t !rid_map
-        ^ "\n- blid_map: "
+       ^ "\n" ^ "\n- blid_map: "
         ^ BorrowId.InjSubst.show_t !blid_map
         ^ "\n- sid_map: "
         ^ SymbolicValueId.InjSubst.show_t !sid_map
@@ -1670,7 +1656,6 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
         blid_map = !blid_map;
         borrow_id_map = !borrow_id_map;
         loan_id_map = !loan_id_map;
-        rid_map = !rid_map;
         sid_map = !sid_map;
         sid_to_value_map = !sid_to_value_map;
       }
@@ -2064,10 +2049,10 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
       method! visit_aproj env p =
         match p with
         | AProjLoans _ -> super#visit_aproj env p
-        | AProjBorrows (sv_id, proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
+        | AProjBorrows { proj = { sv_id; proj_ty }; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span;
             let sv_id = register_symbolic_value_id sv_id in
-            AProjBorrows (sv_id, proj_ty, children)
+            AProjBorrows { proj = { sv_id; proj_ty }; loans }
         | _ -> super#visit_aproj env p
     end
   in
@@ -2133,8 +2118,6 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
 
     let fresh_id = fresh_region_id
   end) in
-  let get_region_id = RegionIdGen.get_id in
-
   let module AbstractionIdGen = MkGenerator (struct
     include AbstractionId.Map
 
@@ -2143,7 +2126,6 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
     let fresh_id = fresh_abstraction_id
   end) in
   let get_abs_id = AbstractionIdGen.get_id in
-
   let visit_src =
     object (self)
       inherit [_] map_eval_ctx as super
@@ -2200,9 +2182,10 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
 
       method! visit_aproj env proj =
         match proj with
-        | AProjLoans (sv_id, proj_ty, children) ->
+        | AProjLoans { proj = { sv_id; proj_ty }; consumed; borrows } ->
             (* The logic is similar to the concrete borrows/loans cases above *)
-            sanity_check __FILE__ __LINE__ (children = []) span;
+            sanity_check __FILE__ __LINE__ (consumed = []) span;
+            sanity_check __FILE__ __LINE__ (borrows = []) span;
             let sv_id =
               begin
                 match
@@ -2219,9 +2202,9 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
               end
             in
             let proj_ty = self#visit_ty env proj_ty in
-            AProjLoans (sv_id, proj_ty, children)
-        | AProjBorrows (sv_id, proj_ty, children) ->
-            sanity_check __FILE__ __LINE__ (children = []) span;
+            AProjLoans { proj = { sv_id; proj_ty }; consumed; borrows }
+        | AProjBorrows { proj = { sv_id; proj_ty }; loans } ->
+            sanity_check __FILE__ __LINE__ (loans = []) span;
             (* Lookup the loan corresponding to this borrow *)
             let src_lid =
               SymbolicValueId.InjSubst.find sv_id
@@ -2241,7 +2224,7 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
               end
             in
             let proj_ty = self#visit_ty env proj_ty in
-            AProjBorrows (sv_id, proj_ty, children)
+            AProjBorrows { proj = { sv_id; proj_ty }; loans }
         | AEndedProjBorrows _ | AEndedProjLoans _ | AEmpty ->
             super#visit_aproj env proj
 
@@ -2250,21 +2233,6 @@ let loop_match_ctx_with_target (config : config) (span : Meta.span)
           "Internal error: region ids should not be visited directly; the \
            visitor should catch cases that contain region ids earlier."
 
-      method! visit_RVar _ var =
-        match var with
-        | Free id ->
-            (* If the bound region is free, then it is a region owned
-               by an abstraction, so we do the same as for the case
-               [abs_region_id]. *)
-            RVar (Free (get_region_id id))
-        | Bound _ -> RVar var
-
-      method! visit_abs_regions _ regions =
-        let { owned; ancestors } = regions in
-        let owned = RegionId.Set.map get_region_id owned in
-        let ancestors = RegionId.Set.map get_region_id ancestors in
-        { owned; ancestors }
-
       (** We also need to change the abstraction kind *)
       method! visit_abs env abs =
         match abs.kind with
diff --git a/src/interp/InterpreterProjectors.ml b/src/interp/InterpreterProjectors.ml
index 3de8c339e..027abd19f 100644
--- a/src/interp/InterpreterProjectors.ml
+++ b/src/interp/InterpreterProjectors.ml
@@ -14,31 +14,28 @@ let log = Logging.projectors_log
 
 (** [ty] shouldn't contain erased regions *)
 let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx)
-    (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t)
-    (v : typed_value) (ty : rty) : abstract_shared_borrows =
-  (* Sanity check - TODO: move those elsewhere (here we perform the check at every
-   * recursive call which is a bit overkill...) *)
-  let ety = Subst.erase_regions ty in
-  sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) span;
+    (fresh_reborrow : BorrowId.id -> BorrowId.id) (v : typed_value)
+    (proj_ty : proj_ty) : abstract_shared_borrows =
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
-  if not (ty_has_regions_in_set regions ty) then []
+  if not (ty_has_free_regions proj_ty) then []
   else
-    match (v.value, ty) with
+    match (v.value, proj_ty) with
     | VLiteral _, TLiteral _ -> []
     | VAdt adt, TAdt { id; generics } ->
         (* Retrieve the types of the fields *)
-        let field_types =
+        let get_field_types =
           Assoc.ctx_adt_get_inst_norm_field_rtypes span ctx id adt.variant_id
-            generics
         in
+        let field_types = get_field_types generics in
 
         (* Project over the field values *)
-        let fields_types = List.combine adt.field_values field_types in
+        let fields_types =
+          Collections.List.combine adt.field_values field_types
+        in
         let proj_fields =
           List.map
             (fun (fv, fty) ->
-              apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow
-                regions fv fty)
+              apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow fv fty)
             fields_types
         in
         List.concat proj_fields
@@ -51,8 +48,8 @@ let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx)
           | VMutBorrow (bid, bv), RMut ->
               (* Apply the projection on the borrowed value *)
               let asb =
-                apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow
-                  regions bv ref_ty
+                apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow bv
+                  ref_ty
               in
               (bid, asb)
           | VSharedBorrow bid, RShared ->
@@ -64,7 +61,7 @@ let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx)
                 | _, Concrete (VSharedLoan (_, sv))
                 | _, Abstract (ASharedLoan (_, _, sv, _)) ->
                     apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow
-                      regions sv ref_ty
+                      sv ref_ty
                 | _ -> craise __FILE__ __LINE__ span "Unexpected"
               in
               (bid, asb)
@@ -76,7 +73,7 @@ let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx)
         let asb =
           (* Check if the region is in the set of projected regions (note that
            * we never project over static regions) *)
-          if region_in_set r regions then
+          if region_is_free r then
             let bid' = fresh_reborrow bid in
             AsbBorrow bid' :: asb
           else asb
@@ -84,42 +81,40 @@ let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx)
         asb
     | VLoan _, _ -> craise __FILE__ __LINE__ span "Unreachable"
     | VSymbolic s, _ ->
-        (* Check that the projection doesn't contain ended regions *)
+        (* Check that the projection doesn't contain ended regions (i.e.,
+           the symbolic value doesn't contain bottom) *)
         sanity_check __FILE__ __LINE__
-          (not
-             (projections_intersect span s.sv_ty ctx.ended_regions ty regions))
+          (not (symbolic_value_contains_bottom span ctx s))
           span;
-        [ AsbProjReborrows (s.sv_id, ty) ]
+        [ AsbProjReborrows { sv_id = s.sv_id; proj_ty } ]
     | _ -> craise __FILE__ __LINE__ span "Unreachable"
 
 let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
     (ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id)
-    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
-    (v : typed_value) (ty : rty) : typed_avalue =
-  (* Sanity check - TODO: move this elsewhere (here we perform the check at every
-   * recursive call which is a bit overkill...) *)
-  let ety = Substitute.erase_regions ty in
-  sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) span;
+    (v : typed_value) (proj_ty : proj_ty) : typed_avalue =
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
-  if not (ty_has_regions_in_set regions ty) then
-    { value = AIgnored (Some v); ty }
+  if not (ty_has_free_regions proj_ty) then
+    { value = AIgnored (Some v); ty = proj_ty }
   else
     let value : avalue =
-      match (v.value, ty) with
+      match (v.value, proj_ty) with
       | VLiteral _, TLiteral _ -> AIgnored (Some v)
       | VAdt adt, TAdt { id; generics } ->
           (* Retrieve the types of the fields *)
-          let field_types =
+          let get_field_types =
             Assoc.ctx_adt_get_inst_norm_field_rtypes span ctx id adt.variant_id
-              generics
           in
+          let field_types = get_field_types generics in
+
           (* Project over the field values *)
-          let fields_types = List.combine adt.field_values field_types in
+          let fields_types =
+            Collections.List.combine adt.field_values field_types
+          in
           let proj_fields =
             List.map
               (fun (fv, fty) ->
                 apply_proj_borrows span check_symbolic_no_ended ctx
-                  fresh_reborrow regions ancestors_regions fv fty)
+                  fresh_reborrow fv fty)
               fields_types
           in
           AAdt { variant_id = adt.variant_id; field_values = proj_fields }
@@ -127,8 +122,8 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
       | VBorrow bc, TRef (r, ref_ty, kind) ->
           if
             (* Check if the region is in the set of projected regions (note that
-             * we never project over static regions) *)
-            region_in_set r regions
+               we never project over static regions) *)
+            region_is_free r
           then
             (* In the set *)
             let bc =
@@ -137,7 +132,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
                   (* Apply the projection on the borrowed value *)
                   let bv =
                     apply_proj_borrows span check_symbolic_no_ended ctx
-                      fresh_reborrow regions ancestors_regions bv ref_ty
+                      fresh_reborrow bv ref_ty
                   in
                   AMutBorrow (PNone, bid, bv)
               | VSharedBorrow bid, RShared ->
@@ -161,21 +156,18 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
             ABorrow bc
           else
             (* Not in the set: ignore the borrow, but project the borrowed
-               value (maybe some borrows *inside* the borrowed value are in
-               the region set) *)
+               value (the projection type is not empty, so there should be
+               some borrows *inside* the borrowed value that need to be projected) *)
             let bc =
               match (bc, kind) with
               | VMutBorrow (bid, bv), RMut ->
                   (* Apply the projection on the borrowed value *)
                   let bv =
                     apply_proj_borrows span check_symbolic_no_ended ctx
-                      fresh_reborrow regions ancestors_regions bv ref_ty
-                  in
-                  (* If the borrow id is in the ancestor's regions, we still need
-                   * to remember it *)
-                  let opt_bid =
-                    if region_in_set r ancestors_regions then Some bid else None
+                      fresh_reborrow bv ref_ty
                   in
+                  (* We need to remember the borrow, even though we ignore it *)
+                  let opt_bid = Some bid in
                   (* Return *)
                   AIgnoredMutBorrow (opt_bid, bv)
               | VSharedBorrow bid, RShared ->
@@ -187,7 +179,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
                     | _, Concrete (VSharedLoan (_, sv))
                     | _, Abstract (ASharedLoan (_, _, sv, _)) ->
                         apply_proj_borrows_on_shared_borrow span ctx
-                          fresh_reborrow regions sv ref_ty
+                          fresh_reborrow sv ref_ty
                     | _ -> craise __FILE__ __LINE__ span "Unexpected"
                   in
                   AProjSharedBorrow asb
@@ -200,33 +192,24 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool)
       | VLoan _, _ -> craise __FILE__ __LINE__ span "Unreachable"
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
-           * if necessary *)
-          if check_symbolic_no_ended then (
-            let ty1 = s.sv_ty in
-            let rset1 = ctx.ended_regions in
-            let ty2 = ty in
-            let rset2 = regions in
-            log#ltrace
-              (lazy
-                ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
-               ^ "\n- rset1: "
-                ^ RegionId.Set.to_string None rset1
-                ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
-                ^ RegionId.Set.to_string None rset2
-                ^ "\n"));
+             if necessary *)
+          if check_symbolic_no_ended then
             sanity_check __FILE__ __LINE__
-              (not (projections_intersect span ty1 rset1 ty2 rset2))
-              span);
-          ASymbolic (PNone, AProjBorrows (s.sv_id, ty, []))
+              (not (symbolic_value_contains_bottom span ctx s))
+              span;
+          ASymbolic
+            ( PNone,
+              AProjBorrows { proj = { sv_id = s.sv_id; proj_ty }; loans = [] }
+            )
       | _ ->
           log#ltrace
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
               ^ typed_value_to_string ~span:(Some span) ctx v
-              ^ "\n- proj rty: " ^ ty_to_string ctx ty));
+              ^ "\n- proj_ty: " ^ ty_to_string ctx proj_ty));
           internal_error __FILE__ __LINE__ span
     in
-    { value; ty }
+    { value; ty = proj_ty }
 
 let symbolic_expansion_non_borrow_to_value (span : Meta.span)
     (sv : symbolic_value) (see : symbolic_expansion) : typed_value =
@@ -260,65 +243,61 @@ let symbolic_expansion_non_shared_borrow_to_value (span : Meta.span)
 (** Apply (and reduce) a projector over loans to a value.
 
     Remark: we need the evaluation context only to access the type declarations.
+    Remark: the projection type should have been normalized (i.e., the regions
+    we should project should be free regions of id 0, and the regions we want to
+    ignore should have been erased).
 
     TODO: detailed comments. See [apply_proj_borrows] *)
 let apply_proj_loans_on_symbolic_expansion (span : Meta.span)
-    (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t)
-    (see : symbolic_expansion) (original_sv_ty : rty) (proj_ty : rty)
-    (ctx : eval_ctx) : typed_avalue =
+    (see : symbolic_expansion) (proj_ty : proj_ty) (ctx : eval_ctx) :
+    typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  sanity_check __FILE__ __LINE__
-    (ty_has_regions_in_set regions original_sv_ty)
-    span;
+  sanity_check __FILE__ __LINE__ (ty_has_free_regions proj_ty) span;
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, proj_ty) with
     | SeLiteral lit, TLiteral _ ->
-        ( AIgnored (Some { value = VLiteral lit; ty = original_sv_ty }),
-          original_sv_ty )
+        (AIgnored (Some { value = VLiteral lit; ty = proj_ty }), proj_ty)
     | SeAdt (variant_id, field_values), TAdt { id = adt_id; generics } ->
         (* Project over the field values *)
-        let field_types =
+        let get_field_types =
           AssociatedTypes.ctx_adt_get_inst_norm_field_rtypes span ctx adt_id
-            variant_id generics
+            variant_id
         in
+        let field_types = get_field_types generics in
         let field_values =
-          List.map2
-            (mk_aproj_loans_value_from_symbolic_value regions)
+          Collections.List.map2 mk_aproj_loans_value_from_symbolic_value
             field_values field_types
         in
-        (AAdt { variant_id; field_values }, original_sv_ty)
+        (AAdt { variant_id; field_values }, proj_ty)
     | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
         (* Sanity check *)
         sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) span;
+
         (* Apply the projector to the borrowed value *)
-        let child_av =
-          mk_aproj_loans_value_from_symbolic_value regions spc ref_ty
-        in
+        let child_av = mk_aproj_loans_value_from_symbolic_value spc ref_ty in
         (* Check if the region is in the set of projected regions (note that
-         * we never project over static regions) *)
-        if region_in_set r regions then
+           we never project over static regions) *)
+        if region_is_free r then
           (* In the set: keep *)
           (ALoan (AMutLoan (PNone, bid, child_av)), ref_ty)
         else
-          (* Not in the set: ignore *)
+          (* Not in the set: check if the inner type has regions we might
+             need to project. *)
           (* If the borrow id is in the ancestor's regions, we still need
            * to remember it *)
-          let opt_bid =
-            if region_in_set r ancestors_regions then Some bid else None
-          in
+          let opt_bid = if ty_has_free_regions ref_ty then Some bid else None in
           (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
         (* Sanity check *)
         sanity_check __FILE__ __LINE__ (spc.sv_ty = ref_ty) span;
+
         (* Apply the projector to the borrowed value *)
-        let child_av =
-          mk_aproj_loans_value_from_symbolic_value regions spc ref_ty
-        in
+        let child_av = mk_aproj_loans_value_from_symbolic_value spc ref_ty in
         (* Check if the region is in the set of projected regions (note that
-         * we never project over static regions) *)
-        if region_in_set r regions then
+           we never project over static regions) *)
+        if region_is_free r then
           (* In the set: keep *)
           let shared_value = mk_typed_value_from_symbolic_value spc in
           (ALoan (ASharedLoan (PNone, bids, shared_value, child_av)), ref_ty)
@@ -466,11 +445,9 @@ let apply_reborrows (span : Meta.span)
             in
             (* Update and explore *)
             super#visit_ASharedLoan env pm bids sv av
-        | AIgnoredSharedLoan _
-        | AMutLoan (_, _, _)
+        | AIgnoredSharedLoan _ | AMutLoan _
         | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-        | AEndedSharedLoan (_, _)
-        | AIgnoredMutLoan (_, _)
+        | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan
             { given_back = _; child = _; given_back_meta = _ } ->
             (* Nothing particular to do *)
@@ -511,10 +488,8 @@ let prepare_reborrows (config : config) (span : Meta.span)
 
 (** [ty] shouldn't have erased regions *)
 let apply_proj_borrows_on_input_value (config : config) (span : Meta.span)
-    (ctx : eval_ctx) (regions : RegionId.Set.t)
-    (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
+    (ctx : eval_ctx) (v : typed_value) (proj_ty : proj_ty) :
     eval_ctx * typed_avalue =
-  sanity_check __FILE__ __LINE__ (ty_is_rty ty) span;
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
   (* Prepare the reborrows *)
@@ -523,8 +498,7 @@ let apply_proj_borrows_on_input_value (config : config) (span : Meta.span)
   in
   (* Apply the projector *)
   let av =
-    apply_proj_borrows span check_symbolic_no_ended ctx fresh_reborrow regions
-      ancestors_regions v ty
+    apply_proj_borrows span check_symbolic_no_ended ctx fresh_reborrow v proj_ty
   in
   (* Apply the reborrows *)
   let ctx = apply_registered_reborrows ctx in
diff --git a/src/interp/InterpreterProjectors.mli b/src/interp/InterpreterProjectors.mli
index 50307dd94..b3c296c16 100644
--- a/src/interp/InterpreterProjectors.mli
+++ b/src/interp/InterpreterProjectors.mli
@@ -11,14 +11,7 @@ open Contexts
     Parameters: [regions] [ancestor_regions] [see] [original_sv_ty]: shouldn't
     have erased regions [proj_ty]: shouldn't have erased regions [eval_ctx] *)
 val apply_proj_loans_on_symbolic_expansion :
-  Meta.span ->
-  RegionId.Set.t ->
-  RegionId.Set.t ->
-  symbolic_expansion ->
-  rty ->
-  rty ->
-  eval_ctx ->
-  typed_avalue
+  Meta.span -> symbolic_expansion -> proj_ty -> eval_ctx -> typed_avalue
 
 (** Convert a symbolic expansion *which is not a borrow* to a value *)
 val symbolic_expansion_non_borrow_to_value :
@@ -104,10 +97,8 @@ val apply_proj_borrows :
   bool ->
   eval_ctx ->
   (BorrowId.id -> BorrowId.id) ->
-  RegionId.Set.t ->
-  RegionId.Set.t ->
   typed_value ->
-  rty ->
+  proj_ty ->
   typed_avalue
 
 (** Parameters:
@@ -122,8 +113,6 @@ val apply_proj_borrows_on_input_value :
   config ->
   Meta.span ->
   eval_ctx ->
-  RegionId.Set.t ->
-  RegionId.Set.t ->
   typed_value ->
-  rty ->
+  proj_ty ->
   eval_ctx * typed_avalue
diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml
index fd15e171e..a7e3dfe0c 100644
--- a/src/interp/InterpreterStatements.ml
+++ b/src/interp/InterpreterStatements.ml
@@ -7,6 +7,7 @@ open Contexts
 open LlbcAst
 open Cps
 open InterpreterUtils
+open InterpreterBorrowsCore
 open InterpreterProjectors
 open InterpreterExpansion
 open InterpreterPaths
@@ -113,7 +114,7 @@ let assign_to_place (config : config) (span : Meta.span) (rv : typed_value)
   (* Write to the destination *)
   (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
   exec_assert __FILE__ __LINE__
-    (not (bottom_in_value ctx.ended_regions rv))
+    (not (bottom_in_value span ctx rv))
     span "The value to move contains bottom";
   (* Update the destination *)
   let ctx = write_place span Write p rv ctx in
@@ -355,7 +356,7 @@ let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool)
     | None -> ()
     | Some ret_value ->
         sanity_check __FILE__ __LINE__
-          (not (bottom_in_value ctx.ended_regions ret_value))
+          (not (bottom_in_value span ctx ret_value))
           span
   in
 
@@ -492,18 +493,10 @@ let eval_builtin_function_call_concrete (config : config) (span : Meta.span)
     which can end or not. *)
 let create_empty_abstractions_from_abs_region_groups
     (kind : RegionGroupId.id -> abs_kind) (rgl : abs_region_group list)
-    (region_can_end : RegionGroupId.id -> bool) : abs list =
-  (* We use a reference to progressively create a map from abstraction ids
-   * to set of ancestor regions. Note that {!abs_to_ancestors_regions} [abs_id]
-   * returns the union of:
-   * - the regions of the ancestors of abs_id
-   * - the regions of abs_id
-   *)
-  let abs_to_ancestors_regions : RegionId.Set.t AbstractionId.Map.t ref =
-    ref AbstractionId.Map.empty
-  in
+    (region_can_end : RegionGroupId.id -> bool) : (region_id_set * abs) list =
   (* Auxiliary function to create one abstraction *)
-  let create_abs (rg_id : RegionGroupId.id) (rg : abs_region_group) : abs =
+  let create_abs (rg_id : RegionGroupId.id) (rg : abs_region_group) :
+      region_id_set * abs =
     let abs_id = rg.id in
     let original_parents = rg.parents in
     let parents =
@@ -511,34 +504,21 @@ let create_empty_abstractions_from_abs_region_groups
         (fun s pid -> AbstractionId.Set.add pid s)
         AbstractionId.Set.empty rg.parents
     in
-    let regions =
-      let owned = RegionId.Set.of_list rg.regions in
-      let ancestors =
-        List.fold_left
-          (fun acc parent_id ->
-            RegionId.Set.union acc
-              (AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
-          RegionId.Set.empty rg.parents
-      in
-      { owned; ancestors }
-    in
-    let ancestors_regions_union_current_regions =
-      RegionId.Set.union regions.owned regions.owned
-    in
+    let regions = rg.regions in
     let can_end = region_can_end rg_id in
-    abs_to_ancestors_regions :=
-      AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
-        !abs_to_ancestors_regions;
     (* Create the abstraction *)
-    {
-      abs_id;
-      kind = kind rg_id;
-      can_end;
-      parents;
-      original_parents;
-      regions;
-      avalues = [];
-    }
+    let abs =
+      {
+        abs_id;
+        kind = kind rg_id;
+        can_end;
+        parents;
+        original_parents;
+        avalues = [];
+      }
+    in
+    (* Return *)
+    (RegionId.Set.of_list regions, abs)
   in
   (* Apply *)
   RegionGroupId.mapi create_abs rgl
@@ -546,7 +526,8 @@ let create_empty_abstractions_from_abs_region_groups
 let create_push_abstractions_from_abs_region_groups
     (kind : RegionGroupId.id -> abs_kind) (rgl : abs_region_group list)
     (region_can_end : RegionGroupId.id -> bool)
-    (compute_abs_avalues : abs -> eval_ctx -> eval_ctx * typed_avalue list)
+    (compute_abs_avalues :
+      region_id_set -> eval_ctx -> eval_ctx * typed_avalue list)
     (ctx : eval_ctx) : eval_ctx =
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let empty_absl =
@@ -555,9 +536,10 @@ let create_push_abstractions_from_abs_region_groups
 
   (* Compute and add the avalues to the abstractions, the insert the abstractions
    * in the context. *)
-  let insert_abs (ctx : eval_ctx) (abs : abs) : eval_ctx =
+  let insert_abs (ctx : eval_ctx) ((regions, abs) : region_id_set * abs) :
+      eval_ctx =
     (* Compute the values to insert in the abstraction *)
-    let ctx, avalues = compute_abs_avalues abs ctx in
+    let ctx, avalues = compute_abs_avalues regions ctx in
     (* Add the avalues to the abstraction *)
     let abs = { abs with avalues } in
     (* Insert the abstraction in the context *)
@@ -1331,10 +1313,12 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
 
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.output in
-  let ret_spc = mk_fresh_symbolic_value span ret_sv_ty in
+  let ret_spc = mk_fresh_symbolic_value span (erase_regions ret_sv_ty) in
   let ret_value = mk_typed_value_from_symbolic_value ret_spc in
   let ret_av regions =
-    mk_aproj_loans_value_from_symbolic_value regions ret_spc ret_sv_ty
+    (* Normalize the type by masking only the regions we want to project *)
+    let ret_sv_ty = normalize_proj_ty regions ret_sv_ty in
+    mk_aproj_loans_value_from_symbolic_value ret_spc ret_sv_ty
   in
   let args_places =
     List.map (fun p -> S.mk_opt_place_from_op span p ctx) args
@@ -1372,18 +1356,19 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
    * First, we define the function which, given an initialized, empty
    * abstraction, computes the avalues which should be inserted inside.
    *)
-  let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
+  let compute_abs_avalues (regions : region_id_set) (ctx : eval_ctx) :
       eval_ctx * typed_avalue list =
     (* Project over the input values *)
     let ctx, args_projs =
       List.fold_left_map
         (fun ctx (arg, arg_rty) ->
-          apply_proj_borrows_on_input_value config span ctx abs.regions.owned
-            abs.regions.ancestors arg arg_rty)
+          (* Normalize the type by masking only the regions we want to project *)
+          let arg_rty = normalize_proj_ty regions arg_rty in
+          apply_proj_borrows_on_input_value config span ctx arg arg_rty)
         ctx args_with_rtypes
     in
     (* Group the input and output values *)
-    (ctx, List.append args_projs [ ret_av abs.regions.owned ])
+    (ctx, List.append args_projs [ ret_av regions ])
   in
   (* Actually initialize and insert the abstractions *)
   let call_id = fresh_fun_call_id () in
diff --git a/src/interp/InterpreterStatements.mli b/src/interp/InterpreterStatements.mli
index afbba613a..f801605ed 100644
--- a/src/interp/InterpreterStatements.mli
+++ b/src/interp/InterpreterStatements.mli
@@ -45,7 +45,7 @@ val create_push_abstractions_from_abs_region_groups :
   (RegionGroupId.id -> abs_kind) ->
   abs_region_group list ->
   (RegionGroupId.id -> bool) ->
-  (abs -> eval_ctx -> eval_ctx * typed_avalue list) ->
+  (region_id_set -> eval_ctx -> eval_ctx * typed_avalue list) ->
   eval_ctx ->
   eval_ctx
 
diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml
index 62abb6295..7433ac381 100644
--- a/src/interp/InterpreterUtils.ml
+++ b/src/interp/InterpreterUtils.ml
@@ -88,7 +88,7 @@ let mk_place_from_var_id (ctx : eval_ctx) (span : Meta.span)
 let mk_fresh_symbolic_value_opt_span (span : Meta.span option) (ty : ty) :
     symbolic_value =
   (* Sanity check *)
-  sanity_check_opt_span __FILE__ __LINE__ (ty_is_rty ty) span;
+  sanity_check_opt_span __FILE__ __LINE__ (ty_is_ety ty) span;
   let sv_id = fresh_symbolic_value_id () in
   let svalue = { sv_id; sv_ty = ty } in
   svalue
@@ -123,12 +123,25 @@ let mk_fresh_symbolic_typed_value_from_no_regions_ty (span : Meta.span)
     Checks if the projector will actually project some regions. If not, returns
     {!Values.AIgnored} ([_]).
 
+    Note that the projection type should have been *normalized* (only the
+    projected regions should be free regions - with id 0 - and the others should
+    have been erased).
+
     TODO: update to handle 'static *)
-let mk_aproj_loans_value_from_symbolic_value (proj_regions : RegionId.Set.t)
-    (svalue : symbolic_value) (proj_ty : ty) : typed_avalue =
-  if ty_has_regions_in_set proj_regions proj_ty then
-    let av = ASymbolic (PNone, AProjLoans (svalue.sv_id, proj_ty, [])) in
-    let av : typed_avalue = { value = av; ty = svalue.sv_ty } in
+let mk_aproj_loans_value_from_symbolic_value (svalue : symbolic_value)
+    (proj_ty : ty) : typed_avalue =
+  if ty_has_free_regions proj_ty then
+    let av =
+      ASymbolic
+        ( PNone,
+          AProjLoans
+            {
+              proj = { sv_id = svalue.sv_id; proj_ty };
+              consumed = [];
+              borrows = [];
+            } )
+    in
+    let av : typed_avalue = { value = av; ty = proj_ty } in
     av
   else
     {
@@ -136,13 +149,14 @@ let mk_aproj_loans_value_from_symbolic_value (proj_regions : RegionId.Set.t)
       ty = svalue.sv_ty;
     }
 
-(** Create a borrows projector from a symbolic value *)
+(** Create a borrows projector from a symbolic value.
+
+    Note that the projection type should have been normalized. *)
 let mk_aproj_borrows_from_symbolic_value (span : Meta.span)
-    (proj_regions : RegionId.Set.t) (svalue : symbolic_value) (proj_ty : ty) :
-    aproj =
+    (svalue : symbolic_value) (proj_ty : ty) : aproj =
   sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) span;
-  if ty_has_regions_in_set proj_regions proj_ty then
-    AProjBorrows (svalue.sv_id, proj_ty, [])
+  if ty_has_free_regions proj_ty then
+    AProjBorrows { proj = { sv_id = svalue.sv_id; proj_ty }; loans = [] }
   else AEmpty
 
 (** TODO: move *)
@@ -208,13 +222,10 @@ exception FoundGBorrowContent of g_borrow_content
 exception FoundGLoanContent of g_loan_content
 
 (** Utility exception *)
-exception
-  FoundAProjBorrows of
-    symbolic_value_id * ty * (msymbolic_value_id * aproj) list
+exception FoundAProjBorrows of aproj_borrows
 
 (** Utility exception *)
-exception
-  FoundAProjLoans of symbolic_value_id * ty * (msymbolic_value_id * aproj) list
+exception FoundAProjLoans of aproj_loans
 
 exception FoundAbsProj of abstraction_id * symbolic_value_id
 
@@ -229,8 +240,8 @@ let symbolic_value_id_in_ctx (sv_id : SymbolicValueId.id) (ctx : eval_ctx) :
 
       method! visit_aproj env aproj =
         (match aproj with
-        | AProjLoans (sv_id1, _, _) | AProjBorrows (sv_id1, _, _) ->
-            if sv_id1 = sv_id then raise Found else ()
+        | AProjLoans { proj; _ } | AProjBorrows { proj; _ } ->
+            if proj.sv_id = sv_id then raise Found else ()
         | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ());
         super#visit_aproj env aproj
 
@@ -238,8 +249,8 @@ let symbolic_value_id_in_ctx (sv_id : SymbolicValueId.id) (ctx : eval_ctx) :
         let visit (asb : abstract_shared_borrow) : unit =
           match asb with
           | AsbBorrow _ -> ()
-          | AsbProjReborrows (sv_id1, _) ->
-              if sv_id1 = sv_id then raise Found else ()
+          | AsbProjReborrows proj ->
+              if proj.sv_id = sv_id then raise Found else ()
         in
         List.iter visit asb
     end
@@ -250,52 +261,6 @@ let symbolic_value_id_in_ctx (sv_id : SymbolicValueId.id) (ctx : eval_ctx) :
     false
   with Found -> true
 
-(** Check that a symbolic value doesn't contain ended regions.
-
-    Note that we don't check that the set of ended regions is empty: we check
-    that the set of ended regions doesn't intersect the set of regions used in
-    the type (this is more general). *)
-let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
-    (s : symbolic_value) : bool =
-  let regions = ty_regions s.sv_ty in
-  not (RegionId.Set.disjoint regions ended_regions)
-
-let region_is_owned (abs : abs) (r : region) : bool =
-  match r with
-  | RVar (Free rid) -> RegionId.Set.mem rid abs.regions.owned
-  | _ -> false
-
-let bottom_in_value_visitor (ended_regions : RegionId.Set.t) =
-  object
-    inherit [_] iter_typed_value
-    method! visit_VBottom _ = raise Found
-
-    method! visit_symbolic_value _ s =
-      if symbolic_value_has_ended_regions ended_regions s then raise Found
-      else ()
-  end
-
-(** Check if a {!type:Values.value} contains [⊥].
-
-    Note that this function is very general: it also checks wether symbolic
-    values contain already ended regions. *)
-let bottom_in_value (ended_regions : RegionId.Set.t) (v : typed_value) : bool =
-  let obj = bottom_in_value_visitor ended_regions in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    false
-  with Found -> true
-
-let bottom_in_adt_value (ended_regions : RegionId.Set.t) (v : adt_value) : bool
-    =
-  let obj = bottom_in_value_visitor ended_regions in
-  (* We use exceptions *)
-  try
-    obj#visit_adt_value () v;
-    false
-  with Found -> true
-
 let value_has_ret_symbolic_value_with_borrow_under_mut span (ctx : eval_ctx)
     (v : typed_value) : bool =
   let obj =
@@ -354,10 +319,6 @@ type ids_sets = {
   borrow_ids : BorrowId.Set.t;  (** Only the borrow ids *)
   loan_ids : BorrowId.Set.t;  (** Only the loan ids *)
   dids : DummyVarId.Set.t;
-  rids : RegionId.Set.t;
-      (** This should only contain **free** region ids (note that we have to be
-          careful because we use the same index type for bound regions and free
-          regions - see the implementation of [compute_ids] below) *)
   sids : SymbolicValueId.Set.t;
 }
 [@@deriving show]
@@ -373,7 +334,6 @@ let compute_ids () =
   let loan_ids = ref BorrowId.Set.empty in
   let aids = ref AbstractionId.Set.empty in
   let dids = ref DummyVarId.Set.empty in
-  let rids = ref RegionId.Set.empty in
   let sids = ref SymbolicValueId.Set.empty in
   let sids_to_values = ref SymbolicValueId.Map.empty in
 
@@ -384,7 +344,6 @@ let compute_ids () =
       borrow_ids = !borrow_ids;
       loan_ids = !loan_ids;
       dids = !dids;
-      rids = !rids;
       sids = !sids;
     }
   in
@@ -409,15 +368,6 @@ let compute_ids () =
           "Region ids should not be visited directly; the visitor should catch \
            cases that contain region ids earlier."
 
-      method! visit_RVar _ var =
-        match var with
-        | Free id -> rids := RegionId.Set.add id !rids
-        | Bound _ -> ()
-
-      method! visit_abs_regions _ (regions : abs_regions) : unit =
-        let { owned; ancestors } = regions in
-        rids := RegionId.Set.union (RegionId.Set.union owned ancestors) !rids
-
       method! visit_symbolic_value env sv =
         sids := SymbolicValueId.Set.add sv.sv_id !sids;
         sids_to_values := SymbolicValueId.Map.add sv.sv_id sv !sids_to_values;
@@ -498,7 +448,6 @@ let initialize_eval_ctx (span : Meta.span option) (ctx : decls_ctx)
     const_generic_vars_map;
     norm_trait_types = TraitTypeRefMap.empty (* Empty for now *);
     env = [ EFrame ];
-    ended_regions = RegionId.Set.empty;
   }
 
 (** Instantiate a function signature, introducing **fresh** abstraction ids and
diff --git a/src/interp/Invariants.ml b/src/interp/Invariants.ml
index 0ac5c7d6e..04916c14a 100644
--- a/src/interp/Invariants.ml
+++ b/src/interp/Invariants.ml
@@ -346,7 +346,7 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit =
           | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } ->
               set_outer_mut info
           | AEndedSharedLoan (_, _) -> set_outer_shared info
-          | AIgnoredMutLoan (_, _) -> set_outer_mut info
+          | AIgnoredMutLoan _ -> set_outer_mut info
           | AEndedIgnoredMutLoan
               { given_back = _; child = _; given_back_meta = _ } ->
               set_outer_mut info
@@ -409,6 +409,13 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
     inherit [_] iter_eval_ctx as super
     method! visit_abs _ abs = super#visit_abs (Some abs) abs
 
+    method! visit_region _ r =
+      (* All free regions should have id 0 because we normalize the projection types *)
+      match r with
+      | RVar (Free rid) ->
+          sanity_check __FILE__ __LINE__ (rid = RegionId.zero) span
+      | _ -> ()
+
     method! visit_EBinding info binder v =
       (* We also check that the regions are erased *)
       sanity_check __FILE__ __LINE__ (ty_is_ety v.ty) span;
@@ -546,16 +553,14 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
       super#visit_typed_value info tv
 
     (* TODO: there is a lot of duplication with {!visit_typed_value}
-     * which is quite annoying. There might be a way of factorizing
-     * that by factorizing the definitions of value and avalue, but
-     * the generation of visitors then doesn't work properly (TODO:
-     * report that). Still, it is actually not that problematic
-     * because this code shouldn't change a lot in the future,
-     * so the cost of maintenance should be pretty low.
+       which is quite annoying. There might be a way of factorizing
+       that by factorizing the definitions of value and avalue, but
+       the generation of visitors then doesn't work properly (TODO:
+       report that). Still, it is actually not that problematic
+       because this code shouldn't change a lot in the future,
+       so the cost of maintenance should be pretty low.
      *)
     method! visit_typed_avalue info atv =
-      (* Check that the types have regions *)
-      sanity_check __FILE__ __LINE__ (ty_is_rty atv.ty) span;
       (* Check the current pair (value, type) *)
       (match (atv.value, atv.ty) with
       (* ADT case *)
@@ -620,17 +625,16 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
           | _ -> craise __FILE__ __LINE__ span "Erroneous type")
       | ABottom, _ -> (* Nothing to check *) ()
       | ABorrow bc, TRef (region, ref_ty, rkind) -> (
-          let abs = Option.get info in
           (* Check the borrow content *)
           match (bc, rkind) with
           | AMutBorrow (_, _, av), RMut ->
               (* Check that the region is owned by the abstraction *)
-              sanity_check __FILE__ __LINE__ (region_is_owned abs region) span;
+              sanity_check __FILE__ __LINE__ (region_is_free region) span;
               (* Check that the child value has the proper type *)
               sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span
           | ASharedBorrow (_, bid), RShared -> (
               (* Check that the region is owned by the abstraction *)
-              sanity_check __FILE__ __LINE__ (region_is_owned abs region) span;
+              sanity_check __FILE__ __LINE__ (region_is_free region) span;
               if lookups then
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan span ek_all bid ctx in
@@ -650,7 +654,6 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
           | AProjSharedBorrow _, RShared -> ()
           | _ -> craise __FILE__ __LINE__ span "Inconsistent context")
       | ALoan lc, aty -> (
-          let abs = Option.get info in
           match lc with
           | AMutLoan (_, bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
             -> (
@@ -659,9 +662,7 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
               begin
                 match lc with
                 | AMutLoan _ ->
-                    sanity_check __FILE__ __LINE__
-                      (region_is_owned abs region)
-                      span
+                    sanity_check __FILE__ __LINE__ (region_is_free region) span
                 | _ -> ()
               end;
               let borrowed_aty = aloan_get_expected_child_type aty in
@@ -687,7 +688,7 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
             ->
               (* Check that the region is owned by the abstraction *)
               let region, _, _ = ty_as_ref aty in
-              sanity_check __FILE__ __LINE__ (region_is_owned abs region) span;
+              sanity_check __FILE__ __LINE__ (region_is_free region) span;
               let borrowed_aty = aloan_get_expected_child_type aty in
               sanity_check __FILE__ __LINE__
                 (sv.ty = Substitute.erase_regions borrowed_aty)
@@ -701,9 +702,7 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
               begin
                 match lc with
                 | AEndedMutLoan _ ->
-                    sanity_check __FILE__ __LINE__
-                      (region_is_owned abs region)
-                      span
+                    sanity_check __FILE__ __LINE__ (region_is_free region) span
                 | _ -> ()
               end;
               let borrowed_aty = aloan_get_expected_child_type aty in
@@ -715,27 +714,25 @@ let check_typing_invariant_visitor span ctx (lookups : bool) =
                 span)
       | ASymbolic (_, aproj), ty -> (
           match aproj with
-          | AProjLoans (sv_id, proj_ty, _) ->
-              check_symbolic_value_type sv_id ty;
-              let abs = Option.get info in
+          | AProjLoans { proj; _ } ->
+              check_symbolic_value_type proj.sv_id ty;
               sanity_check __FILE__ __LINE__
-                (ty_has_regions_in_set abs.regions.owned proj_ty)
+                (ty_has_free_regions proj.proj_ty)
                 span
-          | AProjBorrows (sv_id, proj_ty, _) ->
-              check_symbolic_value_type sv_id ty;
-              let abs = Option.get info in
+          | AProjBorrows { proj; _ } ->
+              check_symbolic_value_type proj.sv_id ty;
               sanity_check __FILE__ __LINE__
-                (ty_has_regions_in_set abs.regions.owned proj_ty)
+                (ty_has_free_regions proj.proj_ty)
                 span
-          | AEndedProjLoans (_msv, given_back_ls) ->
+          | AEndedProjLoans { proj = _; consumed; borrows } ->
               List.iter
                 (fun (_, proj) ->
                   match proj with
-                  | AProjBorrows (_sv, ty', _) ->
-                      sanity_check __FILE__ __LINE__ (ty' = ty) span
+                  | AProjBorrows { proj; _ } | AProjLoans { proj; _ } ->
+                      sanity_check __FILE__ __LINE__ (proj.proj_ty = ty) span
                   | AEndedProjBorrows _ | AEmpty -> ()
                   | _ -> craise __FILE__ __LINE__ span "Unexpected")
-                given_back_ls
+                (consumed @ borrows)
           | AEndedProjBorrows _ | AEmpty -> ())
       | AIgnored _, _ -> ()
       | _ ->
@@ -758,17 +755,12 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) (lookups : bool)
 
 type proj_borrows_info = {
   abs_id : AbstractionId.id;
-  regions : RegionId.Set.t;
   proj_ty : rty;  (** The regions shouldn't be erased *)
   as_shared_value : bool;  (** True if the value is below a shared borrow *)
 }
 [@@deriving show]
 
-type proj_loans_info = {
-  abs_id : AbstractionId.id;
-  regions : RegionId.Set.t;
-  proj_ty : rty;
-}
+type proj_loans_info = { abs_id : AbstractionId.id; proj_ty : rty }
 [@@deriving show]
 
 type sv_info = {
@@ -780,22 +772,18 @@ type sv_info = {
 
 let proj_borrows_info_to_string (ctx : eval_ctx) (info : proj_borrows_info) :
     string =
-  let { abs_id; regions; proj_ty; as_shared_value } = info in
+  let { abs_id; proj_ty; as_shared_value } = info in
   "{ abs_id = "
   ^ AbstractionId.to_string abs_id
-  ^ "; regions = "
-  ^ RegionId.Set.to_string None regions
   ^ "; proj_ty = " ^ ty_to_string ctx proj_ty ^ "; as_shared_value = "
   ^ Print.bool_to_string as_shared_value
   ^ "}"
 
 let proj_loans_info_to_string (ctx : eval_ctx) (info : proj_loans_info) : string
     =
-  let { abs_id; regions; proj_ty } = info in
+  let { abs_id; proj_ty } = info in
   "{ abs_id = "
   ^ AbstractionId.to_string abs_id
-  ^ "; regions = "
-  ^ RegionId.Set.to_string None regions
   ^ "; proj_ty = " ^ ty_to_string ctx proj_ty ^ "}"
 
 let sv_info_to_string (ctx : eval_ctx) (info : sv_info) : string =
@@ -836,16 +824,16 @@ let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit =
     let info = { info with env_count = info.env_count + 1 } in
     update_info sv_id info
   in
-  let add_aproj_borrows (sv : symbolic_value_id) abs_id regions proj_ty
-      as_shared_value : unit =
+  let add_aproj_borrows (sv : symbolic_value_id) abs_id proj_ty as_shared_value
+      : unit =
     let info = lookup_info sv in
-    let binfo = { abs_id; regions; proj_ty; as_shared_value } in
+    let binfo = { abs_id; proj_ty; as_shared_value } in
     let info = { info with aproj_borrows = binfo :: info.aproj_borrows } in
     update_info sv info
   in
-  let add_aproj_loans (sv : symbolic_value_id) proj_ty abs_id regions : unit =
+  let add_aproj_loans (sv : symbolic_value_id) proj_ty abs_id : unit =
     let info = lookup_info sv in
-    let linfo = { abs_id; regions; proj_ty } in
+    let linfo = { abs_id; proj_ty } in
     let info = { info with aproj_loans = linfo :: info.aproj_loans } in
     update_info sv info
   in
@@ -860,16 +848,16 @@ let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit =
         let abs = Option.get abs in
         match asb with
         | AsbBorrow _ -> ()
-        | AsbProjReborrows (sv, proj_ty) ->
-            add_aproj_borrows sv abs.abs_id abs.regions.owned proj_ty true
+        | AsbProjReborrows proj ->
+            add_aproj_borrows proj.sv_id abs.abs_id proj.proj_ty true
 
       method! visit_aproj abs aproj =
         (let abs = Option.get abs in
          match aproj with
-         | AProjLoans (sv, proj_ty, _) ->
-             add_aproj_loans sv proj_ty abs.abs_id abs.regions.owned
-         | AProjBorrows (sv, proj_ty, _) ->
-             add_aproj_borrows sv abs.abs_id abs.regions.owned proj_ty false
+         | AProjLoans { proj; _ } ->
+             add_aproj_loans proj.sv_id proj.proj_ty abs.abs_id
+         | AProjBorrows { proj; _ } ->
+             add_aproj_borrows proj.sv_id abs.abs_id proj.proj_ty false
          | AEndedProjLoans _ | AEndedProjBorrows _ | AEmpty -> ());
         super#visit_aproj abs aproj
     end
@@ -892,12 +880,11 @@ let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit =
       sanity_check __FILE__ __LINE__
         (info.aproj_borrows = [] || info.aproj_loans <> [])
         span;
-      (* Check that the loan projections don't intersect and compute
-         the normalized union of those projections *)
+      (* Check that the loan projections don't intersect by
+         computing their union. *)
       let aproj_loans =
         List.map
-          (fun (linfo : proj_loans_info) ->
-            normalize_proj_ty linfo.regions linfo.proj_ty)
+          (fun (linfo : proj_loans_info) -> linfo.proj_ty)
           info.aproj_loans
       in
 
@@ -915,8 +902,7 @@ let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit =
       (* Check that the union of the loan projectors contains the borrow projections. *)
       let aproj_borrows =
         List.map
-          (fun (linfo : proj_borrows_info) ->
-            normalize_proj_ty linfo.regions linfo.proj_ty)
+          (fun (linfo : proj_borrows_info) -> linfo.proj_ty)
           info.aproj_borrows
       in
       match aproj_borrows with
diff --git a/src/llbc/Contexts.ml b/src/llbc/Contexts.ml
index 9c99d4a06..3de8018c5 100644
--- a/src/llbc/Contexts.ml
+++ b/src/llbc/Contexts.ml
@@ -69,6 +69,8 @@ type eval_ctx = {
   type_ctx : type_ctx;
   fun_ctx : fun_ctx;
   region_groups : RegionGroupId.id list;
+      (** Region groups of the function we are symbolically executing (in case
+          we are performing a symbolic execution) *)
   type_vars : type_var list;
   const_generic_vars : const_generic_var list;
   const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
@@ -83,7 +85,6 @@ type eval_ctx = {
           representatives). Note that this doesn't take into account
           higher-order type constraints (of the shape `for<'a> ...`). *)
   env : env;
-  ended_regions : RegionId.Set.t;
 }
 [@@deriving show]
 
diff --git a/src/llbc/Print.ml b/src/llbc/Print.ml
index c85a660a8..7fbd4a2d3 100644
--- a/src/llbc/Print.ml
+++ b/src/llbc/Print.ml
@@ -11,6 +11,7 @@ open Expressions
 open LlbcAst
 open Contexts
 open Errors
+open Utils
 module Types = Charon.PrintTypes
 module Expressions = Charon.PrintExpressions
 
@@ -115,8 +116,8 @@ module Values = struct
       (abs : abstract_shared_borrow) : string =
     match abs with
     | AsbBorrow bid -> BorrowId.to_string bid
-    | AsbProjReborrows (sv_id, rty) ->
-        "{" ^ symbolic_value_proj_to_string env sv_id rty ^ "}"
+    | AsbProjReborrows proj ->
+        "{" ^ symbolic_value_proj_to_string env proj.sv_id proj.proj_ty ^ "}"
 
   let abstract_shared_borrows_to_string (env : fmt_env)
       (abs : abstract_shared_borrows) : string =
@@ -127,57 +128,78 @@ module Values = struct
   let rec aproj_to_string ?(with_ended : bool = false) (env : fmt_env)
       (pv : aproj) : string =
     match pv with
-    | AProjLoans (sv, rty, given_back) ->
-        let given_back =
-          if given_back = [] then ""
+    | AProjLoans { proj; consumed; borrows } ->
+        let consumed =
+          if consumed = [] then ""
           else
-            let given_back = List.map snd given_back in
-            let given_back =
-              List.map (aproj_to_string ~with_ended env) given_back
+            let consumed = List.map snd consumed in
+            let consumed =
+              List.map (aproj_to_string ~with_ended env) consumed
             in
-            " [" ^ String.concat "," given_back ^ "]"
+            ", consumed=[" ^ String.concat "," consumed ^ "]"
         in
-        "⌊" ^ symbolic_value_proj_to_string env sv rty ^ given_back ^ "⌋"
-    | AProjBorrows (sv, rty, given_back) ->
-        let given_back =
-          if given_back = [] then ""
+        let borrows =
+          if borrows = [] then ""
           else
-            let given_back = List.map snd given_back in
-            let given_back =
-              List.map (aproj_to_string ~with_ended env) given_back
-            in
-            " [" ^ String.concat "," given_back ^ "]"
+            let borrows = List.map snd borrows in
+            let borrows = List.map (aproj_to_string ~with_ended env) borrows in
+            ", borrows=[" ^ String.concat "," borrows ^ "]"
         in
-        "(" ^ symbolic_value_proj_to_string env sv rty ^ given_back ^ ")"
-    | AEndedProjLoans (msv, given_back) ->
+        "⌊"
+        ^ symbolic_value_proj_to_string env proj.sv_id proj.proj_ty
+        ^ consumed ^ borrows ^ "⌋"
+    | AProjBorrows { proj; loans } ->
+        let loans =
+          if loans = [] then ""
+          else
+            let loans = List.map snd loans in
+            let loans = List.map (aproj_to_string ~with_ended env) loans in
+            ", loans=[" ^ String.concat "," loans ^ "]"
+        in
+        "("
+        ^ symbolic_value_proj_to_string env proj.sv_id proj.proj_ty
+        ^ loans ^ ")"
+    | AEndedProjLoans { proj = msv; consumed; borrows } ->
         let msv =
           if with_ended then
             "original_loan = " ^ symbolic_value_id_to_pretty_string msv
           else "_"
         in
-        let given_back = List.map snd given_back in
-        let given_back =
-          List.map (aproj_to_string ~with_ended env) given_back
+        let consumed =
+          if consumed = [] then ""
+          else
+            let consumed = List.map snd consumed in
+            let consumed =
+              List.map (aproj_to_string ~with_ended env) consumed
+            in
+            ", consumed=[" ^ String.concat "," consumed ^ "]"
+        in
+        let borrows =
+          if borrows = [] then ""
+          else
+            let borrows = List.map snd borrows in
+            let borrows = List.map (aproj_to_string ~with_ended env) borrows in
+            ", borrows=[" ^ String.concat "," borrows ^ "]"
         in
-        "ended_aproj_loans (" ^ msv ^ ", ["
-        ^ String.concat "," given_back
-        ^ "])"
-    | AEndedProjBorrows (meta, given_back) ->
+
+        "ended_aproj_loans (" ^ msv ^ consumed ^ borrows ^ ")"
+    | AEndedProjBorrows { mvalues; loans } ->
         let meta =
           if with_ended then
             "original_borrow = "
-            ^ symbolic_value_id_to_pretty_string meta.consumed
+            ^ symbolic_value_id_to_pretty_string mvalues.consumed
             ^ ", given_back = "
-            ^ symbolic_value_to_string env meta.given_back
+            ^ symbolic_value_to_string env mvalues.given_back
           else "_"
         in
-        let given_back = List.map snd given_back in
-        let given_back =
-          List.map (aproj_to_string ~with_ended env) given_back
+        let loans =
+          if loans = [] then ""
+          else
+            let loans = List.map snd loans in
+            let loans = List.map (aproj_to_string ~with_ended env) loans in
+            ", loans=[" ^ String.concat "," loans ^ "]"
         in
-        "ended_aproj_borrows (" ^ meta ^ ", ["
-        ^ String.concat "," given_back
-        ^ "])"
+        "ended_aproj_borrows (" ^ meta ^ loans ^ "])"
     | AEmpty -> "_"
 
   (** Wrap a value inside its marker, if there is one *)
@@ -370,8 +392,6 @@ module Values = struct
     ^ AbstractionId.to_string abs.abs_id
     ^ "{" ^ kind ^ "parents="
     ^ AbstractionId.Set.to_string None abs.parents
-    ^ ",regions="
-    ^ RegionId.Set.to_string None abs.regions.owned
     ^ "," ^ can_end ^ "} {\n" ^ avs ^ "\n" ^ indent ^ "}"
 
   let abs_region_group_to_string (gr : abs_region_group) : string =
@@ -456,10 +476,45 @@ module Contexts = struct
         env_elem_to_string ~span env verbose with_var_types indent indent_incr
           ev
 
-  (** Filters "dummy" bindings from an environment, to gain space and clarity/
+  (** Small helper to check whether a value is a dummy value or not.
+
+      This is is an approximation because checking whether a symbolic value
+      contains live borrows is non-trivial, and the helpers to do this are
+      introduced later. For now, we simply check whether symbolic values contain
+      borrows in their types: if yes, we consider that they contain non-ended
+      borrows. It is ok to be approximate because we do this only for printing
+      purposes. *)
+  let value_has_non_ended_borrows_or_loans_approx type_infos (v : value) : bool
+      =
+    let value_visitor =
+      object
+        inherit [_] iter_typed_value
+        method! visit_borrow_content _ _ = raise Found
+        method! visit_loan_content _ _ = raise Found
+
+        method! visit_symbolic_value _ sv =
+          (* This is an approximation: we only check whether the *type* of the
+             symbolic value contains borrows *)
+          if TypesUtils.ty_has_borrows None type_infos sv.sv_ty then raise Found
+          else ()
+      end
+    in
+    (* We use exceptions *)
+    try
+      value_visitor#visit_value () v;
+      false
+    with Found -> true
+
+  (** Filters "dummy" bindings from an environment, to gain space and clarity
+      (dummy bindings are bindings which map to values which do not contain
+      borrows or loans).
+
+      Remark: we have to do something approximate, because checking whether a
+      symbolic value contains non-ended borrows is non trivial (we need to
+      lookup all the borrow projectors in the environment).
+
       See [env_to_string]. *)
-  let filter_env (ended_regions : RegionId.Set.t) (env : env) :
-      env_elem option list =
+  let filter_env type_infos (env : env) : env_elem option list =
     (* We filter:
        - non-dummy bindings which point to ⊥
        - dummy bindings which don't contain loans nor borrows
@@ -473,8 +528,8 @@ module Contexts = struct
           if is_bottom tv.value then None else Some ev
       | EBinding (BDummy _, tv) ->
           (* Dummy binding: check if the value contains borrows or loans *)
-          if value_has_non_ended_borrows_or_loans ended_regions tv.value then
-            Some ev
+          if value_has_non_ended_borrows_or_loans_approx type_infos tv.value
+          then Some ev
           else None
       | _ -> Some ev
     in
@@ -495,9 +550,9 @@ module Contexts = struct
       type of the variables *)
   let env_to_string ?(span : Meta.span option = None) (filter : bool)
       (fmt_env : fmt_env) (verbose : bool) (with_var_types : bool)
-      (ended_regions : RegionId.Set.t) (env : env) : string =
+      (ctx : eval_ctx) (env : env) : string =
     let env =
-      if filter then filter_env ended_regions env
+      if filter then filter_env ctx.type_ctx.type_infos env
       else List.map (fun ev -> Some ev) env
     in
     "{\n"
@@ -564,7 +619,6 @@ module Contexts = struct
       ?(verbose : bool = false) ?(filter : bool = true)
       ?(with_var_types : bool = true) (ctx : eval_ctx) : string =
     let fmt_env = eval_ctx_to_fmt_env ctx in
-    let ended_regions = RegionId.Set.to_string None ctx.ended_regions in
     let frames = split_env_according_to_frames ctx.env in
     let num_frames = List.length frames in
     let frames =
@@ -585,13 +639,11 @@ module Contexts = struct
           ^ string_of_int !num_bindings
           ^ "\n- dummy bindings: " ^ string_of_int !num_dummies
           ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
-          ^ env_to_string ~span filter fmt_env verbose with_var_types
-              ctx.ended_regions f
+          ^ env_to_string ~span filter fmt_env verbose with_var_types ctx f
           ^ "\n")
         frames
     in
-    "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
-    ^ " frame(s)\n" ^ String.concat "" frames
+    "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames
 end
 
 (** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *)
diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml
index 62a2f3cb5..faa5843d1 100644
--- a/src/llbc/Substitute.ml
+++ b/src/llbc/Substitute.ml
@@ -112,12 +112,6 @@ let subst_ids_visitor (subst : id_subst) =
         "Region ids should not be visited directly; the visitor should catch \
          cases that contain region ids earlier."
 
-    method! visit_abs_regions _ regions =
-      let { owned; ancestors } = regions in
-      let owned = RegionId.Set.map subst.r_subst owned in
-      let ancestors = RegionId.Set.map subst.r_subst ancestors in
-      { owned; ancestors }
-
     method! visit_RVar _ var =
       match var with
       | Free rid -> RVar (Free (subst.r_subst rid))
diff --git a/src/llbc/Types.ml b/src/llbc/Types.ml
index 1a8edb0e5..35a703037 100644
--- a/src/llbc/Types.ml
+++ b/src/llbc/Types.ml
@@ -1,3 +1,13 @@
 include Charon.Types
 
 type region_id_set = RegionId.Set.t [@@deriving show, ord]
+
+(** A normalized projection type.
+
+    A type where regions are either:
+    - the free region of id 0 (the regions we want to keep during a projection)
+    - erased (the regions we want to discard during a projection)
+
+    Note that using this type (rather than, e.g., [ty]) only has an informative
+    purpose. *)
+type proj_ty = ty [@@deriving show, ord]
diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml
index 107f5319b..3a5070c26 100644
--- a/src/llbc/TypesAnalysis.ml
+++ b/src/llbc/TypesAnalysis.ml
@@ -2,6 +2,8 @@ open Types
 open LlbcAst
 open Errors
 open Substitute
+open Charon.TypesUtils
+open SCC
 
 let log = Logging.types_analysis_log
 
@@ -463,3 +465,334 @@ let analyze_ty (span : Meta.span option) (infos : type_infos) (ty : ty) :
   let ty_info = analyze_full_ty span updated infos ty_info ty in
   (* Convert the ty_info *)
   partial_type_info_to_ty_info ty_info
+
+(** Small helper *)
+type region_kind = RkMarked | RkStatic | RkDefault
+
+(** Given a normalized projection type (a projection type is a type which allows
+    to mask a set of regions appearing in a type - this is useful when putting
+    borrows into region abstractions: we use projection types to determine in
+    which region to insert the borrow; a *normalized* projection type is a
+    projection type where regions are either a free region of id 0 if we want to
+    keep the region, and erased if we want to discard it), compute the same type
+    but which projects the regions which outlive the regions in the current
+    projection.
+
+    Note however that we ignore the static regions: static regions outlive all
+    other regions so in theory we should include them in the outlive type, but
+    in practice we handle them differently.
+
+    Ex.: compute_outlive_ty (&'0 mut T) = &'_ mut T (the original projection
+    projects the borrow, the outlive projection is empty)
+
+    compute_outlive_ty (&'0 mut &'_ mut T) = &'_ mut &'0 mut T (the original
+    projection projects the *outer* borrow, the outlive projection projects the
+    *inner* borrow)
+
+    compute_outlive_ty (&'0 (Wrapper<'_, T>)) = &'_ (Wrapper<'0, T>) where
+    struct Wrapper<'a, T>(&'a mut T) (the outlive projection projects the region
+    inside the ADT) *)
+let compute_outlive_proj_ty (span : Meta.span option)
+    (type_decls : type_decl TypeDeclId.Map.t) (ty : ty) : ty =
+  (* The method is as follows:
+
+     1. We visit the type to introduce a fresh identifier for every region,
+     and compute an "outlive" graph. From the outlive graph we can determine whether
+     a region outlives static or a masked region. Note that computing this outlive
+     graph is necessary to properly handle outlive constraints that are implied,
+     for instance, by ADTs.
+
+     2. We then visit the type again to keep the non-masked regions which outlive
+     a mask region and don't outlive 'static ('static has its own treatment),
+     and erase the others.
+  *)
+  let _, fresh_region_id = RegionId.fresh_stateful_generator () in
+  (* The outlive graph. If r0 maps to r1, it means r0 outlives r1. *)
+  let graph = ref RegionMap.empty in
+
+  (* We reserve the region of id 0 *)
+  let zero_id = fresh_region_id () in
+  let zero = RVar (Free zero_id) in
+
+  (* r0 outlives r1 *)
+  let add_outlive (r0 : region) (r1 : region) =
+    graph :=
+      RegionMap.update r0
+        (fun s ->
+          let s = Option.get s in
+          Some (RegionSet.add r1 s))
+        !graph
+  in
+
+  let add_region (masked : bool) (rid : RegionId.id) : region =
+    let r = RVar (Free rid) in
+    sanity_check_opt_span __FILE__ __LINE__ (not (RegionMap.mem r !graph)) span;
+    graph := RegionMap.add r RegionSet.empty !graph;
+    if masked then add_outlive r zero;
+    r
+  in
+  let _ = add_region false zero_id in
+
+  let fresh_region masked = add_region masked (fresh_region_id ()) in
+
+  let add_static (r : region) : unit = add_outlive r RStatic in
+
+  (* [r] outlives the regions in [outlived] *)
+  let add_outlives r (outlived : region list) =
+    List.iter (fun r' -> add_outlive r r') outlived
+  in
+
+  (* Visit to compute the constraints *)
+  let visitor =
+    object (self)
+      inherit [_] map_ty as super
+
+      (* Generate a fresh region, register it, and save the fact that it outlives
+         all the regions inside which we had to dive so far *)
+      method! visit_region outer r =
+        let r =
+          match r with
+          | RErased -> fresh_region false
+          | RVar (Free _) -> fresh_region true
+          | RVar (Bound _) ->
+              craise_opt_span __FILE__ __LINE__ span "Not handled yet"
+          | RStatic ->
+              let r = fresh_region false in
+              add_static r;
+              r
+        in
+        add_outlives r outer;
+        r
+
+      method! visit_generic_args outer generics =
+        (* TODO: we need to handle those *)
+        sanity_check_opt_span __FILE__ __LINE__ (generics.trait_refs = []) span;
+        super#visit_generic_args outer generics
+
+      method! visit_ty outer ty =
+        match ty with
+        | TAdt adt -> begin
+            (* TODO: we need to handle those *)
+            sanity_check_opt_span __FILE__ __LINE__
+              (adt.generics.trait_refs = [])
+              span;
+            match adt.id with
+            | TAdtId id ->
+                (* Lookup the declaration and use the region constraints
+                   to check which regions outlive the masked regions. *)
+                let decl =
+                  silent_unwrap_opt_span __FILE__ __LINE__ span
+                    (TypeDeclId.Map.find_opt id type_decls)
+                in
+                let { regions; types; const_generics; trait_refs } =
+                  adt.generics
+                in
+                let regions = List.map (self#visit_region outer) regions in
+                let types = List.map (self#visit_ty outer) types in
+                let const_generics =
+                  List.map (self#visit_const_generic outer) const_generics
+                in
+                let generics : generic_args =
+                  { regions; types; const_generics; trait_refs }
+                in
+
+                (* Substitute in the constraints *)
+                let subst =
+                  Charon.Substitute.make_subst_from_generics decl.generics
+                    generics
+                in
+                let params =
+                  Charon.Substitute.predicates_substitute subst decl.generics
+                in
+
+                (* Update the graph following the outlive *)
+                let {
+                  regions = _;
+                  types = _;
+                  const_generics = _;
+                  trait_clauses = _;
+                  regions_outlive;
+                  types_outlive;
+                  trait_type_constraints = _;
+                } =
+                  params
+                in
+
+                (* [r0] outlives [r1] *)
+                let visit_region_register_outlive r0 r1 =
+                  match r1 with
+                  | RVar (Bound _) ->
+                      craise_opt_span __FILE__ __LINE__ span
+                        "Bound regions are not handled yet"
+                  | RVar (Free _) -> add_outlives r0 [ r1 ]
+                  | RStatic | RErased ->
+                      internal_error_opt_span __FILE__ __LINE__ span
+                in
+
+                let outlive_visitor =
+                  object
+                    inherit [_] iter_ty
+
+                    (* [r1] outlives [r0] *)
+                    method! visit_region r0 r1 =
+                      visit_region_register_outlive r1 r0
+                  end
+                in
+
+                (* Visit the region outlives constraints (the first region outlives the second)  *)
+                List.iter
+                  (fun (pred : (region, region) outlives_pred region_binder) ->
+                    cassert_opt_span __FILE__ __LINE__
+                      (pred.binder_regions = []) span
+                      "Bound regions are not supported yet";
+                    let r0, r1 = pred.binder_value in
+                    visit_region_register_outlive r0 r1)
+                  regions_outlive;
+
+                (* Visit the type outlives constraints (the type outlives the region) *)
+                List.iter
+                  (fun (pred : (ty, region) outlives_pred region_binder) ->
+                    cassert_opt_span __FILE__ __LINE__
+                      (pred.binder_regions = []) span
+                      "Bound regions are not supported yet";
+                    let ty, r = pred.binder_value in
+                    outlive_visitor#visit_ty r ty)
+                  types_outlive;
+
+                (* Mask the regions which outlive a masked region, erase the masked
+                   regions and the regions which outlive 'static *)
+                let generics = { regions; types; const_generics; trait_refs } in
+                TAdt { adt with generics }
+            | TTuple -> super#visit_ty outer ty
+            | TBuiltin builtin_ty -> (
+                match builtin_ty with
+                | TBox | TArray | TSlice | TStr -> super#visit_ty outer ty)
+          end
+        | TVar _ | TLiteral _ | TNever -> ty
+        | TRef (r, ref_ty, kind) ->
+            let r = self#visit_region outer r in
+            let outer = r :: outer in
+            let ref_ty = self#visit_ty outer ref_ty in
+            TRef (r, ref_ty, kind)
+        | TTraitType (tref, _) ->
+            (* TODO: normalize the trait types.
+               For now we only emit a warning because it makes some tests fail. *)
+            cassert_warn_opt_span __FILE__ __LINE__
+              (not (trait_instance_id_reducible span tref.trait_id))
+              span
+              "Found an unexpected trait impl associated type which was not \
+               inlined while analyzing a type. This is a case we currently do \
+               not handle in all generality. As a result,the consumed/given \
+               back values computed for the generated backward functions may \
+               be incorrect.";
+            ty
+        | TRawPtr _ | TDynTrait _ | TFnPtr _ | TFnDef _ | TError _ ->
+            (* Don't know what to do *)
+            craise_opt_span __FILE__ __LINE__ span "Not handled yet"
+    end
+  in
+  let ty = visitor#visit_ty [] ty in
+
+  (* Compute the strongly connected components, and for each of them,
+     determine whether the component:
+     - contains a masked region
+     - contains a static region
+
+     Then, we map the different regions to a masked region or an erased region
+     depending on whether they outlive an SCC containing a masked region, etc.
+  *)
+  let module Scc = SCC.Make (RegionOrderedType) in
+  let sccs = Scc.compute (RegionMap.to_list !graph) in
+
+  (* Compute, for each SCC whether it contains a marked region or a static region *)
+  let scc_kind =
+    SccId.Map.map
+      (fun ls ->
+        let has_marked = ref false in
+        let has_static = ref false in
+        List.iter
+          (fun r ->
+            match r with
+            | RVar (Free _) -> has_marked := true
+            | RStatic -> has_static := true
+            | _ -> ())
+          ls;
+        let has_marked = !has_marked in
+        let has_static = !has_static in
+        sanity_check_opt_span __FILE__ __LINE__
+          ((not has_marked) || not has_static)
+          span;
+        if has_marked then RkMarked
+        else if has_static then RkStatic
+        else RkDefault)
+      sccs.sccs
+  in
+
+  (* Compute, for each SCC, whether it outlives an SCC containing a marked or static region *)
+  let scc_kind_full = ref SccId.Map.empty in
+  let rec compute_kind (id : SccId.id) : region_kind =
+    let deps_kinds =
+      List.map compute_kind
+        (SccId.Set.to_list (SccId.Map.find id sccs.scc_deps))
+    in
+    let kind = SccId.Map.find id scc_kind in
+    let kinds = kind :: deps_kinds in
+    let has_marked = ref false in
+    let has_static = ref false in
+    List.iter
+      (fun k ->
+        match k with
+        | RkMarked -> has_marked := true
+        | RkStatic -> has_static := true
+        | RkDefault -> ())
+      kinds;
+
+    let has_marked = !has_marked in
+    let has_static = !has_static in
+    sanity_check_opt_span __FILE__ __LINE__
+      ((not has_marked) || not has_static)
+      span;
+    let kind =
+      if has_marked then RkMarked
+      else if has_static then RkStatic
+      else RkDefault
+    in
+    scc_kind_full := SccId.Map.add id kind !scc_kind_full;
+    kind
+  in
+  SccId.Map.iter
+    (fun id _ ->
+      let _ = compute_kind id in
+      ())
+    scc_kind;
+  let scc_kind_full = !scc_kind_full in
+
+  (* Compute the region substitution *)
+  let region_subst = ref RegionMap.empty in
+  SccId.Map.iter
+    (fun id regions ->
+      let kind = SccId.Map.find id scc_kind_full in
+      let rkind =
+        match kind with
+        | RkMarked -> zero
+        | RkStatic -> craise_opt_span __FILE__ __LINE__ span "Not handled yet"
+        | RkDefault -> RErased
+      in
+      List.iter
+        (fun r -> region_subst := RegionMap.add r rkind !region_subst)
+        regions)
+    sccs.sccs;
+
+  (* Substitute *)
+  let subst_visitor =
+    object
+      inherit [_] map_ty
+
+      method! visit_region _ r =
+        match r with
+        | RVar (Free _) | RErased -> RegionMap.find r !region_subst
+        | RVar (Bound _) | RStatic ->
+            craise_opt_span __FILE__ __LINE__ span "Not handled yet"
+    end
+  in
+  subst_visitor#visit_ty () ty
diff --git a/src/llbc/Values.ml b/src/llbc/Values.ml
index 9209fa70d..6f4b11ffd 100644
--- a/src/llbc/Values.ml
+++ b/src/llbc/Values.ml
@@ -171,6 +171,13 @@ type mvalue = typed_value [@@deriving show, ord]
 type msymbolic_value = symbolic_value [@@deriving show, ord]
 
 type msymbolic_value_id = symbolic_value_id [@@deriving show, ord]
+
+type mconsumed_symb = { sv_id : symbolic_value_id; proj_ty : proj_ty }
+[@@deriving show, ord]
+
+type mgiven_back_symb = { sv_id : symbolic_value_id; proj_ty : proj_ty }
+[@@deriving show, ord]
+
 type abstraction_id = AbstractionId.id [@@deriving show, ord]
 type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord]
 
@@ -199,6 +206,11 @@ class ['self] iter_typed_avalue_base =
     method visit_msymbolic_value_id : 'env -> msymbolic_value_id -> unit =
       fun _ _ -> ()
 
+    method visit_mconsumed_symb : 'env -> mconsumed_symb -> unit = fun _ _ -> ()
+
+    method visit_mgiven_back_symb : 'env -> mgiven_back_symb -> unit =
+      fun _ _ -> ()
+
     method visit_region_id_set : 'env -> region_id_set -> unit = fun _ _ -> ()
     method visit_abstraction_id : 'env -> abstraction_id -> unit = fun _ _ -> ()
 
@@ -228,6 +240,13 @@ class ['self] map_typed_avalue_base =
         'env -> msymbolic_value_id -> msymbolic_value_id =
       fun _ m -> m
 
+    method visit_mconsumed_symb : 'env -> mconsumed_symb -> mconsumed_symb =
+      fun _ m -> m
+
+    method visit_mgiven_back_symb : 'env -> mgiven_back_symb -> mgiven_back_symb
+        =
+      fun _ m -> m
+
     method visit_region_id_set : 'env -> region_id_set -> region_id_set =
       fun _ s -> s
 
@@ -261,98 +280,136 @@ class ['self] map_typed_avalue_base =
     symbolic values).
 
     TODO: we may actually need to remember the structure, in order to know which
-    borrows are inside which other borrows... *)
+    borrows are inside which other borrows...
+
+    TODO: remove once we simplify the handling of borrows. *)
 type abstract_shared_borrow =
   | AsbBorrow of borrow_id
-  | AsbProjReborrows of symbolic_value_id * ty
+  | AsbProjReborrows of symbolic_proj
 
 (** A set of abstract shared borrows *)
 and abstract_shared_borrows = abstract_shared_borrow list
 
-and aproj =
-  | AProjLoans of symbolic_value_id * ty * (msymbolic_value_id * aproj) list
-      (** A projector of loans over a symbolic value.
-
-          Whenever we call a function, we introduce a symbolic value for the
-          returned value. We insert projectors of loans over this symbolic value
-          in the abstractions introduced by this function call: those projectors
-          allow to insert the proper loans in the various abstractions whenever
-          symbolic borrows get expanded.
-
-          The borrows of a symbolic value may be spread between different
-          abstractions, meaning that *one* projector of loans might receive
-          *several* (symbolic) given back values.
-
-          This is the case in the following example:
-          {[
-            fn f<'a> (...) -> (&'a mut u32, &'a mut u32);
-            fn g<'b, 'c>(p : (&'b mut u32, &'c mut u32));
-
-            let p = f(...);
-            g(move p);
-
-            // Symbolic context after the call to g:
-            // abs'a {'a} { proj_loans   [s@0 <: (&'a mut u32, &'a mut u32)] }
-            //
-            // abs'b {'b} { proj_borrows (s@0 <: (&'b mut u32, &'c mut u32)) }
-            // abs'c {'c} { proj_borrows (s@0 <: (&'b mut u32, &'c mut u32)) }
-          ]}
+(** Remark: the projection types inside the [symbolic_proj] are redundant with
+    the types contained in the typed avalues they belong to. We duplicate those
+    types because in practice it is a lot more convenient to also have them
+    here. *)
+and symbolic_proj = {
+  sv_id : symbolic_value_id;
+  proj_ty : ty;  (** The normalized projection type *)
+}
 
-          Upon evaluating the call to [f], we introduce a symbolic value [s@0]
-          and a projector of loans (projector loans from the region 'c). This
-          projector will later receive two given back values: one for 'a and one
-          for 'b.
-
-          We accumulate those values in the list of projections (note that the
-          meta value stores the value which was given back).
-
-          We can later end the projector of loans if [s@0] is not referenced
-          anywhere in the context below a projector of borrows which intersects
-          this projector of loans.
-
-          TODO: the projection type is redundant with the type of the avalue
-          TODO: we shouldn't use a symbolic value but rather a symbolic value id
-      *)
-  | AProjBorrows of symbolic_value_id * ty * (msymbolic_value_id * aproj) list
-      (** Note that an AProjBorrows only operates on a value which is not below
-          a shared loan: under a shared loan, we use {!abstract_shared_borrow}.
-
-          Also note that once given to a borrow projection, a symbolic value
-          can't get updated/expanded: this means that we don't need to save any
-          meta-value here.
-
-          Finally, we have the same problem as with loans, that is we may need
-          to reproject loans coming from several abstractions. Consider for
-          instance what happens if we end abs1 and abs2 below: the borrow
-          projector inside of abs0 will receive parts of their given back
-          symbolic values:
-          {[
-            ...
-            abs0 {'c} { proj_borrows (s@0 : (&'a mut &'c mut u32, &'b mut &'c mut u32)) }
-            ...
+and aproj =
+  | AProjLoans of aproj_loans
+  | AProjBorrows of aproj_borrows
+  | AEndedProjLoans of aended_proj_loans
+  | AEndedProjBorrows of aended_proj_borrows
+  | AEmpty  (** Nothing to project (because there are no borrows, etc.) *)
 
-            abs1 {'a} { proj_loans (&'a mut &'c mut u32, &'b mut &'c mut u32)) }
-            abs2 {'b} { proj_loans (&'a mut &'c mut u32, &'b mut &'c mut u32)) }
-            ...
-          ]}
+(** A projector of loans over a symbolic value.
+
+    Whenever we call a function, we introduce a symbolic value for the returned
+    value. We insert projectors of loans over this symbolic value in the
+    abstractions introduced by this function call: those projectors allow to
+    insert the proper loans in the various abstractions whenever symbolic
+    borrows get expanded.
+
+    The borrows of a symbolic value may be spread between different
+    abstractions, meaning that *one* projector of loans might receive *several*
+    (symbolic) given back values.
+
+    This is the case in the following example:
+    {[
+      fn f<'a> (...) -> (&'a mut u32, &'a mut u32);
+      fn g<'b, 'c>(p : (&'b mut u32, &'c mut u32));
+
+      let p = f(...);
+      g(move p);
+
+      // Symbolic context after the call to g:
+      // abs'a {'a} { proj_loans   [s@0 <: (&'a mut u32, &'a mut u32)] }
+      //
+      // abs'b {'b} { proj_borrows (s@0 <: (&'b mut u32, &'c mut u32)) }
+      // abs'c {'c} { proj_borrows (s@0 <: (&'b mut u32, &'c mut u32)) }
+    ]}
+
+    Upon evaluating the call to [f], we introduce a symbolic value [s@0] and a
+    projector of loans (projector loans from the region 'c). This projector will
+    later receive two given back values: one for 'a and one for 'b.
+
+    We accumulate those values in the list of projections (note that the meta
+    value stores the value which was given back).
+
+    We can later end the projector of loans if [s@0] is not referenced anywhere
+    in the context below a projector of borrows which intersects this projector
+    of loans. *)
+and aproj_loans = {
+  proj : symbolic_proj;
+  consumed : (mconsumed_symb * aproj) list;
+      (** The values we consumed because part of the loans in this loan
+          projector were ended. For the reason why there is a list, see the
+          explanations below. Note that because ending the loan may require
+          ending several borrow projectors (and consuming their given back
+          values) we accumulate the consumed values here, and turn the
+          [AProjLoans] into an [AEndedProjLoans] only when there are no
+          intersecting borrow projectors left in the environment. *)
+  borrows : (mconsumed_symb * aproj) list;
+      (** The additional borrow projectors we had to introduce because some
+          ancestor region ended *)
+}
 
-          TODO: the projection type is redundant with the type of the avalue
-          TODO: we shouldn't use a symbolic value but rather a symbolic value id
-      *)
-  | AEndedProjLoans of msymbolic_value_id * (msymbolic_value_id * aproj) list
-      (** An ended projector of loans over a symbolic value.
+(** Note that an AProjBorrows only operates on a value which is not below a
+    shared loan: under a shared loan, we use {!abstract_shared_borrow}.
+
+    Also note that once given to a borrow projection, a symbolic value can't get
+    updated/expanded: this means that we don't need to save any meta-value here.
+
+    TODO: the explanations below are wrong.
+
+    Finally, we have the same problem as with loans, that is we may need to
+    reproject loans coming from several abstractions. Consider for instance what
+    happens if we end abs1 and abs2 below: the borrow projector inside of abs0
+    will receive parts of their given back symbolic values:
+    {[
+      ...
+      abs0 {'c} { proj_borrows (s@0 : (&'a mut &'c mut u32, &'b mut &'c mut u32)) }
+      ...
+
+      abs1 {'a} { proj_loans (&'a mut &'c mut u32, &'b mut &'c mut u32)) }
+      abs2 {'b} { proj_loans (&'a mut &'c mut u32, &'b mut &'c mut u32)) }
+      ...
+    ]} *)
+and aproj_borrows = {
+  proj : symbolic_proj;
+  loans : (mconsumed_symb * aproj) list;
+      (** When an ancestor region ends, we may have to project the loans
+          corresponding to its given back values. We store them here. *)
+}
 
-          See the explanations for {!AProjLoans}
+(** An ended projector of loans over a symbolic value.
+
+    See the explanations for {!AProjLoans} *)
+and aended_proj_loans = {
+  proj : msymbolic_value_id;
+      (** The id of the original symbolic value, that we preserve as a
+          meta-value *)
+  consumed : (mconsumed_symb * aproj) list;
+      (** The values we consumed because part of the loans in this loan
+          projector were ended (for the reason why there is a list, see the
+          explanations below). *)
+  borrows : (mconsumed_symb * aproj) list;
+      (** The additional borrow projectors we had to introduce because some
+          ancestor region ended *)
+}
 
-          Note that we keep the original symbolic value as a meta-value. *)
-  | AEndedProjBorrows of
-      ended_proj_borrow_meta * (msymbolic_value_id * aproj) list
-      (** The only purpose of {!AEndedProjBorrows} is to store, for synthesis
-          purposes:
+and aended_proj_borrows = {
+  mvalues : ended_proj_borrow_meta;
+      (** This stores, for synthesis purposes:
           - the symbolic value which was consumed upon creating the projection
           - the symbolic value which was generated and given back upon ending
             the borrows *)
-  | AEmpty  (** Nothing to project (because there are no borrows, etc.) *)
+  loans : (mconsumed_symb * aproj) list;
+}
 
 (** Abstraction values are used inside of abstractions to properly model
     borrowing relations introduced by function calls.
@@ -716,7 +773,10 @@ and aborrow_content =
     shared aloan has type [& (mut) T] instead of [T]). *)
 and typed_avalue = {
   value : avalue;
-  ty : ty;  (** This should be a type with regions *)
+  ty : ty;
+      (** This should be a type with *normalized* regions, that is: the type
+          should use free regions (with id 0) for the regions belonging to the
+          abstraction, and erased regions for the others. *)
 }
 [@@deriving
   show,
@@ -728,6 +788,7 @@ and typed_avalue = {
       ancestors = [ "iter_typed_avalue_base" ];
       nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
       concrete = true;
+      monomorphic = [ "env" ] (* We need this to allows duplicate field names *);
     },
   visitors
     {
@@ -736,6 +797,7 @@ and typed_avalue = {
       ancestors = [ "map_typed_avalue_base" ];
       nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
       concrete = true;
+      monomorphic = [ "env" ] (* We need this to allows duplicate field names *);
     }]
 
 (** TODO: make those variants of [abs_kind] *)
@@ -826,16 +888,8 @@ type abs = {
   original_parents : abstraction_id list;
       (** The original list of parents, ordered. This is used for synthesis.
           TODO: remove? *)
-  regions : abs_regions;
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }
-
-and abs_regions = {
-  owned : region_id_set;  (** Regions owned by the abstraction *)
-  ancestors : region_id_set;
-      (** Union of the regions owned by this abstraction's ancestors (not
-          including the regions of this abstraction itself) *)
-}
 [@@deriving
   show,
   ord,
diff --git a/src/llbc/ValuesUtils.ml b/src/llbc/ValuesUtils.ml
index 1131bbd98..a4c12f38e 100644
--- a/src/llbc/ValuesUtils.ml
+++ b/src/llbc/ValuesUtils.ml
@@ -93,11 +93,22 @@ let is_unit (v : typed_value) : bool =
 
 let mk_aproj_borrows (pm : proj_marker) (sv_id : symbolic_value_id)
     (proj_ty : ty) =
-  { value = ASymbolic (pm, AProjBorrows (sv_id, proj_ty, [])); ty = proj_ty }
+  {
+    value =
+      ASymbolic (pm, AProjBorrows { proj = { sv_id; proj_ty }; loans = [] });
+    ty = proj_ty;
+  }
 
 let mk_aproj_loans (pm : proj_marker) (sv_id : symbolic_value_id) (proj_ty : ty)
     =
-  { value = ASymbolic (pm, AProjLoans (sv_id, proj_ty, [])); ty = proj_ty }
+  {
+    value =
+      ASymbolic
+        ( pm,
+          AProjLoans { proj = { sv_id; proj_ty }; consumed = []; borrows = [] }
+        );
+    ty = proj_ty;
+  }
 
 (** Check if a value contains a *concrete* borrow (i.e., a [Borrow] value - we
     don't check if there are borrows hidden in symbolic values). *)
@@ -255,33 +266,6 @@ let value_has_borrows span (infos : TypesAnalysis.type_infos) (v : value) : bool
     false
   with Found -> true
 
-let value_has_non_ended_borrows_or_loans (ended_regions : RegionId.Set.t)
-    (v : value) : bool =
-  let ty_visitor =
-    object
-      inherit [_] iter_ty
-
-      method! visit_RVar _ region =
-        match region with
-        | Free rid ->
-            if not (RegionId.Set.mem rid ended_regions) then raise Found else ()
-        | Bound _ -> ()
-    end
-  in
-  let value_visitor =
-    object
-      inherit [_] iter_typed_value
-      method! visit_borrow_content _ _ = raise Found
-      method! visit_loan_content _ _ = raise Found
-      method! visit_symbolic_value _ sv = ty_visitor#visit_ty () sv.sv_ty
-    end
-  in
-  (* We use exceptions *)
-  try
-    value_visitor#visit_value () v;
-    false
-  with Found -> true
-
 (** Check if a value has loans.
 
     Note that loans are necessarily concrete (there can't be loans hidden inside
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index af9e97f0e..4bdcc0392 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -1957,15 +1957,17 @@ type typed_avalue_kind =
       (** No borrows, loans or projections inside the value so we can't know for
           sure *)
 
-let compute_typed_avalue_proj_kind span type_infos
-    (abs_regions : T.RegionId.Set.t) (av : V.typed_avalue) : typed_avalue_kind =
+let compute_typed_avalue_proj_kind span type_infos (av : V.typed_avalue) :
+    typed_avalue_kind =
   let has_borrows = ref false in
   let has_mut_borrows = ref false in
   let has_loans = ref false in
   let has_mut_loans = ref false in
   let keep_region (r : T.region) =
     match r with
-    | T.RVar (Free rid) -> T.RegionId.Set.mem rid abs_regions
+    | T.RVar (Free rid) ->
+        sanity_check __FILE__ __LINE__ (rid = Types.RegionId.zero) span;
+        true
     | _ -> false
   in
   let visitor =
@@ -2007,7 +2009,7 @@ let compute_typed_avalue_proj_kind span type_infos
       method! visit_ASymbolic ty pm aproj =
         sanity_check __FILE__ __LINE__ (pm = PNone) span;
         match aproj with
-        | V.AEndedProjLoans (_, _) ->
+        | V.AEndedProjLoans _ ->
             has_loans := true;
             (* We need to check wether the projected loans are mutable or not *)
             if
@@ -2016,7 +2018,7 @@ let compute_typed_avalue_proj_kind span type_infos
             then has_mut_loans := true;
             (* Continue exploring (same reasons as above) *)
             super#visit_ASymbolic ty pm aproj
-        | AProjLoans (_, _, _) ->
+        | AProjLoans _ ->
             (* TODO: we should probably fail here *)
             has_loans := true;
             (* Continue exploring (same reasons as above) *)
@@ -2030,7 +2032,7 @@ let compute_typed_avalue_proj_kind span type_infos
             then has_mut_borrows := true;
             (* Continue exploring (same reasons as above) *)
             super#visit_ASymbolic ty pm aproj
-        | AProjBorrows (_, _, _) ->
+        | AProjBorrows _ ->
             (* TODO: we should probably fail here *)
             has_borrows := true;
             (* Continue exploring (same reasons as above) *)
@@ -2065,14 +2067,12 @@ let compute_typed_avalue_proj_kind span type_infos
                                   ^^
     ]} *)
 let rec typed_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
-    (ectx : C.eval_ctx) (abs_regions : T.RegionId.Set.t) (av : V.typed_avalue) :
-    texpression option =
+    (ectx : C.eval_ctx) (av : V.typed_avalue) : texpression option =
   let value =
     match av.value with
-    | AAdt adt_v ->
-        adt_avalue_to_consumed_aux ~filter ctx ectx abs_regions av adt_v
+    | AAdt adt_v -> adt_avalue_to_consumed_aux ~filter ctx ectx av adt_v
     | ABottom -> craise __FILE__ __LINE__ ctx.span "Unreachable"
-    | ALoan lc -> aloan_content_to_consumed_aux ~filter ctx ectx abs_regions lc
+    | ALoan lc -> aloan_content_to_consumed_aux ~filter ctx ectx lc
     | ABorrow _ ->
         (* This value should have been generated by a loan projector: there
            can't be aborrows unless there are nested borrows, which are not
@@ -2080,7 +2080,7 @@ let rec typed_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
         craise __FILE__ __LINE__ ctx.span "Unreachable"
     | ASymbolic (pm, aproj) ->
         sanity_check __FILE__ __LINE__ (pm = PNone) ctx.span;
-        aproj_to_consumed_aux ctx abs_regions aproj av.ty
+        aproj_to_consumed_aux ctx aproj av.ty
     | AIgnored mv -> (
         if filter then None
         else
@@ -2102,16 +2102,13 @@ let rec typed_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
   value
 
 and adt_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
-    (ectx : C.eval_ctx) (abs_regions : T.RegionId.Set.t) (av : V.typed_avalue)
-    (adt_v : V.adt_avalue) : texpression option =
+    (ectx : C.eval_ctx) (av : V.typed_avalue) (adt_v : V.adt_avalue) :
+    texpression option =
   (* We do not do the same thing depending on whether we visit a tuple
      or a "regular" ADT *)
   let adt_id, _ = TypesUtils.ty_as_adt av.ty in
   (* Check if the ADT contains borrows *)
-  match
-    compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos abs_regions
-      av
-  with
+  match compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos av with
   | BorrowProj _ -> craise __FILE__ __LINE__ ctx.span "Unreachable"
   | UnknownProj ->
       (* If we filter: ignore the value.
@@ -2120,7 +2117,7 @@ and adt_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
       else
         let fields =
           List.map
-            (typed_avalue_to_consumed_aux ~filter ctx ectx abs_regions)
+            (typed_avalue_to_consumed_aux ~filter ctx ectx)
             adt_v.field_values
         in
         let fields = List.map Option.get fields in
@@ -2144,7 +2141,7 @@ and adt_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
           | TBuiltin _ | TAdtId _ -> borrow_kind = BShared
         in
         List.map
-          (typed_avalue_to_consumed_aux ~filter ctx ectx abs_regions)
+          (typed_avalue_to_consumed_aux ~filter ctx ectx)
           adt_v.field_values
       in
       match adt_id with
@@ -2188,8 +2185,7 @@ and adt_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
     end
 
 and aloan_content_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
-    (ectx : C.eval_ctx) (_abs_regions : T.RegionId.Set.t) (lc : V.aloan_content)
-    : texpression option =
+    (ectx : C.eval_ctx) (lc : V.aloan_content) : texpression option =
   match lc with
   | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) ->
       craise __FILE__ __LINE__ ctx.span "Unreachable"
@@ -2221,17 +2217,18 @@ and aloan_content_to_consumed_aux ~(filter : bool) (ctx : bs_ctx)
       (* This case only happens with nested borrows *)
       craise __FILE__ __LINE__ ctx.span "Unimplemented"
 
-and aproj_to_consumed_aux (ctx : bs_ctx) (_abs_regions : T.RegionId.Set.t)
-    (aproj : V.aproj) (ty : T.ty) : texpression option =
+and aproj_to_consumed_aux (ctx : bs_ctx) (aproj : V.aproj) (ty : T.ty) :
+    texpression option =
   match aproj with
-  | V.AEndedProjLoans (msv, []) ->
+  | V.AEndedProjLoans { proj = msv; consumed = []; borrows = [] } ->
       (* The symbolic value was left unchanged.
 
          We're using the projection type as the type of the symbolic value -
          it doesn't really matter. *)
       let msv : V.symbolic_value = { sv_id = msv; sv_ty = ty } in
       Some (symbolic_value_to_texpression ctx msv)
-  | V.AEndedProjLoans (_msv, [ (mnv, child_aproj) ]) ->
+  | V.AEndedProjLoans
+      { proj = _; consumed = [ (mnv, child_aproj) ]; borrows = [] } ->
       sanity_check __FILE__ __LINE__ (child_aproj = AEmpty) ctx.span;
       (* TODO: check that the updated symbolic values covers all the cases
          (part of the symbolic value might have been updated, and the rest
@@ -2249,9 +2246,9 @@ and aproj_to_consumed_aux (ctx : bs_ctx) (_abs_regions : T.RegionId.Set.t)
 
          We're using the projection type as the type of the symbolic value -
          it doesn't really matter. *)
-      let mnv : V.symbolic_value = { sv_id = mnv; sv_ty = ty } in
+      let mnv : V.symbolic_value = { sv_id = mnv.sv_id; sv_ty = ty } in
       Some (symbolic_value_to_texpression ctx mnv)
-  | V.AEndedProjLoans (_, _) ->
+  | V.AEndedProjLoans _ ->
       (* The symbolic value was updated, and the given back values come from several
          abstractions *)
       craise __FILE__ __LINE__ ctx.span "Unimplemented"
@@ -2259,12 +2256,11 @@ and aproj_to_consumed_aux (ctx : bs_ctx) (_abs_regions : T.RegionId.Set.t)
       (* The value should have been introduced by a loan projector, and should not
          contain nested borrows, so we can't get there *)
       craise __FILE__ __LINE__ ctx.span "Unreachable"
-  | AEmpty | AProjLoans (_, _, _) | AProjBorrows (_, _, _) ->
+  | AEmpty | AProjLoans _ | AProjBorrows _ ->
       craise __FILE__ __LINE__ ctx.span "Unreachable"
 
 let typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
-    (abs_regions : T.RegionId.Set.t) (av : V.typed_avalue) : texpression option
-    =
+    (av : V.typed_avalue) : texpression option =
   (* Check if the value was generated from a loan projector: if yes, and if
      it contains mutable loans, then we generate a consumed value (because
      upon ending the borrow we consumed a value).
@@ -2273,15 +2269,12 @@ let typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
     (lazy
       ("typed_avalue_to_consumed: "
       ^ typed_avalue_to_string ~with_ended:true ectx av));
-  match
-    compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos abs_regions
-      av
-  with
+  match compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos av with
   | LoanProj BMut ->
       log#ltrace
         (lazy
           "typed_avalue_to_consumed: the value contains mutable loan projectors");
-      typed_avalue_to_consumed_aux ~filter:true ctx ectx abs_regions av
+      typed_avalue_to_consumed_aux ~filter:true ctx ectx av
   | LoanProj BShared | BorrowProj _ | UnknownProj ->
       (* If it is a borrow proj we ignore it. If it is an unknown projection,
          it means the value doesn't contain loans nor borrows, so nothing
@@ -2300,9 +2293,7 @@ let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) :
   log#ltrace
     (lazy ("abs_to_consumed:\n" ^ abs_to_string ~with_ended:true ctx abs));
   let values =
-    List.filter_map
-      (typed_avalue_to_consumed ctx ectx abs.regions.owned)
-      abs.avalues
+    List.filter_map (typed_avalue_to_consumed ctx ectx) abs.avalues
   in
   log#ltrace
     (lazy
@@ -2366,13 +2357,11 @@ type borrow_or_symbolic_id =
       which gave it back. We need this to compute default values (see
       [bs_ctx.mut_borrow_to_consumed]).
     - the pattern *)
-let rec typed_avalue_to_given_back_aux ~(filter : bool)
-    (abs_regions : T.RegionId.Set.t) (mp : mplace option) (av : V.typed_avalue)
-    (ctx : bs_ctx) : bs_ctx * typed_pattern option =
+let rec typed_avalue_to_given_back_aux ~(filter : bool) (mp : mplace option)
+    (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   let (ctx, value) : _ * typed_pattern option =
     match av.value with
-    | AAdt adt_v ->
-        adt_avalue_to_given_back_aux ~filter abs_regions av adt_v ctx
+    | AAdt adt_v -> adt_avalue_to_given_back_aux ~filter av adt_v ctx
     | ABottom -> craise __FILE__ __LINE__ ctx.span "Unreachable"
     | ALoan _ ->
         (* The avalue should have been generated by a borrow projector: this case is unreachable *)
@@ -2398,14 +2387,10 @@ let rec typed_avalue_to_given_back_aux ~(filter : bool)
   (* Return *)
   (ctx, value)
 
-and adt_avalue_to_given_back_aux ~(filter : bool)
-    (abs_regions : T.RegionId.Set.t) (av : V.typed_avalue)
+and adt_avalue_to_given_back_aux ~(filter : bool) (av : V.typed_avalue)
     (adt_v : V.adt_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   (* Check if the ADT contains borrows *)
-  match
-    compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos abs_regions
-      av
-  with
+  match compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos av with
   | LoanProj _ -> craise __FILE__ __LINE__ ctx.span "Unreachable"
   | UnknownProj ->
       (* If we filter: ignore the pattern.
@@ -2434,8 +2419,7 @@ and adt_avalue_to_given_back_aux ~(filter : bool)
           | TBuiltin _ | TAdtId _ -> borrow_kind = BShared
         in
         List.fold_left_map
-          (fun ctx fv ->
-            typed_avalue_to_given_back_aux ~filter abs_regions mp fv ctx)
+          (fun ctx fv -> typed_avalue_to_given_back_aux ~filter mp fv ctx)
           ctx adt_v.field_values
       in
       match adt_id with
@@ -2520,9 +2504,9 @@ and aborrow_content_to_given_back_aux ~(filter : bool) (mp : mplace option)
 and aproj_to_given_back_aux (mp : mplace option) (aproj : V.aproj) (ty : T.ty)
     (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match aproj with
-  | V.AEndedProjLoans (_, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable"
-  | AEndedProjBorrows (mv, given_back) ->
-      cassert __FILE__ __LINE__ (given_back = []) ctx.span "Unreachable";
+  | V.AEndedProjLoans _ -> craise __FILE__ __LINE__ ctx.span "Unreachable"
+  | AEndedProjBorrows { mvalues = mv; loans } ->
+      cassert __FILE__ __LINE__ (loans = []) ctx.span "Unreachable";
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv.given_back ctx in
       let pat = mk_typed_pattern_from_var var mp in
@@ -2540,22 +2524,17 @@ and aproj_to_given_back_aux (mp : mplace option) (aproj : V.aproj) (ty : T.ty)
         }
       in
       (ctx, Some pat)
-  | AEmpty | AProjLoans (_, _, _) | AProjBorrows (_, _, _) ->
+  | AEmpty | AProjLoans _ | AProjBorrows _ ->
       craise __FILE__ __LINE__ ctx.span "Unreachable"
 
-let typed_avalue_to_given_back (abs_regions : T.RegionId.Set.t)
-    (mp : mplace option) (v : V.typed_avalue) (ctx : bs_ctx) :
-    bs_ctx * typed_pattern option =
+let typed_avalue_to_given_back (mp : mplace option) (v : V.typed_avalue)
+    (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   (* Check if the value was generated from a borrow projector: if yes, and if
      it contains mutable borrows we generate a given back pattern (because
      upon ending the borrow the abstraction gave back a value).
      Otherwise we ignore it. *)
-  match
-    compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos abs_regions
-      v
-  with
-  | BorrowProj BMut ->
-      typed_avalue_to_given_back_aux abs_regions mp ~filter:true v ctx
+  match compute_typed_avalue_proj_kind ctx.span ctx.type_ctx.type_infos v with
+  | BorrowProj BMut -> typed_avalue_to_given_back_aux mp ~filter:true v ctx
   | BorrowProj BShared | LoanProj _ | UnknownProj ->
       (* If it is a loan proj we ignore it. If it is an unknown projection,
          it means the value doesn't contain loans nor borrows, so nothing
@@ -2574,8 +2553,7 @@ let abs_to_given_back (mpl : mplace option list option) (abs : V.abs)
   in
   let ctx, values =
     List.fold_left_map
-      (fun ctx (mp, av) ->
-        typed_avalue_to_given_back abs.regions.owned mp av ctx)
+      (fun ctx (mp, av) -> typed_avalue_to_given_back mp av ctx)
       ctx avalues
   in
   let values = List.filter_map (fun x -> x) values in
@@ -4237,7 +4215,7 @@ and translate_forward_end (return_value : (C.eval_ctx * V.typed_value) option)
       (* Translate the input values *)
       let loop_input_values =
         List.map
-          (fun sv ->
+          (fun (sv : Values.symbolic_value) ->
             log#ltrace
               (lazy
                 ("translate_forward_end: looking up input_svl: "
@@ -4437,7 +4415,8 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   (* Translate the loop inputs *)
   let inputs =
     List.map
-      (fun sv -> V.SymbolicValueId.Map.find sv.V.sv_id ctx.sv_to_var)
+      (fun (sv : Values.symbolic_value) ->
+        V.SymbolicValueId.Map.find sv.V.sv_id ctx.sv_to_var)
       loop.input_svalues
   in
   let inputs_lvs =