Start storing meta-values in the avalues, for synthesis purposes

11 files changed, 309 insertions, 244 deletions

diff --git a/TODO.md b/TODO.md
index b7f03ee3..60211c32 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,9 @@
 
 1. stateful maps/sets modules (hashtbl?)
 
+1. Check the occurrence of visitors like visit_AEndedMutLoan: the parameters are
+   sometimes inverted!
+
 0. compute the region constraints for the type definitions
 
 2. set of types with mutable borrows (what to do when type variables appear under
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 6f469044..e64dbe77 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -118,9 +118,9 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
          * need it to properly instantiate the backward functions when generating
          * the pure translation. *)
         match lc with
-        | V.AMutLoan (bid, av) ->
+        | V.AMutLoan (_, _) ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AMutLoan outer bid av)
+            super#visit_ALoan outer lc
         | V.ASharedLoan (bids, v, av) ->
             (* Explore the shared value - we need to update the outer borrows *)
             let souter = update_outer_borrows outer (Borrows bids) in
@@ -129,27 +129,22 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
             let av = super#visit_typed_avalue outer av in
             (* Reconstruct *)
             V.ALoan (V.ASharedLoan (bids, v, av))
-        | V.AEndedMutLoan { given_back; child } ->
-            (* The loan has ended, so no need to update the outer borrows *)
-            V.ALoan (super#visit_AEndedMutLoan outer given_back child)
-        | V.AEndedSharedLoan (v, av) ->
-            (* The loan has ended, so no need to update the outer borrows *)
-            V.ALoan (super#visit_AEndedSharedLoan outer v av)
-        | V.AIgnoredMutLoan (bid, av) ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredMutLoan outer bid av)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child)
-        | V.AIgnoredSharedLoan av ->
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedLoan _
+        (* The loan has ended, so no need to update the outer borrows *)
+        | V.AIgnoredMutLoan _ (* Nothing special to do *)
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        (* Nothing special to do *)
+        | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan outer av)
+            super#visit_ALoan outer lc
       (** We reimplement [visit_ALoan] because we may have to update the
           outer borrows *)
 
       method! visit_ABorrow outer bc =
         match bc with
-        | V.AMutBorrow (bid, av) ->
+        | V.AMutBorrow (_, bid, _) ->
             (* Check if this is the borrow we are looking for *)
             if bid = l then (
               (* When ending a mut borrow, there are two cases:
@@ -166,12 +161,15 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
               (* Register the update *)
               set_replaced_bc (Abstract bc);
               (* Update the value - note that we are necessarily in the second
-               * of the two cases described above *)
+               * of the two cases described above.
+               * Also note that, as we are moving the borrowed value inside the
+               * abstraction (and not really giving the value back to the context)
+               * we do not insert [AEndedMutBorrow] but rather [ABottom] *)
               V.ABottom)
             else
               (* Update the outer borrows before diving into the child avalue *)
               let outer = update_outer_borrows outer (Borrow bid) in
-              V.ABorrow (super#visit_AMutBorrow outer bid av)
+              super#visit_ABorrow outer bc
         | V.ASharedBorrow bid ->
             (* Check if this is the borrow we are looking for *)
             if bid = l then (
@@ -183,15 +181,13 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
               (* Update the value - note that we are necessarily in the second
                * of the two cases described above *)
               V.ABottom)
-            else V.ABorrow (super#visit_ASharedBorrow outer bid)
-        | V.AIgnoredMutBorrow (opt_bid, av) ->
-            (* Nothing special to do *)
-            V.ABorrow (super#visit_AIgnoredMutBorrow outer opt_bid av)
-        | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+            else super#visit_ABorrow outer bc
+        | V.AIgnoredMutBorrow (_, _)
+        | V.AEndedMutBorrow _
+        | V.AEndedIgnoredMutBorrow
+            { given_back_loans_proj = _; child = _; given_back_meta = _ } ->
             (* Nothing special to do *)
-            V.ABorrow
-              (super#visit_AEndedIgnoredMutBorrow outer given_back_loans_proj
-                 child)
+            super#visit_ABorrow outer bc
         | V.AProjSharedBorrow asb ->
             (* Check if the borrow we are looking for is in the asb *)
             if borrow_in_asb l asb then (
@@ -204,9 +200,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
                * of the two cases described above *)
               let asb = remove_borrow_from_asb l asb in
               V.ABorrow (V.AProjSharedBorrow asb))
-            else
-              (* Nothing special to do *)
-              V.ABorrow (super#visit_AProjSharedBorrow outer asb)
+            else (* Nothing special to do *)
+              super#visit_ABorrow outer bc
 
       method! visit_abs outer abs =
         (* Update the outer abs *)
@@ -317,6 +312,8 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               match nv.V.value with
               | V.Symbolic sv ->
                   let abs = Option.get opt_abs in
+                  (* Remember the given back value as a meta-value *)
+                  let given_back_meta = nv in
                   (* The loan projector *)
                   let given_back_loans_proj =
                     mk_aproj_loans_value_from_symbolic_value abs.regions sv
@@ -325,7 +322,8 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                   let child = super#visit_typed_avalue opt_abs child in
                   (* Return *)
                   V.ABorrow
-                    (V.AEndedIgnoredMutBorrow { given_back_loans_proj; child })
+                    (V.AEndedIgnoredMutBorrow
+                       { given_back_loans_proj; child; given_back_meta })
               | _ -> failwith "Unreachable"
             else
               (* Continue exploring *)
@@ -359,6 +357,8 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                * an ended loan *)
               (* Register the insertion *)
               set_replaced ();
+              (* Remember the given back value as a meta-value *)
+              let given_back_meta = nv in
               (* Apply the projection *)
               let given_back =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
@@ -367,23 +367,22 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
               (* Return the new value *)
-              V.ALoan (V.AEndedMutLoan { given_back; child }))
-            else
-              (* Continue exploring *)
-              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
-        | V.ASharedLoan (bids, v, av) ->
+              V.ALoan (V.AEndedMutLoan { child; given_back; given_back_meta }))
+            else (* Continue exploring *)
+              super#visit_ALoan opt_abs lc
+        | V.ASharedLoan (_, _, _) ->
             (* We are giving back a value to a *mutable* loan: nothing special to do *)
-            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
-        | V.AEndedMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
-        | V.AEndedSharedLoan (v, av) ->
+            super#visit_ALoan opt_abs lc
+        | V.AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, _) ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+            super#visit_ALoan opt_abs lc
         | V.AIgnoredMutLoan (bid', child) ->
             (* This loan is ignored, but we may have to project on a subvalue
              * of the value which is given back *)
             if bid' = bid then
+              (* Remember the given back value as a meta-value *)
+              let given_back_meta = nv in
               (* Note that we replace the ignored mut loan by an *ended* ignored
                * mut loan. Also, this is not the loan we are looking for *per se*:
                * we don't register the fact that we inserted the value somewhere
@@ -394,14 +393,14 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
-              V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
-            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
+              V.ALoan
+                (V.AEndedIgnoredMutLoan { given_back; child; given_back_meta })
+            else super#visit_ALoan opt_abs lc
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
-        | V.AIgnoredSharedLoan av ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
+            super#visit_ALoan opt_abs lc
       (** We are not specializing an already existing method, but adding a
           new method (for projections, we need type information) *)
 
@@ -432,6 +431,9 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
 let give_back_symbolic_value (_config : C.config)
     (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value)
     (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Store the given-back value as a meta-value for synthesis purposes *)
+  let mv = mk_typed_value_from_symbolic_value nsv in
+  (* Substitution function, to replace the borrow projectors over symbolic values *)
   let subst (_abs : V.abs) _abs_proj_ty =
     (* Compute the projection over the given back value *)
     let child_proj =
@@ -466,7 +468,7 @@ let give_back_symbolic_value (_config : C.config)
             None
         | _ -> failwith "Unreachable")
     in
-    V.AEndedProjLoans child_proj
+    V.AEndedProjLoans (mv, child_proj)
   in
   update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
 
@@ -484,8 +486,8 @@ let give_back_symbolic_value (_config : C.config)
     to convert the [avalue] to a [value] by introducing the proper symbolic values.
  *)
 let give_back_avalue_to_same_abstraction (_config : C.config)
-    (bid : V.BorrowId.id) (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx
-    =
+    (bid : V.BorrowId.id) (mv : V.mvalue) (nv : V.typed_avalue)
+    (ctx : C.eval_ctx) : C.eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -530,19 +532,17 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
               (* Register the insertion *)
               set_replaced ();
               (* Return the new value *)
-              V.ALoan (V.AEndedMutLoan { given_back = nv; child }))
-            else
-              (* Continue exploring *)
-              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
-        | V.ASharedLoan (bids, v, av) ->
-            (* We are giving back a value to a *mutable* loan: nothing special to do *)
-            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
-        | V.AEndedMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
-        | V.AEndedSharedLoan (v, av) ->
+              V.ALoan
+                (V.AEndedMutLoan
+                   { given_back = nv; child; given_back_meta = mv }))
+            else (* Continue exploring *)
+              super#visit_ALoan opt_abs lc
+        | V.ASharedLoan (_, _, _)
+        (* We are giving back a value to a *mutable* loan: nothing special to do *)
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, _) ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+            super#visit_ALoan opt_abs lc
         | V.AIgnoredMutLoan (bid', child) ->
             (* This loan is ignored, but we may have to project on a subvalue
              * of the value which is given back *)
@@ -553,14 +553,15 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
                * (i.e., we don't call [set_replaced]) *)
               (* Sanity check *)
               assert (nv.V.ty = ty);
-              V.ALoan (V.AEndedIgnoredMutLoan { given_back = nv; child }))
-            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
-        | V.AIgnoredSharedLoan av ->
+              V.ALoan
+                (V.AEndedIgnoredMutLoan
+                   { given_back = nv; child; given_back_meta = mv }))
+            else super#visit_ALoan opt_abs lc
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
+            super#visit_ALoan opt_abs lc
       (** We are not specializing an already existing method, but adding a
           new method (for projections, we need type information) *)
     end
@@ -634,22 +635,19 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
                      (V.BorrowId.Set.remove bid bids, shared_value, child)))
             else
               (* Not the loan we are looking for: continue exploring *)
-              V.ALoan (super#visit_ASharedLoan opt_abs bids shared_value child)
-        | V.AEndedMutLoan { given_back; child } ->
-            (* Nothing special to do (the loan has ended) *)
-            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
-        | V.AEndedSharedLoan (v, av) ->
-            (* Nothing special to do (the loan has ended) *)
-            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
-        | V.AIgnoredMutLoan (bid, av) ->
-            (* Nothing special to do (we are giving back a *shared* borrow) *)
-            V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid av)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
-        | V.AIgnoredSharedLoan av ->
+              super#visit_ALoan opt_abs lc
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        (* Nothing special to do (the loan has ended) *)
+        | V.AEndedSharedLoan (_, _)
+        (* Nothing special to do (the loan has ended) *)
+        | V.AIgnoredMutLoan (_, _)
+        (* Nothing special to do (we are giving back a *shared* borrow) *)
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        (* Nothing special to do *)
+        | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
+            super#visit_ALoan opt_abs lc
     end
   in
 
@@ -736,13 +734,13 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
       (* Update the context *)
       give_back_shared config l ctx
-  | Abstract (V.AMutBorrow (l', av)) ->
+  | Abstract (V.AMutBorrow (mv, l', av)) ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
       (* Update the context *)
-      give_back_avalue_to_same_abstraction config l av ctx
+      give_back_avalue_to_same_abstraction config l mv av ctx
   | Abstract (V.ASharedBorrow l') ->
       (* Sanity check *)
       assert (l' = l);
@@ -755,7 +753,9 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (borrow_in_asb l asb);
       (* Update the context *)
       give_back_shared config l ctx
-  | Abstract (V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _) ->
+  | Abstract
+      (V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _)
+    ->
       failwith "Unreachable"
 
 (** Convert an [avalue] to a [value].
@@ -1017,21 +1017,22 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
         match lc with
         | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
         | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
-        | V.AEndedMutLoan { given_back; child } ->
-            super#visit_AEndedMutLoan env given_back child
-        | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av
-        | V.AIgnoredMutLoan (bid, av) ->
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, _) ->
+            super#visit_aloan_content env lc
+        | V.AIgnoredMutLoan (_, _) ->
             (* Note that this loan can't come from a parent abstraction, because
              * we should have ended them already) *)
-            super#visit_AIgnoredMutLoan env bid av
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            super#visit_AEndedIgnoredMutLoan env given_back child
-        | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
+            super#visit_aloan_content env lc
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan _ ->
+            super#visit_aloan_content env lc
 
       method! visit_aproj env sproj =
         (match sproj with
         | V.AProjBorrows (_, _)
-        | V.AEndedProjLoans _ | V.AEndedProjBorrows | V.AIgnoredProjBorrows ->
+        | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
             ()
         | V.AProjLoans sv -> raise (FoundSymbolicValue sv));
         super#visit_aproj env sproj
@@ -1062,28 +1063,11 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
   (* Note that the abstraction mustn't contain any loans *)
   (* We end the borrows, starting with the *inner* ones. This is important
      when considering nested borrows which have the same lifetime.
-     TODO: is that really important?
-
-     For instance:
-     ```
-     x -> mut_loan l1
-     px -> mut_loan l0
-     abs0 { a_mut_borrow l0 (a_mut_borrow l1 (U32 3)) }
-     ```
-
-     becomes (`U32 3` doesn't contain ⊥, so we give back a symbolic value):
-     ```
-     x -> @s0
-     px -> mut_loan l0
-     abs0 { a_mut_borrow l0 ⊥ }
-     ```
-
-     then (the borrowed value contains ⊥, we give back ⊥):
-     ```
-     x -> @s0
-     px -> ⊥
-     abs0 { ⊥ }
-     ```
+     TODO: is that really important? Initially, there was a concern about
+     whether we should give back ⊥ or not, but everything is handled by
+     the symbolic value expansion... Also, now we use the AEndedMutBorrow
+     values to store the children avalues (which was not the case before - we
+     initially replaced the ended mut borrows with ⊥).
   *)
   (* We explore in-depth and use exceptions. When exploring a borrow, if
    * the exploration didn't trigger an exception, it means there are no
@@ -1099,7 +1083,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
         (* No exception was raise: we can raise an exception for the
          * current borrow *)
         match bc with
-        | V.AMutBorrow (_, _) | V.ASharedBorrow _ ->
+        | V.AMutBorrow (_, _, _) | V.ASharedBorrow _ ->
             (* Raise an exception *)
             raise (FoundABorrowContent bc)
         | V.AProjSharedBorrow asb ->
@@ -1110,7 +1094,8 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
                 asb
             then raise (FoundABorrowContent bc)
             else ()
-        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+        | V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _
+        | V.AEndedIgnoredMutBorrow _ ->
             (* Nothing to do for ignored borrows *)
             ()
 
@@ -1119,7 +1104,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
         | V.AProjLoans _ -> failwith "Unexpected"
         | V.AProjBorrows (sv, proj_ty) ->
             raise (FoundAProjBorrows (sv, proj_ty))
-        | V.AEndedProjLoans _ | V.AEndedProjBorrows | V.AIgnoredProjBorrows ->
+        | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
             ());
         super#visit_aproj env sproj
     end
@@ -1134,49 +1119,64 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
   with
   (* There are concrete borrows: end them, then reexplore *)
   | FoundABorrowContent bc ->
-      (* First, replace the borrow by ⊥ *)
-      let bid =
-        match bc with
-        | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
-        | V.AProjSharedBorrow asb -> (
-            (* There should be at least one borrow identifier in the set, which we
-             * can use to identify the whole set *)
-            match
-              List.find
-                (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
-                asb
-            with
-            | V.AsbBorrow bid -> bid
-            | _ -> failwith "Unexpected")
-        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
-            failwith "Unexpected"
-      in
-      let ctx = update_aborrow ek_all bid V.ABottom ctx in
-      (* Then give back the value *)
       let ctx =
         match bc with
-        | V.AMutBorrow (bid, av) ->
+        | V.AMutBorrow (_, bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
             let v = convert_avalue_to_given_back_value av in
+            (* Replace the mut borrow to register the fact that we ended
+             * it and store with it the freshly generated given back value *)
+            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (v, av)) in
+            let ctx = update_aborrow ek_all bid ended_borrow ctx in
+            (* Give the value back *)
             give_back_value config bid v ctx
-        | V.ASharedBorrow bid -> give_back_shared config bid ctx
-        | V.AProjSharedBorrow _ ->
-            (* Nothing to do *)
+        | V.ASharedBorrow bid ->
+            (* Replace the shared borrow with bottom *)
+            let ctx = update_aborrow ek_all bid V.ABottom ctx in
+            (* Give back *)
+            give_back_shared config bid ctx
+        | V.AProjSharedBorrow asb ->
+            (* Retrieve the borrow ids *)
+            let bids =
+              List.filter_map
+                (fun asb ->
+                  match asb with
+                  | V.AsbBorrow bid -> Some bid
+                  | V.AsbProjReborrows (_, _) -> None)
+                asb
+            in
+            (* There should be at least one borrow identifier in the set, which we
+             * can use to identify the whole set *)
+            let repr_bid = List.hd bids in
+            (* Replace the shared borrow with Bottom *)
+            let ctx = update_aborrow ek_all repr_bid V.ABottom ctx in
+            (* Give back the shared borrows *)
+            let ctx =
+              List.fold_left
+                (fun ctx bid -> give_back_shared config bid ctx)
+                ctx bids
+            in
+            (* Continue *)
             ctx
-        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+        | V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _
+        | V.AEndedIgnoredMutBorrow _ ->
             failwith "Unexpected"
       in
       (* Reexplore *)
       end_abstraction_borrows config chain abs_id ctx
   (* There are symbolic borrows: end them, then reexplore *)
   | FoundAProjBorrows (sv, proj_ty) ->
+      (* Generate a fresh symbolic value *)
+      let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
+      let ended_borrow =
+        V.AEndedProjBorrows (mk_typed_value_from_symbolic_value nsv)
+      in
       let ctx =
-        update_intersecting_aproj_borrows_non_shared abs.regions sv
-          V.AEndedProjBorrows ctx
+        update_intersecting_aproj_borrows_non_shared abs.regions sv ended_borrow
+          ctx
       in
-      (* Give back a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
+      (* Give back the symbolic value *)
       let ctx =
         give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
       in
@@ -1257,14 +1257,17 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
        * end it directly, otherwise we need to end the abstraction where it
        * came from first *)
       if abs_id' = abs_id then
+        (* As the symbolic value was left unchanged, we give it back *)
+        let given_back_sv = sv in
         (* Replace the proj_borrows *)
-        let npb = V.AEndedProjBorrows in
+        let given_back = mk_typed_value_from_symbolic_value given_back_sv in
+        let npb = V.AEndedProjBorrows given_back in
         let ctx =
           update_intersecting_aproj_borrows_non_shared regions sv npb ctx
         in
         (* Replace the proj_loans - note that the loaned (symbolic) value
          * was left unchanged *)
-        give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx
+        give_back_symbolic_value config regions sv.V.sv_ty sv given_back_sv ctx
       else
         (* End the abstraction.
          * Don't retry ending the current proj_loans after ending the abstraction:
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 8f6827b3..d2f8e3e3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -186,13 +186,13 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
             if V.BorrowId.Set.mem l bids then
               raise (FoundGLoanContent (Abstract lc))
             else super#visit_ASharedLoan env bids v av
-        | V.AEndedMutLoan { given_back; child } ->
-            super#visit_AEndedMutLoan env given_back child
-        | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av
-        | V.AIgnoredMutLoan (bid, av) -> super#visit_AIgnoredMutLoan env bid av
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            super#visit_AEndedIgnoredMutLoan env given_back child
-        | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, _)
+        | V.AIgnoredMutLoan (_, _)
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan _ ->
+            super#visit_aloan_content env lc
       (** Note that we don't control diving inside the abstractions: if we
           allow to dive inside abstractions, we allow to go anywhere
           (because there are no use cases requiring finer control) *)
@@ -326,13 +326,13 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id)
         | V.ASharedLoan (bids, v, av) ->
             if V.BorrowId.Set.mem l bids then update ()
             else super#visit_ASharedLoan env bids v av
-        | V.AEndedMutLoan { given_back; child } ->
-            super#visit_AEndedMutLoan env given_back child
-        | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av
-        | V.AIgnoredMutLoan (bid, av) -> super#visit_AIgnoredMutLoan env bid av
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            super#visit_AEndedIgnoredMutLoan env given_back child
-        | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, _)
+        | V.AIgnoredMutLoan (_, _)
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan _ ->
+            super#visit_aloan_content env lc
 
       method! visit_abs env abs =
         if ek.enter_abs then super#visit_abs env abs else abs
@@ -378,16 +378,17 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_aborrow_content env bc =
         match bc with
-        | V.AMutBorrow (bid, av) ->
+        | V.AMutBorrow (mv, bid, av) ->
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
-            else super#visit_AMutBorrow env bid av
+            else super#visit_AMutBorrow env mv bid av
         | V.ASharedBorrow bid ->
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
             else super#visit_ASharedBorrow env bid
-        | V.AIgnoredMutBorrow (opt_bid, av) ->
-            super#visit_AIgnoredMutBorrow env opt_bid av
-        | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
-            super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj child
+        | V.AIgnoredMutBorrow (_, _)
+        | V.AEndedMutBorrow _
+        | V.AEndedIgnoredMutBorrow
+            { given_back_loans_proj = _; child = _; given_back_meta = _ } ->
+            super#visit_aborrow_content env bc
         | V.AProjSharedBorrow asb ->
             if borrow_in_asb l asb then
               raise (FoundGBorrowContent (Abstract bc))
@@ -494,18 +495,15 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue)
 
       method! visit_ABorrow env bc =
         match bc with
-        | V.AMutBorrow (bid, av) ->
+        | V.AMutBorrow (mv, bid, av) ->
             if bid = l then update ()
-            else V.ABorrow (super#visit_AMutBorrow env bid av)
+            else V.ABorrow (super#visit_AMutBorrow env mv bid av)
         | V.ASharedBorrow bid ->
             if bid = l then update ()
             else V.ABorrow (super#visit_ASharedBorrow env bid)
-        | V.AIgnoredMutBorrow (opt_bid, av) ->
-            V.ABorrow (super#visit_AIgnoredMutBorrow env opt_bid av)
-        | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
-            V.ABorrow
-              (super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj
-                 child)
+        | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
+        | V.AEndedIgnoredMutBorrow _ ->
+            super#visit_ABorrow env bc
         | V.AProjSharedBorrow asb ->
             if borrow_in_asb l asb then update ()
             else V.ABorrow (super#visit_AProjSharedBorrow env asb)
@@ -671,7 +669,7 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
       method! visit_aproj abs sproj =
         (let abs = Option.get abs in
          match sproj with
-         | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows
+         | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _
          | AIgnoredProjBorrows ->
              ()
          | AProjBorrows (sv', proj_rty) ->
@@ -760,7 +758,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool)
 
       method! visit_aproj abs sproj =
         match sproj with
-        | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows
+        | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _
         | AIgnoredProjBorrows ->
             super#visit_aproj abs sproj
         | AProjBorrows (sv', proj_rty) ->
@@ -853,7 +851,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
 
       method! visit_aproj abs sproj =
         match sproj with
-        | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows
+        | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _
         | AIgnoredProjBorrows ->
             super#visit_aproj abs sproj
         | AProjLoans sv' ->
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 0842dee7..5d2d4f6f 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -75,7 +75,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
         (match aproj with
         | AProjLoans sv | AProjBorrows (sv, _) ->
             assert (not (same_symbolic_id sv original_sv))
-        | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ());
+        | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
       (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called
           only on child projections (i.e., projections which appear in [AEndedProjLoans]).
@@ -90,9 +90,9 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
         (* 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
-        | V.AEndedProjLoans None, _ | V.AEndedProjBorrows, _ ->
+        | V.AEndedProjLoans (_, None), _ | V.AEndedProjBorrows _, _ ->
             V.ASymbolic aproj
-        | V.AEndedProjLoans (Some child_proj), _ ->
+        | V.AEndedProjLoans (_, Some child_proj), _ ->
             (* Explore the child projection to make sure we don't have to expand
              * anything in there *)
             V.ASymbolic (self#visit_aproj (Some current_abs) child_proj)
@@ -329,7 +329,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
         (match aproj with
         | AProjLoans sv | AProjBorrows (sv, _) ->
             assert (not (same_symbolic_id sv original_sv))
-        | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ());
+        | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
       (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called
           only on child projections (i.e., projections which appear in [AEndedProjLoans]).
@@ -339,7 +339,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
 
       method! visit_ASymbolic proj_regions aproj =
         match aproj with
-        | AEndedProjBorrows | AIgnoredProjBorrows ->
+        | AEndedProjBorrows _ | AIgnoredProjBorrows ->
             (* We ignore borrows *) V.ASymbolic aproj
         | AProjLoans _ ->
             (* Loans are handled later *)
@@ -349,8 +349,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
             match reborrow_ashared (Option.get proj_regions) sv proj_ty with
             | None -> super#visit_ASymbolic proj_regions aproj
             | Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
-        | AEndedProjLoans None -> V.ASymbolic aproj
-        | AEndedProjLoans (Some child_aproj) ->
+        | AEndedProjLoans (_, None) -> V.ASymbolic aproj
+        | AEndedProjLoans (_, Some child_aproj) ->
             (* Sanity check: make sure there is nothing to expand inside children
              * projections *)
             V.ASymbolic (self#visit_aproj proj_regions child_aproj)
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index c0d1c528..431a2076 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -182,10 +182,12 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                 | ( _,
                     Abstract
                       ( V.AMutLoan (_, _)
-                      | V.AEndedMutLoan { given_back = _; child = _ }
+                      | V.AEndedMutLoan
+                          { given_back = _; child = _; given_back_meta = _ }
                       | V.AEndedSharedLoan (_, _)
                       | V.AIgnoredMutLoan (_, _)
-                      | V.AEndedIgnoredMutLoan { given_back = _; child = _ }
+                      | V.AEndedIgnoredMutLoan
+                          { given_back = _; child = _; given_back_meta = _ }
                       | V.AIgnoredSharedLoan _ ) ) ->
                     failwith "Expected a shared (abstraction) loan"
                 | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> (
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 7c648563..982d9460 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -171,12 +171,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
             let bc =
               match (bc, kind) with
               | V.MutBorrow (bid, bv), T.Mut ->
+                  (* Remember the borrowed value we are about to project as a meta-value *)
+                  let mv = bv in
                   (* Apply the projection on the borrowed value *)
                   let bv =
                     apply_proj_borrows check_symbolic_no_ended ctx
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
-                  V.AMutBorrow (bid, bv)
+                  V.AMutBorrow (mv, bid, bv)
               | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
               | V.InactivatedMutBorrow _, _ ->
                   failwith
@@ -480,10 +482,11 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
             super#visit_ASharedLoan env bids sv av
         | V.AIgnoredSharedLoan _
         | V.AMutLoan (_, _)
-        | V.AEndedMutLoan { given_back = _; child = _ }
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
         | V.AEndedSharedLoan (_, _)
         | V.AIgnoredMutLoan (_, _)
-        | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ } ->
             (* Nothing particular to do *)
             super#visit_aloan_content env lc
     end
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index c3fe9781..761c2fbd 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -171,7 +171,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
         (match aproj with
         | AProjLoans sv | AProjBorrows (sv, _) ->
             if sv.V.sv_id = sv_id then raise Found else ()
-        | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ());
+        | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj env aproj
 
       method! visit_abstract_shared_borrows _ asb =
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 67084684..33e7d90b 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -160,9 +160,10 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
           | V.AIgnoredMutLoan (bid, _) -> register_ignored_loan T.Mut bid
           | V.AIgnoredSharedLoan _
-          | V.AEndedMutLoan { given_back = _; child = _ }
+          | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
           | V.AEndedSharedLoan (_, _)
-          | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
+          | V.AEndedIgnoredMutLoan
+              { given_back = _; child = _; given_back_meta = _ } ->
               (* Do nothing *)
               ()
         in
@@ -250,11 +251,12 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
       method! visit_aborrow_content env bc =
         let _ =
           match bc with
-          | V.AMutBorrow (bid, _) -> register_borrow Mut bid
+          | V.AMutBorrow (_, bid, _) -> register_borrow Mut bid
           | V.ASharedBorrow bid -> register_borrow Shared bid
           | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
           | V.AIgnoredMutBorrow (None, _)
-          | V.AEndedIgnoredMutBorrow _ | V.AProjSharedBorrow _ ->
+          | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _
+          | V.AProjSharedBorrow _ ->
               (* Do nothing *)
               ()
         in
@@ -340,10 +342,13 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
           match lc with
           | V.AMutLoan (_, _) -> set_outer_mut info
           | V.ASharedLoan (_, _, _) -> set_outer_shared info
-          | V.AEndedMutLoan { given_back = _; child = _ } -> set_outer_mut info
+          | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+            ->
+              set_outer_mut info
           | V.AEndedSharedLoan (_, _) -> set_outer_shared info
           | V.AIgnoredMutLoan (_, _) -> set_outer_mut info
-          | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
+          | V.AEndedIgnoredMutLoan
+              { given_back = _; child = _; given_back_meta = _ } ->
               set_outer_mut info
           | V.AIgnoredSharedLoan _ -> set_outer_shared info
         in
@@ -354,9 +359,10 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         (* Update the info *)
         let info =
           match bc with
-          | V.AMutBorrow (_, _) -> set_outer_mut info
+          | V.AMutBorrow (_, _, _) -> set_outer_mut info
           | V.ASharedBorrow _ -> set_outer_shared info
-          | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+          | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
+          | V.AEndedIgnoredMutBorrow _ ->
               set_outer_mut info
           | V.AProjSharedBorrow _ -> set_outer_shared info
         in
@@ -466,7 +472,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 let glc = lookup_borrow ek_all bid ctx in
                 match glc with
                 | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
-                | Abstract (V.AMutBorrow (_, sv)) ->
+                | Abstract (V.AMutBorrow (_, _, sv)) ->
                     assert (Subst.erase_regions sv.V.ty = ty)
                 | _ -> failwith "Inconsistent context"))
         | V.Symbolic sv, ty ->
@@ -535,7 +541,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.ABottom, _ -> (* Nothing to check *) ()
         | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | V.AMutBorrow (_, av), T.Mut ->
+            | V.AMutBorrow (_, _, av), T.Mut ->
                 (* Check that the child value has the proper type *)
                 assert (av.V.ty = ref_ty)
             | V.ASharedBorrow bid, T.Shared -> (
@@ -548,8 +554,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 | _ -> failwith "Inconsistent context")
             | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
                 assert (av.V.ty = ref_ty)
-            | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child }, T.Mut
-              ->
+            | ( V.AEndedIgnoredMutBorrow
+                  { given_back_loans_proj; child; given_back_meta = _ },
+                T.Mut ) ->
                 assert (given_back_loans_proj.V.ty = ref_ty);
                 assert (child.V.ty = ref_ty)
             | V.AProjSharedBorrow _, T.Shared -> ()
@@ -565,7 +572,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 match glc with
                 | Concrete (V.MutBorrow (_, bv)) ->
                     assert (bv.V.ty = Subst.erase_regions borrowed_aty)
-                | Abstract (V.AMutBorrow (_, sv)) ->
+                | Abstract (V.AMutBorrow (_, _, sv)) ->
                     assert (
                       Subst.erase_regions sv.V.ty
                       = Subst.erase_regions borrowed_aty)
@@ -576,8 +583,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 assert (sv.V.ty = Subst.erase_regions borrowed_aty);
                 (* TODO: the type of aloans doesn't make sense, see above *)
                 assert (child_av.V.ty = borrowed_aty)
-            | V.AEndedMutLoan { given_back; child }
-            | V.AEndedIgnoredMutLoan { given_back; child } ->
+            | V.AEndedMutLoan { given_back; child; given_back_meta = _ }
+            | V.AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ }
+              ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
                 assert (given_back.V.ty = borrowed_aty);
                 assert (child.V.ty = borrowed_aty)
@@ -593,13 +601,13 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                  * otherwise they should have been reduced to `_` *)
                 let abs = Option.get info in
                 assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
-            | V.AEndedProjLoans (Some proj) -> (
+            | V.AEndedProjLoans (_, Some proj) -> (
                 match proj with
                 | V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
-                | V.AEndedProjBorrows -> ()
+                | V.AEndedProjBorrows _ -> ()
                 | _ -> failwith "Unexpected")
-            | V.AEndedProjLoans None
-            | V.AEndedProjBorrows | V.AIgnoredProjBorrows ->
+            | V.AEndedProjLoans (_, None)
+            | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
                 ())
         | V.AIgnored, _ -> ()
         | _ -> failwith "Erroneous typing");
@@ -694,7 +702,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
          | AProjLoans sv -> add_aproj_loans sv abs.abs_id abs.regions
          | AProjBorrows (sv, proj_ty) ->
              add_aproj_borrows sv abs.abs_id abs.regions proj_ty false
-         | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ());
+         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj abs aproj
     end
   in
diff --git a/src/Print.ml b/src/Print.ml
index 94546675..6c39366c 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -313,11 +313,11 @@ module Values = struct
         "[" ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv ^ "]"
     | AProjBorrows (sv, rty) ->
         "(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
-    | AEndedProjLoans aproj_opt -> (
+    | AEndedProjLoans (_mv, aproj_opt) -> (
         match aproj_opt with
         | None -> "_"
         | Some aproj -> aproj_to_string fmt aproj)
-    | AEndedProjBorrows -> "_"
+    | AEndedProjBorrows _mv -> "_"
     | AIgnoredProjBorrows -> "_"
 
   let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
@@ -409,7 +409,7 @@ module Values = struct
   and aborrow_content_to_string (fmt : value_formatter) (bc : V.aborrow_content)
       : string =
     match bc with
-    | AMutBorrow (bid, av) ->
+    | AMutBorrow (_, bid, av) ->
         "&mut@" ^ V.BorrowId.to_string bid ^ " ("
         ^ typed_avalue_to_string fmt av
         ^ ")"
@@ -420,7 +420,10 @@ module Values = struct
         ^ ", "
         ^ typed_avalue_to_string fmt av
         ^ ")"
-    | AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+    | AEndedMutBorrow (_mv, child) ->
+        "@ended_mut_borrow(" ^ typed_avalue_to_string fmt child ^ ")"
+    | AEndedIgnoredMutBorrow
+        { child; given_back_loans_proj; given_back_meta = _ } ->
         "@ended_ignored_mut_borrow{ "
         ^ typed_avalue_to_string fmt child
         ^ "; "
diff --git a/src/Values.ml b/src/Values.ml
index 6386f8db..8e6bda43 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -185,6 +185,14 @@ and typed_value = { value : value; ty : ety }
       }]
 (** "Regular" typed value (we map variables to typed values) *)
 
+type mvalue = typed_value [@@deriving show]
+(** "Meta"-value: information we store for the synthesis.
+
+     Note that we never automatically visit the meta-values with the
+     visitors: they really are meta information, and shouldn't be considered
+     as part of the environment during a symbolic execution.
+ *)
+
 (** When giving shared borrows to functions (i.e., inserting shared borrows inside
     abstractions) we need to reborrow the shared values. When doing so, we lookup
     the shared values and apply some special projections to the shared value
@@ -213,6 +221,8 @@ class ['self] iter_aproj_base =
     inherit [_] iter_typed_value
 
     method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
+
+    method visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for [aproj] map visitor *)
@@ -221,6 +231,8 @@ class ['self] map_aproj_base =
     inherit [_] map_typed_value
 
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
+
+    method visit_mvalue : 'env -> mvalue -> mvalue = fun _ v -> v
   end
 
 type aproj =
@@ -228,18 +240,22 @@ type aproj =
   | AProjBorrows of symbolic_value * rty
       (** 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]. *)
-  | AEndedProjLoans of aproj option
+  | AEndedProjLoans of mvalue * aproj option
       (** When ending a proj_loans over a symbolic value, we may need to insert
           (and keep track of) a proj_borrows over the given back value, if the
           symbolic value was consumed by an abstraction then updated.
           
-          Rk.: for now this is useless, because we forbid borrow overwrites on
+          Rk.: for now the option is useless, because we forbid borrow overwrites on
           returned values. A consequence is that when a proj_loans over a symbolic
           value ends, we don't project the given back value.
+          
+          The meta-value is the value which was given back (and thus consumed by
+          the loan when it ended).
+       *)
+  | AEndedProjBorrows of mvalue
+      (** The only purpose of [AEndedProjBorrows] is to store the (symbolic) value
+          which was generated upon ending the borrow (this is useful for synthesis)
        *)
-  | AEndedProjBorrows
-  (* TODO: remove AEndedProjBorrows? We might need it for synthesis, to contain
-   * meta values *)
   | AIgnoredProjBorrows
 [@@deriving
   show,
@@ -369,11 +385,19 @@ and aloan_content =
           px -> shared_loan l0
           ```
      *)
-  | AEndedMutLoan of { child : typed_avalue; given_back : typed_avalue }
+  | AEndedMutLoan of {
+      child : typed_avalue;
+      given_back : typed_avalue;
+      given_back_meta : mvalue;
+    }
       (** An ended mutable loan in an abstraction.
           We need it because abstractions must keep track of the values
           we gave back to them, so that we can correctly instantiate
           backward functions.
+          
+          Rk.: *DO NOT* use [visit_AEndedMutLoan]. If we update the order of
+          the arguments and you forget to swap them at the level of
+          [visit_AEndedMutLoan], you will not notice it.          
       
           Example:
           ========
@@ -388,15 +412,6 @@ and aloan_content =
           abs0 { a_ended_mut_loan { given_back = U32 3; child = ⊥; }
           x -> ⊥
           ```
-      
-          TODO: in the formalization, given_back was initially a typed value
-          (not an avalue). It seems more consistent to use a value, especially
-          because then the invariants about the borrows are simpler (otherwise,
-          there may be borrow ids duplicated in the context, which is very
-          annoying).
-          I think the original idea was that using values would make it
-          simple to instantiate the backward function (because projecting
-          deconstructs a bit the values with which we feed the function).
        *)
   | AEndedSharedLoan of typed_value * typed_avalue
       (** Similar to [AEndedMutLoan] but in this case there are no avalues to
@@ -424,8 +439,16 @@ and aloan_content =
           > x -> mut_borrow l0 (mut_borrow l1 @s1)
           ```
        *)
-  | AEndedIgnoredMutLoan of { child : typed_avalue; given_back : typed_avalue }
-      (** Similar to [AEndedMutLoan], for ignored loans *)
+  | AEndedIgnoredMutLoan of {
+      child : typed_avalue;
+      given_back : typed_avalue;
+      given_back_meta : mvalue;
+    }
+      (** Similar to [AEndedMutLoan], for ignored loans.
+
+           Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
+           See the comment for [AEndedMutLoan].
+       *)
   | AIgnoredSharedLoan of typed_avalue
       (** An ignored shared loan.
       
@@ -446,7 +469,7 @@ and aloan_content =
     children values).
 
     Note that contrary to [aloan_content], here the children avalues are
-    note independent of the parent avalues. For instance, a value
+    not independent of the parent avalues. For instance, a value
     `AMutBorrow (_, AMutBorrow (_, ...)` (ignoring the types) really is
     to be seen like a `mut_borrow ... (mut_borrow ...)`.
     
@@ -454,7 +477,7 @@ and aloan_content =
     ids)?
 *)
 and aborrow_content =
-  | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue
+  | AMutBorrow of mvalue * (BorrowId.id[@opaque]) * typed_avalue
       (** A mutable borrow owned by an abstraction.
       
           Is used when an abstraction "consumes" borrows, when giving borrows
@@ -474,6 +497,11 @@ and aborrow_content =
           > px -> ⊥
           > abs0 { a_mut_borrow l0 (U32 0) }
           ```
+          
+          The meta-value stores the initial value on which the projector was
+          applied, which reduced to this mut borrow. This meta-information
+          is only used for the synthesis.
+          TODO: do we really use it actually?
      *)
   | ASharedBorrow of (BorrowId.id[@opaque])
       (** A shared borrow owned by an abstraction.
@@ -565,9 +593,24 @@ and aborrow_content =
             abstraction so that we can properly call the backward functions
             when generating the pure translation.
        *)
+  | AEndedMutBorrow of mvalue * typed_avalue
+      (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value
+          that we gave back as a meta-value, to help with the synthesis.
+          We also remember the child [avalue] because this structural information
+          is useful for the synthesis (but not for the symbolic execution):
+          in practice the child value should only contain ended borrows, ignored
+          values, bottom values, etc.
+       *)
   | AEndedIgnoredMutBorrow of {
       child : typed_avalue;
       given_back_loans_proj : typed_avalue;
+      given_back_meta : mvalue;
+          (** [given_back_meta] is used to store the (symbolic) value we gave back
+              upon ending the borrow.
+
+              Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
+              See the comment for [AEndedMutLoan].
+          *)
     }  (** See the explanations for [AIgnoredMutBorrow] *)
   | AProjSharedBorrow of abstract_shared_borrows
       (** A projected shared borrow.
@@ -601,10 +644,7 @@ and aborrow_content =
           ```
        *)
 
-(* TODO: we may want to merge this with typed_value - would prevent some issues
-   when accessing fields....
-
-   TODO: the type of avalues doesn't make sense for loan avalues: they currently
+(* TODO: the type of avalues doesn't make sense for loan avalues: they currently
    are typed as `& (mut) T` instead of `T`...
 *)
 and typed_avalue = { value : avalue; ty : rty }
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index f3876f53..623703ee 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -26,6 +26,11 @@ let is_symbolic (v : value) : bool =
 let as_symbolic (v : value) : symbolic_value =
   match v with Symbolic s -> s | _ -> failwith "Unexpected"
 
+let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
+  match v.value with
+  | Borrow (MutBorrow (bid, bv)) -> (bid, bv)
+  | _ -> failwith "Unexpected"
+
 (** Check if a value contains a borrow *)
 let borrows_in_value (v : typed_value) : bool =
   let obj =