Add more loop examples and fix issues

16 files changed, 906 insertions, 250 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index f47c6226..ea61e2b2 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -138,7 +138,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return
   log#ldebug
     (lazy
       ("evaluate_function_symbolic_synthesize_backward_from_return:"
-     ^ "\n- back_id: "
+     ^ "\n- fname: "
+      ^ Print.fun_name_to_string fdef.name
+      ^ "\n- back_id: "
       ^ T.RegionGroupId.to_string back_id
       ^ "\n- loop_id: "
       ^ Print.option_to_string V.LoopId.to_string loop_id
@@ -213,6 +215,62 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       else ctx
     in
 
+    (* We now need to end the proper *input* abstractions - pay attention
+     * to the fact that we end the *input* abstractions, not the *return*
+     * abstractions (of course, the corresponding return abstractions will
+     * automatically be ended, because they consumed values coming from the
+     * input abstractions...) *)
+    (* End the parent abstractions and the current abstraction - note that we
+     * end them in an order which follows the regions hierarchy: it should lead
+     * to generated code which has a better consistency between the parent
+     * and children backward functions.
+     *
+     * Note that we don't end the same abstraction if we are *inside* a loop (i.e.,
+     * we are evaluating an [EndContinue]) or not.
+     *)
+    let current_abs_id, end_fun_synth_input =
+      let fun_abs_id =
+        (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
+      in
+      if not inside_loop then (fun_abs_id, true)
+      else
+        let pred (abs : V.abs) =
+          match abs.kind with
+          | V.Loop (_, rg_id', kind) ->
+              let rg_id' = Option.get rg_id' in
+              let is_ret =
+                match kind with V.LoopSynthInput -> true | V.LoopCall -> false
+              in
+              rg_id' = back_id && is_ret
+          | _ -> false
+        in
+        (* There is not necessarily an input synthesis abstraction specifically
+           for the loop.
+           If there is none, the input synthesis abstraction is actually the
+           function input synthesis abstraction.
+
+           Example:
+           ========
+           {[
+             fn clear(v: &mut Vec<u32>) {
+                 let mut i = 0;
+                 while i < v.len() {
+                     v[i] = 0;
+                     i += 1;
+                 }
+             }
+           ]}
+        *)
+        match C.ctx_find_abs ctx pred with
+        | Some abs -> (abs.abs_id, false)
+        | None -> (fun_abs_id, true)
+    in
+    log#ldebug
+      (lazy
+        ("evaluate_function_symbolic_synthesize_backward_from_return: ending \
+          input abstraction: "
+        ^ V.AbstractionId.to_string current_abs_id));
+
     (* Set the proper abstractions as endable *)
     let ctx =
       let visit_loop_abs =
@@ -237,7 +295,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
                 assert (loop_id = Some loop_id');
                 { abs with can_end = true }
             | V.SynthInput rg_id' ->
-                if rg_id' = back_id && not inside_loop then
+                if rg_id' = back_id && end_fun_synth_input then
                   { abs with can_end = true }
                 else abs
             | _ ->
@@ -248,41 +306,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       visit_loop_abs#visit_eval_ctx () ctx
     in
 
-    (* We now need to end the proper *input* abstractions - pay attention
-     * to the fact that we end the *input* abstractions, not the *return*
-     * abstractions (of course, the corresponding return abstractions will
-     * automatically be ended, because they consumed values coming from the
-     * input abstractions...) *)
-    (* End the parent abstractions and the current abstraction - note that we
-     * end them in an order which follows the regions hierarchy: it should lead
-     * to generated code which has a better consistency between the parent
-     * and children backward functions.
-     *
-     * Note that we don't end the same abstraction if we are *inside* a loop (i.e.,
-     * we are evaluating an [EndContinue]) or not.
-     *)
-    let current_abs_id =
-      if not inside_loop then
-        (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
-      else
-        let pred (abs : V.abs) =
-          match abs.kind with
-          | V.Loop (_, rg_id', kind) ->
-              let rg_id' = Option.get rg_id' in
-              let is_ret =
-                match kind with V.LoopSynthInput -> true | V.LoopCall -> false
-              in
-              rg_id' = back_id && is_ret
-          | _ -> false
-        in
-        let abs = Option.get (C.ctx_find_abs ctx pred) in
-        abs.abs_id
-    in
-    log#ldebug
-      (lazy
-        ("evaluate_function_symbolic_synthesize_backward_from_return: ending \
-          input abstraction: "
-        ^ V.AbstractionId.to_string current_abs_id));
     let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
     let cf_end_target_abs cf =
       List.fold_left
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index b2a46b1e..38c6df3d 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -753,6 +753,9 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
     | V.SynthRet _ -> V.SynthRetGivenBack
     | V.SynthInput _ -> V.SynthInputGivenBack
     | V.Loop _ -> V.LoopGivenBack
+    | V.Identity ->
+        (* Identity abstractions give back nothing *)
+        raise (Failure "Unreachable")
   in
   mk_fresh_symbolic_value sv_kind av.V.ty
 
@@ -1453,18 +1456,6 @@ let end_borrows config : V.BorrowId.Set.t -> cm_fun =
 let end_abstraction config = end_abstraction_aux config []
 let end_abstractions config = end_abstractions_aux config []
 
-(** Auxiliary function - call a function which requires a continuation,
-    and return the let context given to the continuation *)
-let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx =
-  let nctx = ref None in
-  let cf ctx =
-    assert (!nctx = None);
-    nctx := Some ctx;
-    None
-  in
-  let _ = f cf ctx in
-  Option.get !nctx
-
 let end_borrow_no_synth config id ctx =
   get_cf_ctx_no_synth (end_borrow config id) ctx
 
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 43580312..82d8586a 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -548,9 +548,22 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
-  | E.Shared | E.TwoPhaseMut ->
+  | E.Shared | E.TwoPhaseMut | E.Shallow ->
+      (* **REMARK**: we treat shallow borrows like shared borrows. In theory,
+         this is incomplete. But in practice, this should allow to handle
+         many cases: in effect, we are simply forbidding match guards from
+         performing too many modifications in the environment, which is
+         probably not a too bad thing to do.
+      *)
+
       (* Access the value *)
-      let access = if bkind = E.Shared then Read else Write in
+      let access =
+        match bkind with
+        | E.Shared | E.Shallow -> Read
+        | E.TwoPhaseMut -> Write
+        | _ -> raise (Failure "Unreachable")
+      in
+
       let expand_prim_copy = false in
       let prepare =
         access_rplace_reorganize_and_read config expand_prim_copy access p
@@ -578,12 +591,21 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         let ctx = write_place access p nv ctx in
         (* Compute the rvalue - simply a shared borrow with a the fresh id.
          * Note that the reference is *mutable* if we do a two-phase borrow *)
-        let rv_ty =
-          T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
+        let ref_kind =
+          match bkind with
+          | E.Shared | E.Shallow -> T.Shared
+          | E.TwoPhaseMut -> T.Mut
+          | _ -> raise (Failure "Unreachable")
         in
+        let rv_ty = T.Ref (T.Erased, v.ty, ref_kind) in
         let bc =
-          if bkind = E.Shared then V.SharedBorrow bid
-          else V.ReservedMutBorrow bid
+          match bkind with
+          | E.Shared | E.Shallow ->
+              (* See the remark at the beginning of the match branch: we
+                 handle shallow borrows like shared borrows *)
+              V.SharedBorrow bid
+          | E.TwoPhaseMut -> V.ReservedMutBorrow bid
+          | _ -> raise (Failure "Unreachable")
         in
         let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
         (* Continue *)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index d5d6fa7e..76085b55 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -89,7 +89,7 @@ type updt_env_kind =
 exception ValueMatchFailure of updt_env_kind
 
 (** Utility exception *)
-exception Distinct
+exception Distinct of string
 
 type ctx_or_update = (C.eval_ctx, updt_env_kind) result
 
@@ -1781,90 +1781,102 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
   module MkGetSetM (Id : Identifiers.Id) = struct
     module Inj = Id.InjSubst
 
-    let get (m : Inj.t ref) (k : Id.id) : Id.id =
-      match Inj.find_opt k !m with None -> k | Some k -> k
-
-    let add (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) =
-      if Inj.mem k0 !m then raise Distinct
-      else if Inj.Set.mem k1 (Inj.elements !m) then raise Distinct
-      else (
-        m := Inj.add k0 k1 !m;
-        k1)
-
-    let match_e (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) : Id.id =
-      let k0 = get m k0 in
-      if k0 = k1 then k1 else add m k0 k1
-
-    let match_el (m : Inj.t ref) (kl0 : Id.id list) (kl1 : Id.id list) :
-        Id.id list =
-      List.map (fun (k0, k1) -> match_e m k0 k1) (List.combine kl0 kl1)
+    let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) =
+      (* Check if k0 is already registered as a key *)
+      match Inj.find_opt k0 !m with
+      | None ->
+          (* Not registered: check if k1 is in the set of values,
+             otherwise add the binding *)
+          if Inj.Set.mem k1 (Inj.elements !m) then
+            raise
+              (Distinct
+                 (msg ^ "adding [k0=" ^ Id.to_string k0 ^ " -> k1="
+                ^ Id.to_string k1 ^ " ]: k1 already in the set of elements"))
+          else (
+            m := Inj.add k0 k1 !m;
+            k1)
+      | Some k1' ->
+          (* It is: check that the bindings are consistent *)
+          if k1 <> k1' then raise (Distinct (msg ^ "already a binding for k0"))
+          else k1
+
+    let match_e (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) : Id.id
+        =
+      (* TODO: merge the add and merge functions *)
+      add msg m k0 k1
+
+    let match_el (msg : string) (m : Inj.t ref) (kl0 : Id.id list)
+        (kl1 : Id.id list) : Id.id list =
+      List.map (fun (k0, k1) -> match_e msg m k0 k1) (List.combine kl0 kl1)
 
     (** Figuring out mappings between sets of ids is hard in all generality...
         We use the fact that the fresh ids should have been generated
         the same way (i.e., in the same order) and match the ids two by
         two in increasing order.
      *)
-    let match_es (m : Inj.t ref) (ks0 : Id.Set.t) (ks1 : Id.Set.t) : Id.Set.t =
-      Id.Set.of_list (match_el m (Id.Set.elements ks0) (Id.Set.elements ks1))
+    let match_es (msg : string) (m : Inj.t ref) (ks0 : Id.Set.t)
+        (ks1 : Id.Set.t) : Id.Set.t =
+      Id.Set.of_list
+        (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1))
   end
 
   module GetSetRid = MkGetSetM (T.RegionId)
 
-  let match_rid = GetSetRid.match_e S.rid_map
+  let match_rid = GetSetRid.match_e "match_rid: " S.rid_map
 
   (*  let match_ridl = GetSetRid.match_el S.rid_map *)
-  let match_rids = GetSetRid.match_es S.rid_map
+  let match_rids = GetSetRid.match_es "match_rids: " S.rid_map
 
   module GetSetBid = MkGetSetM (V.BorrowId)
 
-  let get_blid = GetSetBid.get S.blid_map
-  let match_blid = GetSetBid.match_e S.blid_map
-  let match_blidl = GetSetBid.match_el S.blid_map
-  let match_blids = GetSetBid.match_es S.blid_map
-
-  let get_borrow_id =
-    if S.check_equiv then get_blid else GetSetBid.get S.borrow_id_map
+  let match_blid msg = GetSetBid.match_e msg S.blid_map
+  let match_blidl msg = GetSetBid.match_el msg S.blid_map
+  let match_blids msg = GetSetBid.match_es msg S.blid_map
 
   let match_borrow_id =
-    if S.check_equiv then match_blid else GetSetBid.match_e S.borrow_id_map
+    if S.check_equiv then match_blid "match_borrow_id: "
+    else GetSetBid.match_e "match_borrow_id: " S.borrow_id_map
 
   let match_borrow_idl =
-    if S.check_equiv then match_blidl else GetSetBid.match_el S.borrow_id_map
+    if S.check_equiv then match_blidl "match_borrow_idl: "
+    else GetSetBid.match_el "match_borrow_idl: " S.borrow_id_map
 
   let match_borrow_ids =
-    if S.check_equiv then match_blids else GetSetBid.match_es S.borrow_id_map
-
-  let get_loan_id =
-    if S.check_equiv then get_blid else GetSetBid.get S.loan_id_map
+    if S.check_equiv then match_blids "match_borrow_ids: "
+    else GetSetBid.match_es "match_borrow_ids: " S.borrow_id_map
 
   let match_loan_id =
-    if S.check_equiv then match_blid else GetSetBid.match_e S.loan_id_map
+    if S.check_equiv then match_blid "match_loan_id: "
+    else GetSetBid.match_e "match_loan_id: " S.loan_id_map
 
   let match_loan_idl =
-    if S.check_equiv then match_blidl else GetSetBid.match_el S.loan_id_map
+    if S.check_equiv then match_blidl "match_loan_idl: "
+    else GetSetBid.match_el "match_loan_idl: " S.loan_id_map
 
   let match_loan_ids =
-    if S.check_equiv then match_blids else GetSetBid.match_es S.loan_id_map
+    if S.check_equiv then match_blids "match_loan_ids: "
+    else GetSetBid.match_es "match_loan_ids: " S.loan_id_map
 
   module GetSetSid = MkGetSetM (V.SymbolicValueId)
   module GetSetAid = MkGetSetM (V.AbstractionId)
 
-  let match_aid = GetSetAid.match_e S.aid_map
-  let match_aidl = GetSetAid.match_el S.aid_map
-  let match_aids = GetSetAid.match_es S.aid_map
+  let match_aid = GetSetAid.match_e "match_aid: " S.aid_map
+  let match_aidl = GetSetAid.match_el "match_aidl: " S.aid_map
+  let match_aids = GetSetAid.match_es "match_aids: " S.aid_map
 
   (** *)
-  let match_etys ty0 ty1 = if ty0 <> ty1 then raise Distinct else ty0
+  let match_etys ty0 ty1 =
+    if ty0 <> ty1 then raise (Distinct "match_etys") else ty0
 
   let match_rtys ty0 ty1 =
-    let match_distinct_types _ _ = raise Distinct in
+    let match_distinct_types _ _ = raise (Distinct "match_rtys") in
     let match_regions r0 r1 =
       match (r0, r1) with
       | T.Static, T.Static -> r1
       | Var rid0, Var rid1 ->
           let rid = match_rid rid0 rid1 in
           Var rid
-      | _ -> raise Distinct
+      | _ -> raise (Distinct "match_rtys")
     in
     match_types match_distinct_types match_regions ty0 ty1
 
@@ -1874,11 +1886,16 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
 
   let match_distinct_adts (_ty : T.ety) (_adt0 : V.adt_value)
       (_adt1 : V.adt_value) : V.typed_value =
-    raise Distinct
+    raise (Distinct "match_distinct_adts")
 
   let match_shared_borrows
       (match_typed_values : V.typed_value -> V.typed_value -> V.typed_value)
       (_ty : T.ety) (bid0 : V.borrow_id) (bid1 : V.borrow_id) : V.borrow_id =
+    log#ldebug
+      (lazy
+        ("MakeCheckEquivMatcher: match_shared_borrows: " ^ "bid0: "
+       ^ V.BorrowId.to_string bid0 ^ ", bid1: " ^ V.BorrowId.to_string bid1));
+
     let bid = match_borrow_id bid0 bid1 in
     (* If we don't check for equivalence (i.e., we apply a fixed-point),
        we lookup the shared values and match them.
@@ -1888,6 +1905,14 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
       else
         let v0 = S.lookup_shared_value_in_ctx0 bid0 in
         let v1 = S.lookup_shared_value_in_ctx1 bid1 in
+        log#ldebug
+          (lazy
+            ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:"
+           ^ "sv0: "
+            ^ typed_value_to_string S.ctx v0
+            ^ ", sv1: "
+            ^ typed_value_to_string S.ctx v1));
+
         let _ = match_typed_values v0 v1 in
         ()
     in
@@ -1914,14 +1939,24 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
     let id0 = sv0.sv_id in
     let id1 = sv1.sv_id in
 
+    log#ldebug
+      (lazy
+        ("MakeCheckEquivMatcher: match_symbolic_values: " ^ "sv0: "
+        ^ V.SymbolicValueId.to_string id0
+        ^ ", sv1: "
+        ^ V.SymbolicValueId.to_string id1));
+
     (* If we don't check for equivalence, we also update the map from sids
        to values *)
     if S.check_equiv then
       (* Create the joined symbolic value *)
-      let sv_id = GetSetSid.match_e S.sid_map id0 id1 in
+      let sv_id =
+        GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1
+      in
       let sv_ty = match_rtys sv0.V.sv_ty sv1.V.sv_ty in
       let sv_kind =
-        if sv0.V.sv_kind = sv1.V.sv_kind then sv0.V.sv_kind else raise Distinct
+        if sv0.V.sv_kind = sv1.V.sv_kind then sv0.V.sv_kind
+        else raise (Distinct "match_symbolic_values: sv_kind")
       in
       let sv = { V.sv_id; sv_ty; sv_kind } in
       sv
@@ -1942,7 +1977,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
 
   let match_symbolic_with_other (left : bool) (sv : V.symbolic_value)
       (v : V.typed_value) : V.typed_value =
-    if S.check_equiv then raise Distinct
+    if S.check_equiv then raise (Distinct "match_symbolic_with_other")
     else (
       assert left;
       let id = sv.sv_id in
@@ -1963,9 +1998,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
        a continue, where the fixed point contains some bottom values. *)
     if left && not (value_has_loans_or_borrows S.ctx v.V.value) then
       mk_bottom v.V.ty
-    else raise Distinct
+    else raise (Distinct "match_bottom_with_other")
 
-  let match_distinct_aadts _ _ _ _ _ = raise Distinct
+  let match_distinct_aadts _ _ _ _ _ = raise (Distinct "match_distinct_adts")
 
   let match_ashared_borrows _ty0 bid0 _ty1 bid1 ty =
     let bid = match_borrow_id bid0 bid1 in
@@ -2001,7 +2036,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
         ^ typed_avalue_to_string S.ctx v0
         ^ "\n- v1: "
         ^ typed_avalue_to_string S.ctx v1));
-    raise Distinct
+    raise (Distinct "match_avalues")
 end
 
 (** See {!match_ctxs} *)
@@ -2154,7 +2189,8 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
     in
 
     let _ = CEM.match_aid abs_id0 abs_id1 in
-    if kind0 <> kind1 || can_end0 <> can_end1 then raise Distinct;
+    if kind0 <> kind1 || can_end0 <> can_end1 then
+      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
@@ -2192,21 +2228,19 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
     match (env0, env1) with
     | ( C.Var (C.DummyBinder b0, v0) :: env0',
         C.Var (C.DummyBinder b1, v1) :: env1' ) ->
-        (* Two cases: the dummy value is an old value, in which case the bindings
-           must be the same and their values equal (and the borrows/loans/symbolic
-           values they reference must be fixed) *)
+        (* Sanity check: if the dummy value is an old value, the bindings must
+           be the same and their values equal (and the borrows/loans/symbolic *)
         if C.DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Fixed values: the values must be equal *)
           assert (b0 = b1);
           assert (v0 = v1);
           (* The ids present in the left value must be fixed *)
           let ids, _ = compute_typed_value_ids v0 in
-          assert ((not S.check_equiv) || ids_are_fixed ids);
-          (* Continue *)
-          match_envs env0' env1')
-        else
-          let _ = M.match_typed_values ctx v0 v1 in
-          match_envs env0' env1'
+          assert ((not S.check_equiv) || ids_are_fixed ids));
+        (* We still match the values - allows to compute mappings (which
+           are the identity actually) *)
+        let _ = M.match_typed_values ctx v0 v1 in
+        match_envs env0' env1'
     | C.Var (C.VarBinder b0, v0) :: env0', C.Var (C.VarBinder b1, v1) :: env1'
       ->
         assert (b0 = b1);
@@ -2238,7 +2272,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
         ()
     | _ ->
         (* The elements don't match *)
-        raise Distinct
+        raise (Distinct "match_ctxs: match_envs: env elements don't match")
   in
 
   (* Match the environments.
@@ -2267,7 +2301,9 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets)
       }
     in
     Some maps
-  with Distinct -> None
+  with Distinct msg ->
+    log#ldebug (lazy ("match_ctxs: distinct: " ^ msg));
+    None
 
 (** Compute whether two contexts are equivalent modulo an identifier substitution.
 
@@ -2350,17 +2386,6 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
         ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
        ^ eval_ctx_to_string ctx));
 
-    (* (* Push the abstractions introduced by {!prepare_shared_loans} as
-          far as we can to preserve the structure of the context. *)
-       let ctx =
-         push_fresh_shared_loans_abs fresh_shared_loans_abs_ids original_ctx_length
-           ctx
-       in
-       log#ldebug
-         (lazy
-           ("loop_join_origin_with_continue_ctxs:join_one: after push fresh \
-             shared loan abs:\n" ^ eval_ctx_to_string ctx)); *)
-
     (* Destructure the abstractions introduced in the new context *)
     let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in
     log#ldebug
@@ -2435,9 +2460,40 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
     We do this because it makes it easier to compute joins and fixed points.
 
     We return the new context and the set of fresh abs ids.
+
+    **REMARK**:
+    As a side note, only reborrow the loan ids whose corresponding borrows appear in
+    values (i.e., not in abstractions).
+
+    For instance, if we have:
+    {[
+      abs'0 {
+        SL {l0} s0
+        SL {l1} s1
+      }
+      abs'1 { SB l0 }
+      x -> SB l1
+    ]}
+
+    we only introduce a fresh abstraction for [l1].
+  *)
+let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun =
+ fun cf ctx0 ->
+  let ctx = ctx0 in
+  (* Compute the set of borrows which appear in the abstractions, so that
+     we can filter the borrows that we reborrow.
   *)
-let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.AbstractionId.Set.t =
+  let absl =
+    List.filter_map
+      (function C.Var _ | C.Frame -> None | C.Abs abs -> Some abs)
+      ctx.env
+  in
+  let absl_ids, absl_id_maps = compute_absl_ids absl in
+  let abs_borrow_ids = absl_ids.borrow_ids in
+
+  (* Map from the fresh sids to the original symbolic values *)
+  let sid_subst = ref [] in
+
   (* Return the same value but where:
      - the shared loans have been removed
      - the symbolic values have been replaced with fresh symbolic values
@@ -2453,7 +2509,11 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
       (fun r -> if T.RegionId.Set.mem r rids then nrid else r)
       (fun x -> x)
       (fun x -> x)
-      (fun _ -> C.fresh_symbolic_value_id ())
+      (fun id ->
+        let nid = C.fresh_symbolic_value_id () in
+        let sv = V.SymbolicValueId.Map.find id absl_id_maps.sids_to_values in
+        sid_subst := (nid, sv) :: !sid_subst;
+        nid)
       (fun x -> x)
       v
   in
@@ -2522,7 +2582,11 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
 
     (* Create the abstraction *)
     let avalues = [ borrow_value; loan_value ] in
-    let kind = V.Loop (loop_id, None, V.LoopSynthInput) in
+    let kind =
+      match loop_id with
+      | Some loop_id -> V.Loop (loop_id, None, V.LoopSynthInput)
+      | None -> V.Identity
+    in
     let can_end = true in
     let fresh_abs =
       {
@@ -2546,26 +2610,30 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
      when necessary.
   *)
   let collect_shared_values_in_abs (abs : V.abs) : unit =
+    let collect_shared_value lids (sv : V.typed_value) =
+      (* Sanity check: we don't support nested borrows for now *)
+      assert (not (value_has_borrows ctx sv.V.value));
+
+      (* Filter the loan ids whose corresponding borrows appear in abstractions
+         (see the documentation of the function) *)
+      let lids = V.BorrowId.Set.diff lids abs_borrow_ids in
+
+      (* Generate fresh borrows and values *)
+      V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids
+    in
+
     let visit_avalue =
       object
         inherit [_] V.iter_typed_avalue as super
 
         method! visit_SharedLoan env lids sv =
-          (* Sanity check: we don't support nested borrows for now *)
-          assert (not (value_has_borrows ctx sv.V.value));
-
-          (* Generate fresh borrows and values *)
-          V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids;
+          collect_shared_value lids sv;
 
           (* Continue the exploration *)
           super#visit_SharedLoan env lids sv
 
         method! visit_ASharedLoan env lids sv _ =
-          (* Sanity check: we don't support nested borrows for now *)
-          assert (not (value_has_borrows ctx sv.V.value));
-
-          (* Generate fresh borrows and values *)
-          V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids;
+          collect_shared_value lids sv;
 
           (* Continue the exploration *)
           super#visit_SharedLoan env lids sv
@@ -2635,14 +2703,30 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
   in
 
   (* Add the abstractions *)
-  let fresh_abs_ids =
-    V.AbstractionId.Set.of_list (List.map (fun abs -> abs.V.abs_id) !fresh_absl)
-  in
   let fresh_absl = List.map (fun abs -> C.Abs abs) !fresh_absl in
   let env = List.append fresh_absl env in
-
-  (* Return *)
-  ({ ctx with C.env }, fresh_abs_ids)
+  let ctx = { ctx with env } in
+
+  let _, new_ctx_ids_map = compute_context_ids ctx in
+
+  (* Synthesize *)
+  match cf ctx with
+  | None -> None
+  | Some e ->
+      (* Add the let-bindings which introduce the fresh symbolic values *)
+      Some
+        (List.fold_left
+           (fun e (sid, v) ->
+             let v = mk_typed_value_from_symbolic_value v in
+             let sv =
+               V.SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values
+             in
+             SymbolicAst.IntroSymbolic (ctx, None, sv, v, e))
+           e !sid_subst)
+
+let prepare_ashared_loans_no_synth (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  get_cf_ctx_no_synth (prepare_ashared_loans (Some loop_id)) ctx
 
 (** Compute a fixed-point for the context at the entry of the loop.
     We also return the sets of fixed ids, and the list of symbolic values
@@ -2669,7 +2753,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
 
      For more details, see the comments for {!prepare_ashared_loans}
   *)
-  let ctx, _ = prepare_ashared_loans loop_id ctx0 in
+  let ctx = prepare_ashared_loans_no_synth loop_id ctx0 in
 
   (* Debug *)
   log#ldebug
@@ -2935,9 +3019,23 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
           (* Retrieve the first id of the group *)
           match ids with
           | [] ->
-              (* This would be rather unexpected... let's fail for now to see
-                 in which situations this happens *)
-              raise (Failure "Unexpected")
+              (* This happens for instance in the following case (there
+                 is no "magic wand" linking the values before and after
+                 the loop, in particular because we return nothing):
+
+                 Example:
+                 ========
+                 {[
+                   fn clear(v: &mut Vec<u32>) {
+                       let mut i = 0;
+                       while i < v.len() {
+                           v[i] = 0;
+                           i += 1;
+                       }
+                   }
+                 ]}
+              *)
+              ()
           | id0 :: ids ->
               let id0 = ref id0 in
               (* Add the proper region group into the abstraction *)
@@ -3072,6 +3170,7 @@ type borrow_loan_corresp = {
   borrow_to_loan_id_map : V.BorrowId.InjSubst.t;
   loan_to_borrow_id_map : V.BorrowId.InjSubst.t;
 }
+[@@deriving show]
 
 let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
   let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } =
@@ -3442,10 +3541,14 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
    **Parameters**:
    [is_loop_entry]: [true] if first entry into the loop, [false] if re-entry
    (i.e., continue).
+   [fp_input_svalues]: the list of symbolic values appearing in the fixed
+   point and which must be instantiated during the match (this is the list
+   of input parameters of the loop).
  *)
 let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
-    (fixed_ids : ids_sets) (src_ctx : C.eval_ctx) : st_cm_fun =
+    (fp_input_svalues : V.SymbolicValueId.id list) (fixed_ids : ids_sets)
+    (src_ctx : C.eval_ctx) : st_cm_fun =
  fun cf tgt_ctx ->
   (* Debug *)
   log#ldebug
@@ -3543,10 +3646,14 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
      we substitute the loans and introduce fresh ids for the borrows, symbolic
      values, etc. About the *identity abstractions*, see the comments for
      [compute_fixed_point_id_correspondance].
+
+     TODO: this whole thing is very technical and error-prone.
+     We should rely on a more primitive and safer function
+     [add_identity_abs] to add the identity abstractions one by one.
   *)
   let cf_introduce_loop_fp_abs : m_fun =
    fun tgt_ctx ->
-    (* Match the tgt and target contexts *)
+    (* Match the source and target contexts *)
     let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in
     let filt_src_env, new_absl, new_dummyl =
       ctx_split_fixed_new fixed_ids src_ctx
@@ -3555,8 +3662,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in
     let filt_src_ctx = { src_ctx with env = filt_src_env } in
 
-    let check_equiv = false in
     let src_to_tgt_maps =
+      let check_equiv = false in
       let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in
       let open InterpreterBorrowsCore in
       let lookup_shared_loan lid ctx : V.typed_value =
@@ -3567,6 +3674,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
       in
       let lookup_in_src id = lookup_shared_loan id src_ctx in
       let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
+      (* Match *)
       Option.get
         (match_ctxs check_equiv fixed_ids lookup_in_src lookup_in_tgt
            filt_src_ctx filt_tgt_ctx)
@@ -3581,12 +3689,17 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     (* Debug *)
     log#ldebug
       (lazy
-        ("match_ctx_with_target:cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: "
+        ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: "
        ^ eval_ctx_to_string tgt_ctx ^ "\n\n- src_ctx: "
        ^ eval_ctx_to_string src_ctx ^ "\n\n- filt_tgt_ctx: "
-        ^ eval_ctx_to_string filt_tgt_ctx
+        ^ eval_ctx_to_string_no_filter filt_tgt_ctx
         ^ "\n\n- filt_src_ctx: "
-        ^ eval_ctx_to_string filt_src_ctx
+        ^ eval_ctx_to_string_no_filter filt_src_ctx
+        ^ "\n\n- new_absl:\n"
+        ^ eval_ctx_to_string
+            { src_ctx with C.env = List.map (fun abs -> C.Abs abs) new_absl }
+        ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n"
+        ^ show_borrow_loan_corresp fp_bl_maps
         ^ "\n\n- src_to_tgt_maps: "
         ^ show_ids_maps src_to_tgt_maps));
 
@@ -3618,8 +3731,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
          }
        ]}
 
-       Through matching, we detected that in [env_fp], [l1] will be matched
-       to [l5]. We introduced a fresh borrow [l6] for [l1], and remember
+       Through matching, we detect that in [env_fp], [l1] is matched
+       to [l5]. We introduce a fresh borrow [l6] for [l1], and remember
        in the map [src_fresh_borrows_map] that: [{ l1 -> l6}].
 
        We get:
@@ -3638,6 +3751,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
          abs@2 { MB l5, ML l6 }
        ]}
     *)
+    (* First, compute the set of borrows which appear in the fresh abstractions
+       of the fixed-point: we want to introduce fresh ids only for those. *)
+    let new_absl_ids, _ = compute_absl_ids new_absl in
     let src_fresh_borrows_map = ref V.BorrowId.Map.empty in
     let visit_tgt =
       object
@@ -3646,8 +3762,13 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
         method! visit_borrow_id _ id =
           (* Map the borrow, if it needs to be mapped *)
           if
+            (* We map the borrows for which we computed a mapping *)
             V.BorrowId.InjSubst.Set.mem id
               (V.BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map)
+            (* And which have corresponding loans in the fresh fixed-point abstractions *)
+            && V.BorrowId.Set.mem
+                 (V.BorrowId.Map.find id tgt_to_src_borrow_map)
+                 new_absl_ids.loan_ids
           then (
             let src_id = V.BorrowId.Map.find id tgt_to_src_borrow_map in
             let nid = C.fresh_borrow_id () in
@@ -3659,6 +3780,13 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     in
     let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in
 
+    log#ldebug
+      (lazy
+        ("match_ctx_with_target: cf_introduce_loop_fp_abs: \
+          src_fresh_borrows_map:\n"
+        ^ V.BorrowId.Map.show V.BorrowId.to_string !src_fresh_borrows_map
+        ^ "\n"));
+
     (* Rem.: we don't update the symbolic values. It is not necessary
        because there shouldn't be any symbolic value containing borrows.
 
@@ -3695,21 +3823,54 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
         inherit [_] C.map_eval_ctx as super
 
         method! visit_borrow_id _ bid =
+          log#ldebug
+            (lazy
+              ("match_ctx_with_target: cf_introduce_loop_fp_abs: \
+                visit_borrow_id: " ^ V.BorrowId.to_string bid ^ "\n"));
+
           (* Lookup the id of the loan corresponding to this borrow *)
           let src_lid =
             V.BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map
           in
+
+          log#ldebug
+            (lazy
+              ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \
+                src_lid: "
+              ^ V.BorrowId.to_string src_lid
+              ^ "\n"));
+
           (* Lookup the tgt borrow id to which this borrow was mapped *)
           let tgt_bid =
             V.BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map
           in
+
+          log#ldebug
+            (lazy
+              ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \
+                tgt_bid: "
+              ^ V.BorrowId.to_string tgt_bid
+              ^ "\n"));
+
           tgt_bid
 
         method! visit_loan_id _ id =
+          log#ldebug
+            (lazy
+              ("match_ctx_with_target: cf_introduce_loop_fp_abs: \
+                visit_loan_id: " ^ V.BorrowId.to_string id ^ "\n"));
           (* Map the borrow - rem.: we mapped the borrows *in the values*,
              meaning we know how to map the *corresponding loans in the
              abstractions* *)
-          V.BorrowId.Map.find id !src_fresh_borrows_map
+          match V.BorrowId.Map.find_opt id !src_fresh_borrows_map with
+          | None ->
+              (* No mapping: this means that the borrow was mapped when
+                 we matched values (it doesn't come from a fresh abstraction)
+                 and because of this, it should actually be mapped to itself *)
+              assert (
+                V.BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id);
+              id
+          | Some id -> id
 
         method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id ()
         method! visit_abstraction_id _ _ = C.fresh_abstraction_id ()
@@ -3752,7 +3913,15 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     let cc = InterpreterBorrows.end_borrows config new_borrows in
 
     (* Compute the loop input values *)
-    let input_values = src_to_tgt_maps.sid_to_value_map in
+    let input_values =
+      V.SymbolicValueId.Map.of_list
+        (List.map
+           (fun sid ->
+             ( sid,
+               V.SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map
+             ))
+           fp_input_svalues)
+    in
 
     (* Continue *)
     cc
@@ -3812,6 +3981,95 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
   (* Apply *)
   eval_loop_body reeval_loop_body ctx
 
+(** Compute the set of "quantified" symbolic value ids in a fixed-point context.
+
+    We compute:
+    - the set of symbolic value ids that are freshly introduced
+    - the list of input symbolic values
+ *)
+let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) :
+    V.SymbolicValueId.Set.t * V.symbolic_value list =
+  let old_ids, _ = compute_context_ids ctx in
+  let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in
+  let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in
+
+  (* Compute the set of symbolic values which appear in shared values inside
+     *fixed* abstractions: because we introduce fresh abstractions and reborrows
+     with {!prepare_ashared_loans}, those values are never accessed directly
+     inside the loop iterations: we can ignore them (and should, because
+     otherwise it leads to a very ugly translation with duplicated, unused
+     values) *)
+  let shared_sids_in_fixed_abs =
+    let fixed_absl =
+      List.filter
+        (fun (ee : C.env_elem) ->
+          match ee with
+          | C.Var _ | C.Frame -> false
+          | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids)
+        ctx.env
+    in
+
+    (* Rem.: as we greedily expand the symbolic values containing borrows, and
+       in particular the (mutable/shared) borrows, we could simply list the
+       symbolic values appearing in the abstractions: those are necessarily
+       shared values. We prefer to be more general, in prevision of later
+       changes.
+    *)
+    let sids = ref V.SymbolicValueId.Set.empty in
+    let visitor =
+      object (self : 'self)
+        inherit [_] C.iter_env
+
+        method! visit_ASharedLoan inside_shared _ sv child_av =
+          self#visit_typed_value true sv;
+          self#visit_typed_avalue inside_shared child_av
+
+        method! visit_symbolic_value_id inside_shared sid =
+          if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids
+      end
+    in
+    visitor#visit_env false fixed_absl;
+    !sids
+  in
+
+  (* Remove the shared symbolic values present in the fixed abstractions -
+     see comments for [shared_sids_in_fixed_abs]. *)
+  let sids_to_values = fp_ids_maps.sids_to_values in
+
+  log#ldebug
+    (lazy
+      ("compute_fp_ctx_symbolic_values:" ^ "\n- shared_sids_in_fixed_abs:"
+      ^ V.SymbolicValueId.Set.show shared_sids_in_fixed_abs
+      ^ "\n- all_sids_to_values: "
+      ^ V.SymbolicValueId.Map.show (symbolic_value_to_string ctx) sids_to_values
+      ^ "\n"));
+
+  let sids_to_values =
+    V.SymbolicValueId.Map.filter
+      (fun sid _ ->
+        not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs))
+      sids_to_values
+  in
+
+  (* The value ids should be listed in increasing order *)
+  let input_svalues =
+    List.map snd (V.SymbolicValueId.Map.bindings sids_to_values)
+  in
+
+  log#ldebug
+    (lazy
+      ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n"
+      ^ eval_ctx_to_string_no_filter ctx
+      ^ "\n- fixed point:\n"
+      ^ eval_ctx_to_string_no_filter fp_ctx
+      ^ "\n- fresh_sids: "
+      ^ V.SymbolicValueId.Set.show fresh_sids
+      ^ "\n- input_svalues: "
+      ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues
+      ^ "\n\n"));
+
+  (fresh_sids, input_svalues)
+
 (** Evaluate a loop in symbolic mode *)
 let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     st_cm_fun =
@@ -3820,14 +4078,9 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
   log#ldebug
     (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
 
-  (* Compute a fresh loop id *)
+  (* Generate a fresh loop id *)
   let loop_id = C.fresh_loop_id () in
 
-  log#ldebug
-    (lazy
-      ("eval_loop_symbolic:\nContext after shared borrows preparation:\n"
-     ^ eval_ctx_to_string ctx ^ "\n\n"));
-
   (* Compute the fixed point at the loop entrance *)
   let fp_ctx, fixed_ids =
     compute_loop_entry_fixed_point config loop_id eval_loop_body ctx
@@ -3839,6 +4092,10 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
       ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ctx
      ^ "\n\nFixed point:\n" ^ eval_ctx_to_string fp_ctx));
 
+  (* Compute the loop input parameters *)
+  let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values ctx fp_ctx in
+  let fp_input_svalues = List.map (fun sv -> sv.V.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
      will end with a call to the loop translation
@@ -3847,8 +4104,8 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx
   in
   let end_expr =
-    match_ctx_with_target config loop_id true fp_bl_corresp fixed_ids fp_ctx cf
-      ctx
+    match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues
+      fixed_ids fp_ctx cf ctx
   in
 
   (* Synthesize the loop body by evaluating it, with the continuation for
@@ -3869,8 +4126,8 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
         (* We don't support nested loops for now *)
         assert (i = 0);
         let cc =
-          match_ctx_with_target config loop_id false fp_bl_corresp fixed_ids
-            fp_ctx
+          match_ctx_with_target config loop_id false fp_bl_corresp
+            fp_input_svalues fixed_ids fp_ctx
         in
         cc cf ctx
     | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
@@ -3881,75 +4138,18 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
   in
   let loop_expr = eval_loop_body cf_loop fp_ctx in
 
-  (* Compute the list of fresh symbolic values *)
-  let fresh_sids, input_svalues =
-    let old_ids, _ = compute_context_ids ctx in
-    let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in
-    let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in
-
-    (* Compute the set of symbolic values which appear in shared values inside
-       *fixed* abstractions: because we introduce fresh abstractions and reborrows
-       with {!prepare_ashared_loans}, those values are never accessed directly
-       inside the loop iterations: we can ignore them (and should, because
-       otherwise it leads to a very ugly translation with duplicated, unused
-       values) *)
-    let shared_sids_in_fixed_abs =
-      let fixed_absl =
-        List.filter
-          (fun (ee : C.env_elem) ->
-            match ee with
-            | C.Var _ | C.Frame -> false
-            | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids)
-          ctx.env
-      in
-
-      (* Rem.: as we greedily expand the symbolic values containing borrows, and
-         in particular the (mutable/shared) borrows, we could simply list the
-         symbolic values appearing in the abstractions: those are necessarily
-         shared values. We prefer to be more general, in prevision of later
-         changes.
-      *)
-      let sids = ref V.SymbolicValueId.Set.empty in
-      let visitor =
-        object (self : 'self)
-          inherit [_] C.iter_env
-
-          method! visit_ASharedLoan inside_shared _ sv child_av =
-            self#visit_typed_value true sv;
-            self#visit_typed_avalue inside_shared child_av
-
-          method! visit_symbolic_value_id inside_shared sid =
-            if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids
-        end
-      in
-      visitor#visit_env false fixed_absl;
-      !sids
-    in
-
-    (* Remove the shared symbolic values present in the fixed abstractions -
-       see comments for [shared_sids_in_fixed_abs]. *)
-    let sids_to_values = fp_ids_maps.sids_to_values in
-    let sids_to_values =
-      V.SymbolicValueId.Map.filter
-        (fun sid _ ->
-          not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs))
-        sids_to_values
-    in
-    (* The value ids should be listed in increasing order *)
-    let input_svalues =
-      List.map snd (V.SymbolicValueId.Map.bindings sids_to_values)
-    in
-    (fresh_sids, input_svalues)
-  in
-
   log#ldebug
     (lazy
       ("eval_loop_symbolic: result:" ^ "\n- src context:\n"
-     ^ eval_ctx_to_string ctx ^ "\n- fixed point:\n" ^ eval_ctx_to_string fp_ctx
-     ^ "\n- fixed_sids: "
+      ^ eval_ctx_to_string_no_filter ctx
+      ^ "\n- fixed point:\n"
+      ^ eval_ctx_to_string_no_filter fp_ctx
+      ^ "\n- fixed_sids: "
       ^ V.SymbolicValueId.Set.show fixed_ids.sids
-      ^ "\n- input_svalues: "
+      ^ "\n- fresh_sids: "
       ^ V.SymbolicValueId.Set.show fresh_sids
+      ^ "\n- input_svalues: "
+      ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues
       ^ "\n\n"));
 
   (* Put together *)
@@ -3960,4 +4160,24 @@ let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
   match config.C.mode with
   | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
-  | SymbolicMode -> eval_loop_symbolic config eval_loop_body cf ctx
+  | SymbolicMode ->
+      (* We want to make sure the loop will *not* manipulate shared avalues
+         containing themselves shared loans (i.e., nested shared loans in
+         the abstractions), because it complexifies the matches between values
+         (when joining environments, or checking that two environments are
+         equivalent).
+
+         We thus call {!prepare_ashared_loans} once *before* diving into
+         the loop, to make sure the shared values are deconstructed.
+
+         Note that we will call this function again inside {!eval_loop_symbolic},
+         to introduce fresh, non-fixed abstractions containing the shared values
+         which can be manipulated (and thus borrowed, expanded, etc.) so
+         that the fixed abstractions are never modified.
+
+         This is important to understand: we call this function once here to
+         introduce *fixed* abstractions, and again later to introduce
+         *non-fixed* abstractions.
+      *)
+      let cc = prepare_ashared_loans None in
+      comp cc (eval_loop_symbolic config eval_loop_body) cf ctx
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index fe508f6b..f5b1111e 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -811,12 +811,12 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
                   let expr = assign_to_place config rv p (cf Unit) ctx in
                   (* Update the synthesized AST - here we store meta-information.
                    * We do it only in specific cases (it is not always useful, and
-                   * also it can lead to issues - for instance, if we borrow an
+                   * also it can lead to issues - for instance, if we borrow a
                    * reserved borrow, we later can't translate it to pure values...) *)
                   match rvalue with
                   | E.Global _ -> raise (Failure "Unreachable")
                   | E.Use _
-                  | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut))
+                  | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow))
                   | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _
                   | E.Aggregate _ ->
                       let rp = rvalue_get_place rvalue in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 670435a5..d60ddfe6 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -8,9 +8,22 @@ module L = Logging
 open Utils
 open TypesUtils
 module PA = Print.EvalCtxLlbcAst
+open Cps
 
 (** Some utilities *)
 
+(** Auxiliary function - call a function which requires a continuation,
+    and return the let context given to the continuation *)
+let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx =
+  let nctx = ref None in
+  let cf ctx =
+    assert (!nctx = None);
+    nctx := Some ctx;
+    None
+  in
+  let _ = f cf ctx in
+  Option.get !nctx
+
 let eval_ctx_to_string_no_filter = Print.Contexts.eval_ctx_to_string_no_filter
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
 let ety_to_string = PA.ety_to_string
@@ -368,12 +381,16 @@ let compute_absl_ids (xl : V.abs list) : ids_sets * ids_to_values =
 let compute_abs_ids (x : V.abs) : ids_sets * ids_to_values =
   compute_absl_ids [ x ]
 
-(** Compute the sets of ids found in an environment element. *)
-let compute_env_elem_ids (x : C.env_elem) : ids_sets * ids_to_values =
+(** Compute the sets of ids found in an environment. *)
+let compute_env_ids (x : C.env) : ids_sets * ids_to_values =
   let compute, get_ids, get_ids_to_values = compute_ids () in
-  compute#visit_env_elem () x;
+  compute#visit_env () x;
   (get_ids (), get_ids_to_values ())
 
+(** Compute the sets of ids found in an environment element. *)
+let compute_env_elem_ids (x : C.env_elem) : ids_sets * ids_to_values =
+  compute_env_ids [ x ]
+
 (** Compute the sets of ids found in a list of contexts. *)
 let compute_contexts_ids (ctxl : C.eval_ctx list) : ids_sets * ids_to_values =
   let compute, get_ids, get_ids_to_values = compute_ids () in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index c69e6441..981c2c46 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -784,7 +784,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
 
 let check_invariants (ctx : C.eval_ctx) : unit =
   if !Config.check_invariants then (
-    log#ldebug (lazy "Checking invariants");
+    log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx));
     check_loans_borrows_relation_invariant ctx;
     check_borrowed_values_invariant ctx;
     check_typing_invariant ctx;
diff --git a/compiler/Print.ml b/compiler/Print.ml
index d040680f..cf227172 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -315,6 +315,7 @@ module Values = struct
         ^ ", loop abs kind: "
         ^ loop_abs_kind_to_string abs_kind
         ^ ")"
+    | Identity -> "Identity"
 
   let abs_to_string (fmt : value_formatter) (verbose : bool) (indent : string)
       (indent_incr : string) (abs : V.abs) : string =
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 33082dc3..de68adc3 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -426,7 +426,7 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) :
   let lp_suff =
     match lp_id with
     | None -> ""
-    | Some lp_id -> "^loop^" ^ LoopId.to_string lp_id
+    | Some lp_id -> "^loop" ^ LoopId.to_string lp_id
   in
 
   let rg_suff =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 4ecb194b..7f682c9c 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -160,6 +160,22 @@ type expression =
           We use it to compute meaningful names for the variables we introduce,
           to prettify the generated code.
        *)
+  | IntroSymbolic of
+      Contexts.eval_ctx
+      * mplace option
+      * V.symbolic_value
+      * V.typed_value
+      * expression
+      (** We introduce a new symbolic value, equal to some other value.
+
+        This is used for instance when reorganizing the environment to compute
+        fixed points: we duplicate some shared symbolic values to destructure
+        the shared values, in order to make the environment a bit more general
+        (while losing precision of course).
+
+        The context is the evaluation context from before introducing the new
+        value. It has the same purpose as for the {!Return} case.
+      *)
   | ForwardEnd of
       Contexts.eval_ctx
       * V.typed_value symbolic_value_id_map option
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 174fc4d1..b2b5e010 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1278,6 +1278,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx
   | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx
   | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
+  | IntroSymbolic (ectx, p, sv, v, e) ->
+      translate_intro_symbolic ectx p sv v e ctx
   | Meta (meta, e) -> translate_meta meta e ctx
   | ForwardEnd (ectx, loop_input_values, e, back_e) ->
       translate_forward_end ectx loop_input_values e back_e ctx
@@ -1521,6 +1523,7 @@ and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs)
   | V.SynthRet rg_id -> translate_end_abstraction_synth_ret ectx abs e ctx rg_id
   | V.Loop (loop_id, rg_id, abs_kind) ->
       translate_end_abstraction_loop ectx abs e ctx loop_id rg_id abs_kind
+  | V.Identity -> translate_end_abstraction_identity ectx abs e ctx
 
 and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
     (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression
@@ -1707,6 +1710,20 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     next_e)
   else mk_let effect_info.can_fail output call next_e
 
+and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
+    (e : S.expression) (ctx : bs_ctx) : texpression =
+  (* We simply check that the abstraction only contains shared borrows/loans,
+     and translate the next expression *)
+
+  (* We can do this simply by checking that it consumes and gives back nothing *)
+  let inputs = abs_to_consumed ctx ectx abs in
+  let ctx, outputs = abs_to_given_back None abs ctx in
+  assert (inputs = []);
+  assert (outputs = []);
+
+  (* Translate the next expression *)
+  translate_expression e ctx
+
 and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
     (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression
     =
@@ -2087,6 +2104,25 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
         List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches);
       { e; ty }
 
+and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
+    (sv : V.symbolic_value) (v : V.typed_value) (e : S.expression)
+    (ctx : bs_ctx) : texpression =
+  let mplace = translate_opt_mplace p in
+
+  (* Introduce a fresh variable for the symbolic value *)
+  let ctx, var = fresh_var_for_symbolic_value sv ctx in
+
+  (* Translate the value *)
+  let v = typed_value_to_texpression ctx ectx v in
+
+  (* Translate the next expression *)
+  let next_e = translate_expression e ctx in
+
+  (* Make the let-binding *)
+  let monadic = false in
+  let var = mk_typed_pattern_from_var var mplace in
+  mk_let monadic var v next_e
+
 and translate_forward_end (ectx : C.eval_ctx)
     (loop_input_values : V.typed_value S.symbolic_value_id_map option)
     (e : S.expression) (back_e : S.expression S.region_group_id_map)
@@ -2129,12 +2165,19 @@ and translate_forward_end (ectx : C.eval_ctx)
           ^ "\n- loop_info.input_svl:\n"
           ^ Print.list_to_string
               (symbolic_value_to_string ctx)
-              loop_info.input_svl));
+              loop_info.input_svl
+          ^ "\n"));
 
       (* Translate the input values *)
       let loop_input_values =
         List.map
-          (fun sv -> V.SymbolicValueId.Map.find sv.V.sv_id loop_input_values)
+          (fun sv ->
+            log#ldebug
+              (lazy
+                ("translate_forward_end: looking up input_svl: "
+                ^ V.SymbolicValueId.to_string sv.V.sv_id
+                ^ "\n"));
+            V.SymbolicValueId.Map.find sv.V.sv_id loop_input_values)
           loop_info.input_svl
       in
       let args =
@@ -2218,8 +2261,12 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
     in
     log#ldebug
       (lazy
-        ("translate_loop:" ^ "\n- filtered svl: "
-        ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl));
+        ("translate_loop:" ^ "\n- input_svalues: "
+        ^ (Print.list_to_string (symbolic_value_to_string ctx))
+            loop.input_svalues
+        ^ "\n- filtered svl: "
+        ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl
+        ^ "\n"));
     let ctx, _ = fresh_vars_for_symbolic_values svl ctx in
     ctx
   in
@@ -2384,7 +2431,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
       ^ Print.fun_name_to_string def.A.name
       ^ " ("
       ^ Print.option_to_string T.RegionGroupId.to_string bid
-      ^ ")"));
+      ^ ")\n"));
 
   (* Translate the declaration *)
   let def_id = def.A.def_id in
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 7d5ecc01..d4eff58a 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -939,6 +939,13 @@ type abs_kind =
           After we computed a fixed point, we give a unique region group
           identifier for each loop abstraction.
        *)
+  | Identity
+      (** An identity abstraction, which only consumes and provides shared
+          borrows/loans.
+
+          We introduce them to abstract the context a bit, for instance
+          to compute fixed-points.
+        *)
 [@@deriving show, ord]
 
 (** Ancestor for {!abs} iter visitor *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4fc68e1c..ec8fa39c 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -62,6 +62,29 @@ Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
   sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32)
 .
 
+(** [loops::clear] *)
+Definition clear_loop_fwd_back
+  (n : nat) (v : vec u32) (i : usize) : result (vec u32) :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    let i0 := vec_len u32 v in
+    if i s< i0
+    then (
+      i1 <- usize_add i 1%usize;
+      v0 <- vec_index_mut_back u32 v i (0%u32);
+      v1 <- clear_loop_fwd n0 v0 i1;
+      let _ := v1 in
+      Return v0)
+    else Return v
+  end
+.
+
+(** [loops::clear] *)
+Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) :=
+  v0 <- clear_loop_fwd n v (0%usize); let _ := v0 in Return v
+.
+
 (** [loops::List] *)
 Inductive List_t (T : Type) :=
 | ListCons : T -> List_t T -> List_t T
@@ -71,6 +94,25 @@ Inductive List_t (T : Type) :=
 Arguments ListCons {T} _ _.
 Arguments ListNil {T}.
 
+(** [loops::list_mem] *)
+Fixpoint list_mem_loop_fwd
+  (n : nat) (i : u32) (ls : List_t u32) : result bool :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons y tl =>
+      if y s= i then Return true else list_mem_loop_fwd n0 i tl
+    | ListNil => Return false
+    end
+  end
+.
+
+(** [loops::list_mem] *)
+Definition list_mem_fwd (n : nat) (x : u32) (ls : List_t u32) : result bool :=
+  list_mem_loop_fwd n x ls
+.
+
 (** [loops::list_nth_mut_loop] *)
 Fixpoint list_nth_mut_loop_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
@@ -144,6 +186,100 @@ Definition list_nth_shared_loop_fwd
   list_nth_shared_loop_loop_fwd T n ls i
 .
 
+(** [loops::id_mut] *)
+Definition id_mut_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
+  Return ls
+.
+
+(** [loops::id_mut] *)
+Definition id_mut_back
+  (T : Type) (ls : List_t T) (ret : List_t T) : result (List_t T) :=
+  Return ret
+.
+
+(** [loops::id_shared] *)
+Definition id_shared_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
+  Return ls
+.
+
+(** [loops::list_nth_mut_loop_with_id] *)
+Fixpoint list_nth_mut_loop_with_id_loop_fwd
+  (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return x
+      else (
+        i0 <- u32_sub i 1%u32; list_nth_mut_loop_with_id_loop_fwd T n0 i0 tl)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_loop_with_id] *)
+Definition list_nth_mut_loop_with_id_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  ls0 <- id_mut_fwd T ls; list_nth_mut_loop_with_id_loop_fwd T n i ls0
+.
+
+(** [loops::list_nth_mut_loop_with_id] *)
+Fixpoint list_nth_mut_loop_with_id_loop_back
+  (T : Type) (n : nat) (i : u32) (ls : List_t T) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return (ListCons ret tl)
+      else (
+        i0 <- u32_sub i 1%u32;
+        l <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
+        Return (ListCons x l))
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_loop_with_id] *)
+Definition list_nth_mut_loop_with_id_back
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  ls0 <- id_mut_fwd T ls;
+  l <- list_nth_mut_loop_with_id_loop_back T n i ls0 ret;
+  id_mut_back T ls l
+.
+
+(** [loops::list_nth_shared_loop_with_id] *)
+Fixpoint list_nth_shared_loop_with_id_loop_fwd
+  (T : Type) (n : nat) (l : List_t T) (i : u32) (ls : List_t T) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return x
+      else (
+        i0 <- u32_sub i 1%u32;
+        list_nth_shared_loop_with_id_loop_fwd T n0 l i0 tl)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_shared_loop_with_id] *)
+Definition list_nth_shared_loop_with_id_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  ls0 <- id_shared_fwd T ls; list_nth_shared_loop_with_id_loop_fwd T n ls i ls0
+.
+
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_fwd
   (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index cd29ca13..98d0a8ad 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -19,6 +19,12 @@ unfold
 let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
   admit ()
 
+(** [loops::clear]: decreases clause *)
+unfold let clear_decreases (v : vec u32) (i : usize) : nat = admit ()
+
+(** [loops::list_mem]: decreases clause *)
+unfold let list_mem_decreases (i : u32) (ls : list_t u32) : nat = admit ()
+
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
 let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
@@ -30,6 +36,18 @@ let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat
   =
   admit ()
 
+(** [loops::list_nth_mut_loop_with_id]: decreases clause *)
+unfold
+let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
+  nat =
+  admit ()
+
+(** [loops::list_nth_shared_loop_with_id]: decreases clause *)
+unfold
+let list_nth_shared_loop_with_id_decreases (t : Type0) (l : list_t t) 
+  (i : u32) (ls : list_t t) : nat =
+  admit ()
+
 (** [loops::list_nth_mut_loop_pair]: decreases clause *)
 unfold
 let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 9cf5db1f..e673d4ff 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -19,6 +19,14 @@ unfold
 let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
   if max >= i then max - i else 0
 
+(** [loops::clear]: decreases clause *)
+unfold let clear_decreases (v : vec u32) (i : usize) : nat =
+  if i <= List.Tot.length v then List.Tot.length v - i else 0
+
+(** [loops::list_mem]: decreases clause *)
+unfold let list_mem_decreases (i : u32) (ls : list_t u32) : list_t u32 =
+  ls
+
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
 let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
@@ -29,6 +37,18 @@ unfold
 let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
   ls
 
+(** [loops::list_nth_mut_loop_with_id]: decreases clause *)
+unfold
+let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
+  list_t t =
+  ls
+
+(** [loops::list_nth_shared_loop_with_id]: decreases clause *)
+unfold
+let list_nth_shared_loop_with_id_decreases (t : Type0) (l : list_t t)
+  (i : u32) (ls : list_t t) : list_t t =
+  ls
+
 (** [loops::list_nth_mut_loop_pair]: decreases clause *)
 unfold
 let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index ee8e95d2..d19e9328 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -69,6 +69,49 @@ let rec sum_with_shared_borrows_loop_fwd
 let sum_with_shared_borrows_fwd (max : u32) : result u32 =
   sum_with_shared_borrows_loop_fwd max 0 0
 
+(** [loops::clear] *)
+let clear_loop_fwd_back
+  (v : vec u32) (i : usize) :
+  Tot (result (vec u32)) (decreases (clear_decreases v i))
+  =
+  let i0 = vec_len u32 v in
+  if i < i0
+  then
+    begin match usize_add i 1 with
+    | Fail e -> Fail e
+    | Return i1 ->
+      begin match vec_index_mut_back u32 v i 0 with
+      | Fail e -> Fail e
+      | Return v0 ->
+        begin match clear_loop_fwd v0 i1 with
+        | Fail e -> Fail e
+        | Return _ -> Return v0
+        end
+      end
+    end
+  else Return v
+
+(** [loops::clear] *)
+let clear_fwd_back (v : vec u32) : result (vec u32) =
+  begin match clear_loop_fwd v 0 with
+  | Fail e -> Fail e
+  | Return _ -> Return v
+  end
+
+(** [loops::list_mem] *)
+let rec list_mem_loop_fwd
+  (i : u32) (ls : list_t u32) :
+  Tot (result bool) (decreases (list_mem_decreases i ls))
+  =
+  begin match ls with
+  | ListCons y tl -> if y = i then Return true else list_mem_loop_fwd i tl
+  | ListNil -> Return false
+  end
+
+(** [loops::list_mem] *)
+let list_mem_fwd (x : u32) (ls : list_t u32) : result bool =
+  list_mem_loop_fwd x ls
+
 (** [loops::list_nth_mut_loop] *)
 let rec list_nth_mut_loop_loop_fwd
   (t : Type0) (ls : list_t t) (i : u32) :
@@ -137,6 +180,101 @@ let rec list_nth_shared_loop_loop_fwd
 let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
   list_nth_shared_loop_loop_fwd t ls i
 
+(** [loops::id_mut] *)
+let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls
+
+(** [loops::id_mut] *)
+let id_mut_back
+  (t : Type0) (ls : list_t t) (ret : list_t t) : result (list_t t) =
+  Return ret
+
+(** [loops::id_shared] *)
+let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls
+
+(** [loops::list_nth_mut_loop_with_id] *)
+let rec list_nth_mut_loop_with_id_loop_fwd
+  (t : Type0) (i : u32) (ls : list_t t) :
+  Tot (result t) (decreases (list_nth_mut_loop_with_id_decreases t i ls))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return x
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 -> list_nth_mut_loop_with_id_loop_fwd t i0 tl
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_with_id] *)
+let list_nth_mut_loop_with_id_fwd
+  (t : Type0) (ls : list_t t) (i : u32) : result t =
+  begin match id_mut_fwd t ls with
+  | Fail e -> Fail e
+  | Return ls0 -> list_nth_mut_loop_with_id_loop_fwd t i ls0
+  end
+
+(** [loops::list_nth_mut_loop_with_id] *)
+let rec list_nth_mut_loop_with_id_loop_back
+  (t : Type0) (i : u32) (ls : list_t t) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (list_nth_mut_loop_with_id_decreases t i ls))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return (ListCons ret tl)
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 ->
+        begin match list_nth_mut_loop_with_id_loop_back t i0 tl ret with
+        | Fail e -> Fail e
+        | Return l -> Return (ListCons x l)
+        end
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop_with_id] *)
+let list_nth_mut_loop_with_id_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
+  begin match id_mut_fwd t ls with
+  | Fail e -> Fail e
+  | Return ls0 ->
+    begin match list_nth_mut_loop_with_id_loop_back t i ls0 ret with
+    | Fail e -> Fail e
+    | Return l -> id_mut_back t ls l
+    end
+  end
+
+(** [loops::list_nth_shared_loop_with_id] *)
+let rec list_nth_shared_loop_with_id_loop_fwd
+  (t : Type0) (l : list_t t) (i : u32) (ls : list_t t) :
+  Tot (result t) (decreases (list_nth_shared_loop_with_id_decreases t l i ls))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return x
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t l i0 tl
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_shared_loop_with_id] *)
+let list_nth_shared_loop_with_id_fwd
+  (t : Type0) (ls : list_t t) (i : u32) : result t =
+  begin match id_shared_fwd t ls with
+  | Fail e -> Fail e
+  | Return ls0 -> list_nth_shared_loop_with_id_loop_fwd t ls i ls0
+  end
+
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_fwd
   (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :