diff --git a/charon-pin b/charon-pin
index c1830e84..d7d09300 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-7744bf94275e2ba3e7a2e4163c1fa062225d7a75
+4f5cb493fd5e02976f51eb6aa636f615d7b96fcf
diff --git a/flake.lock b/flake.lock
index 3c32186b..8d16ce7d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1733313551,
-        "narHash": "sha256-CSaj6Cadz+S/qmiLtoQMWfm3mHSE2cCx3UUxt5JmoAM=",
+        "lastModified": 1733487112,
+        "narHash": "sha256-E1pqGoFWvOx01fD3uEKf1ynpGD78tmgkb1NtdL+kkSA=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "7744bf94275e2ba3e7a2e4163c1fa062225d7a75",
+        "rev": "4f5cb493fd5e02976f51eb6aa636f615d7b96fcf",
         "type": "github"
       },
       "original": {
@@ -177,11 +177,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1733279627,
-        "narHash": "sha256-NCNDAGPkdFdu+DLErbmNbavmVW9AwkgP7azROFFSB0U=",
+        "lastModified": 1733452419,
+        "narHash": "sha256-eh2i2GtqdWVOP7yjiWtB8FMUWktCZ4vjo81n6g5mSiE=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "4da5a80ef76039e80468c902f1e9f5c0eab87d96",
+        "rev": "020701e6057992329a7cfafc6e3c5d5658bbcf79",
         "type": "github"
       },
       "original": {
diff --git a/src/interp/InterpreterBorrows.ml b/src/interp/InterpreterBorrows.ml
index 3b0e6fa4..bcffdb03 100644
--- a/src/interp/InterpreterBorrows.ml
+++ b/src/interp/InterpreterBorrows.ml
@@ -1813,7 +1813,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                 let ty =
                   (* Take the first region of the abstraction - this doesn't really matter *)
                   let r = RegionId.Set.min_elt abs0.regions in
-                  TRef (RFVar r, ty, RShared)
+                  TRef (RVar (Free r), ty, RShared)
                 in
                 { value; ty }
               in
@@ -1935,7 +1935,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
         | VSharedBorrow bid ->
             cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span
               "Nested borrows are not supported yet";
-            let ty = TRef (RFVar r_id, ref_ty, kind) in
+            let ty = TRef (RVar (Free r_id), ref_ty, kind) in
             let value = ABorrow (ASharedBorrow (PNone, bid)) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
@@ -1945,7 +1945,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
               (not (value_has_borrows (Some span) ctx bv.value))
               span "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
-            let ty = TRef (RFVar r_id, ref_ty, kind) in
+            let ty = TRef (RVar (Free r_id), ref_ty, kind) in
             let ignored = mk_aignored span ref_ty None in
             let av = ABorrow (AMutBorrow (PNone, bid, ignored)) in
             let av = { value = av; ty } in
@@ -1971,7 +1971,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* We use [AIgnore] for the inner value *)
             let ignored = mk_aignored span ty None in
             (* For avalues, a loan has the type borrow (see the comments in [avalue]) *)
-            let ty = mk_ref_ty (RFVar r_id) ty RShared in
+            let ty = mk_ref_ty (RVar (Free r_id)) ty RShared in
             (* Rem.: the shared value might contain loans *)
             let avl, sv = to_avalues false true true r_id sv in
             let av = ALoan (ASharedLoan (PNone, bids, sv, ignored)) in
@@ -1991,7 +1991,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* We use [AIgnore] for the inner value *)
             let ignored = mk_aignored span ty in
             (* For avalues, a loan has the type borrow (see the comments in [avalue]) *)
-            let ty = mk_ref_ty (RFVar r_id) ty RMut in
+            let ty = mk_ref_ty (RVar (Free r_id)) ty RMut in
             let av = ALoan (AMutLoan (PNone, bid, ignored None)) in
             let av = { value = av; ty } in
             ([ av ], v))
diff --git a/src/interp/InterpreterLoopsFixedPoint.ml b/src/interp/InterpreterLoopsFixedPoint.ml
index e7c666a9..ab6f4760 100644
--- a/src/interp/InterpreterLoopsFixedPoint.ml
+++ b/src/interp/InterpreterLoopsFixedPoint.ml
@@ -231,7 +231,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     let child_av = mk_aignored span child_rty None in
 
     (* Create the shared loan *)
-    let loan_rty = TRef (RFVar nrid, rty, RShared) in
+    let loan_rty = TRef (RVar (Free nrid), rty, RShared) in
     let loan_value =
       ALoan (ASharedLoan (PNone, BorrowId.Set.singleton nlid, nsv, child_av))
     in
diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml
index 89ff3ad2..998c26fa 100644
--- a/src/interp/InterpreterLoopsMatchCtxs.ml
+++ b/src/interp/InterpreterLoopsMatchCtxs.ml
@@ -520,7 +520,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
       (* Update the type of the shared loan to use the fresh region *)
       let _, bv_ty, kind = ty_as_ref ty in
-      let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
+      let borrow_ty = mk_ref_ty (RVar (Free rid)) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (pm : proj_marker) (bid : borrow_id) : typed_avalue =
@@ -633,7 +633,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
         let bv_ty = bv.ty in
         cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span
           "Nested borrows are not supported yet";
-        let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
+        let borrow_ty = mk_ref_ty (RVar (Free rid)) bv_ty kind in
 
         let borrow_av =
           let ty = borrow_ty in
@@ -685,7 +685,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       let _, bv_ty, kind = ty_as_ref ty in
       let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty span bv_ty in
 
-      let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
+      let borrow_ty = mk_ref_ty (RVar (Free rid)) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (pm : proj_marker) (bid : borrow_id) (bv : typed_value) :
@@ -1110,9 +1110,9 @@ struct
     let match_regions r0 r1 =
       match (r0, r1) with
       | RStatic, RStatic -> r1
-      | RFVar rid0, RFVar rid1 ->
+      | RVar (Free rid0), RVar (Free rid1) ->
           let rid = match_rid rid0 rid1 in
-          RFVar rid
+          RVar (Free rid)
       | _ -> raise (Distinct "match_rtys")
     in
     match_types span ctx0 ctx1 match_distinct_types match_regions ty0 ty1
diff --git a/src/llbc/AssociatedTypes.ml b/src/llbc/AssociatedTypes.ml
index 1d5eebf7..f7a4c280 100644
--- a/src/llbc/AssociatedTypes.ml
+++ b/src/llbc/AssociatedTypes.ml
@@ -221,13 +221,14 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
   | TRawPtr (ty, rkind) ->
       let ty = norm_ctx_normalize_ty ctx ty in
       TRawPtr (ty, rkind)
-  | TArrow (regions, inputs, output) ->
+  | TArrow binder ->
       (* TODO: for now it works because we don't support predicates with
          bound regions. If we do support them, we probably need to do
          something smarter here. *)
+      let { binder_regions; binder_value = inputs, output } = binder in
       let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in
       let output = norm_ctx_normalize_ty ctx output in
-      TArrow (regions, inputs, output)
+      TArrow { binder_regions; binder_value = (inputs, output) }
   | TTraitType (trait_ref, type_name) -> (
       log#ldebug
         (lazy
@@ -512,7 +513,7 @@ let ctx_adt_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
 (** Same as [substitute_signature] but normalizes the types *)
 let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
     (asubst : RegionGroupId.id -> AbstractionId.id)
-    (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (r_subst : BoundRegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
     (cg_subst : ConstGenericVarId.id -> const_generic)
     (tr_subst : TraitClauseId.id -> trait_instance_id)
     (tr_self : trait_instance_id) (sg : fun_sig)
diff --git a/src/llbc/Builtin.ml b/src/llbc/Builtin.ml
index 19e9c9f2..1727f123 100644
--- a/src/llbc/Builtin.ml
+++ b/src/llbc/Builtin.ml
@@ -36,8 +36,8 @@ open LlbcAst
 module Sig = struct
   (** A few utilities *)
 
-  let rvar_id_0 = RegionVarId.of_int 0
-  let rvar_0 : region = RBVar (0, rvar_id_0)
+  let rvar_id_0 = BoundRegionId.of_int 0
+  let rvar_0 : region = RVar (zero_db_var rvar_id_0)
   let rg_id_0 = RegionGroupId.of_int 0
   let tvar_id_0 = TypeVarId.of_int 0
   let tvar_0 : ty = TVar tvar_id_0
diff --git a/src/llbc/RegionsHierarchy.ml b/src/llbc/RegionsHierarchy.ml
index 6b29a6bf..120c882a 100644
--- a/src/llbc/RegionsHierarchy.ml
+++ b/src/llbc/RegionsHierarchy.ml
@@ -88,11 +88,11 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
     Subst.fresh_regions_with_substs_from_vars sg.generics.regions
       (snd (RegionId.fresh_stateful_generator ()))
   in
-  let region_id_to_var_map : RegionVarId.id RegionId.Map.t =
+  let region_id_to_var_map : BoundRegionId.id RegionId.Map.t =
     RegionId.Map.of_list
       (List.map
          (fun (var_id, id) -> (id, var_id))
-         (RegionVarId.Map.bindings region_var_to_id_map))
+         (BoundRegionId.Map.bindings region_var_to_id_map))
   in
   let subst = { Subst.empty_subst with r_subst = bound_regions_subst } in
   let g : RegionSet.t RegionMap.t ref =
@@ -100,7 +100,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
     let m =
       List.map
         (fun (r : region_var) ->
-          (RFVar (bound_regions_id_subst r.index), s_set))
+          (RVar (Free (bound_regions_id_subst r.index)), s_set))
         sg.generics.regions
     in
     let s = (RStatic, RegionSet.empty) in
@@ -113,7 +113,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
     sanity_check_opt_span __FILE__ __LINE__ (long <> RErased) span;
     (* Ignore the locally bound regions (at the level of arrow types for instance *)
     match (short, long) with
-    | RBVar _, _ | _, RBVar _ -> ()
+    | RVar (Bound _), _ | _, RVar (Bound _) -> ()
     | _, _ ->
         let m = !g in
         let s = RegionMap.find short !g in
@@ -196,11 +196,13 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
           span;
         (* We have nothing to do *)
         ()
-    | TArrow (regions, inputs, output) ->
+    | TArrow binder ->
         (* TODO: *)
-        cassert_opt_span __FILE__ __LINE__ (regions = []) span
-          "We don't support arrow types with locally quantified regions";
+        cassert_opt_span __FILE__ __LINE__
+          (binder.binder_regions = [])
+          span "We don't support arrow types with locally quantified regions";
         (* We can ignore the outer regions *)
+        let inputs, output = binder.binder_value in
         List.iter (explore_ty []) (output :: inputs)
     | TDynTrait _ ->
         craise_opt_span __FILE__ __LINE__ span
@@ -296,11 +298,11 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
       let id = RegionGroupId.of_int i in
 
       (* Retrieve the set of regions in the group *)
-      let regions : RegionVarId.id list =
+      let regions : BoundRegionId.id list =
         List.map
           (fun r ->
             match r with
-            | RFVar rid -> RegionId.Map.find rid region_id_to_var_map
+            | RVar (Free rid) -> RegionId.Map.find rid region_id_to_var_map
             | _ -> craise __FILE__ __LINE__ (Option.get span) "Unreachable")
           scc
       in
diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml
index 5b48096d..103f285a 100644
--- a/src/llbc/Substitute.ml
+++ b/src/llbc/Substitute.ml
@@ -10,41 +10,43 @@ open ContextsBase
 open Errors
 
 (** Substitute regions at the binding level where we start to substitute *)
-let make_region_subst_from_fn (subst : RegionVarId.id -> region) :
-    region -> region = function
+let make_region_subst_from_fn (subst : BoundRegionId.id -> region) :
+    de_bruijn_var -> region = function
   (* The DeBruijn index is kept correct wrt the start of the substituttion *)
-  | RBVar (bdid, rid) when bdid = 0 -> subst rid
-  | r -> r
+  | Bound (bdid, rid) when bdid = 0 -> subst rid
+  | r -> RVar r
 
 (** Generate fresh regions for region variables.
 
     Return the list of new regions and appropriate substitutions from the
     original region variables to the fresh regions.
     
-    TODO: simplify? we only need the subst [RegionVarId.id -> RegionId.id]
+    TODO: simplify? we only need the subst [BoundRegionId.id -> RegionId.id]
   *)
-let fresh_regions_with_substs (region_vars : RegionVarId.id list)
+let fresh_regions_with_substs (region_vars : BoundRegionId.id list)
     (fresh_region_id : unit -> region_id) :
-    RegionId.id RegionVarId.Map.t
-    * (RegionVarId.id -> RegionId.id)
-    * (region -> region) =
+    RegionId.id BoundRegionId.Map.t
+    * (BoundRegionId.id -> RegionId.id)
+    * (de_bruijn_var -> region) =
   (* Map each region var id to a fresh region *)
   let rid_map =
-    RegionVarId.Map.of_list
+    BoundRegionId.Map.of_list
       (List.map (fun var -> (var, fresh_region_id ())) region_vars)
   in
   (* Generate the substitution from region var id to region *)
-  let rid_subst id = RegionVarId.Map.find id rid_map in
+  let rid_subst id = BoundRegionId.Map.find id rid_map in
   (* Generate the substitution from region to region *)
-  let r_subst = make_region_subst_from_fn (fun id -> RFVar (rid_subst id)) in
+  let r_subst =
+    make_region_subst_from_fn (fun id -> RVar (Free (rid_subst id)))
+  in
   (* Return *)
   (rid_map, rid_subst, r_subst)
 
 let fresh_regions_with_substs_from_vars (region_vars : region_var list)
     (fresh_region_id : unit -> region_id) :
-    RegionId.id RegionVarId.Map.t
-    * (RegionVarId.id -> RegionId.id)
-    * (region -> region) =
+    RegionId.id BoundRegionId.Map.t
+    * (BoundRegionId.id -> RegionId.id)
+    * (de_bruijn_var -> region) =
   fresh_regions_with_substs
     (List.map (fun (r : region_var) -> r.index) region_vars)
     fresh_region_id
@@ -55,12 +57,14 @@ let fresh_regions_with_substs_from_vars (region_vars : region_var list)
     **IMPORTANT:** this function doesn't normalize the types.
  *)
 let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
-    (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (r_subst : BoundRegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
     (cg_subst : ConstGenericVarId.id -> const_generic)
     (tr_subst : TraitClauseId.id -> trait_instance_id)
     (tr_self : trait_instance_id) (sg : fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
-  let r_subst' = make_region_subst_from_fn (fun id -> RFVar (r_subst id)) in
+  let r_subst' =
+    make_region_subst_from_fn (fun id -> RVar (Free (r_subst id)))
+  in
   let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
   let inputs = List.map (ty_substitute subst) sg.inputs in
   let output = ty_substitute subst sg.output in
diff --git a/src/llbc/Types.ml b/src/llbc/Types.ml
index c76b6ffa..551c5536 100644
--- a/src/llbc/Types.ml
+++ b/src/llbc/Types.ml
@@ -1 +1,6 @@
 include Charon.Types
+module RegionId = FreeRegionId
+
+type bound_region_id = BoundRegionId.id [@@deriving show, ord]
+type region_id = RegionId.id [@@deriving show, ord]
+type region_id_set = RegionId.Set.t [@@deriving show, ord]
diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml
index 53e40051..730ddc2f 100644
--- a/src/llbc/TypesAnalysis.ml
+++ b/src/llbc/TypesAnalysis.ml
@@ -35,7 +35,7 @@ type 'p g_type_info = {
       (** If true, it means the type is a record that we should extract as a tuple.
           This field is only valid for type declarations.
       *)
-  mut_regions : RegionVarId.Set.t;
+  mut_regions : BoundRegionId.Set.t;
       (** The set of regions used in mutable borrows *)
 }
 [@@deriving show]
@@ -83,7 +83,7 @@ let initialize_g_type_info (is_tuple_struct : bool) (param_infos : 'p) :
     borrows_info = type_borrows_info_init;
     is_tuple_struct;
     param_infos;
-    mut_regions = RegionVarId.Set.empty;
+    mut_regions = BoundRegionId.Set.empty;
   }
 
 let initialize_type_decl_info (is_rec : bool) (def : type_decl) : type_decl_info
@@ -138,18 +138,18 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
   in
   let r_is_static (r : region) : bool = r = RStatic in
   let update_mut_regions_with_rid mut_regions rid =
-    let rid = RegionVarId.of_int (RegionId.to_int rid) in
-    if RegionVarId.Set.mem rid mut_regions then ty_info.mut_regions
+    let rid = BoundRegionId.of_int (RegionId.to_int rid) in
+    if BoundRegionId.Set.mem rid mut_regions then ty_info.mut_regions
     else (
       updated := true;
-      RegionVarId.Set.add rid mut_regions)
+      BoundRegionId.Set.add rid mut_regions)
   in
   let update_mut_regions mut_regions mut_region =
     match mut_region with
-    | RStatic | RBVar _ ->
+    | RStatic | RVar (Bound _) ->
         mut_regions (* We can have bound vars because of arrows *)
     | RErased -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
-    | RFVar rid -> update_mut_regions_with_rid mut_regions rid
+    | RVar (Free rid) -> update_mut_regions_with_rid mut_regions rid
   in
 
   (* Update a partial_type_info, while registering if we actually performed an update *)
@@ -336,19 +336,22 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
             (fun mut_regions (adt_rid, r) ->
               (* Check if the region is a variable and is used for mutable borrows *)
               match r with
-              | RStatic | RBVar _ | RErased -> mut_regions
+              | RStatic | RVar (Bound _) | RErased -> mut_regions
               (* We can have bound vars because of arrows, and erased regions
                  when analyzing types appearing in function bodies *)
-              | RFVar rid ->
-                  if RegionVarId.Set.mem adt_rid adt_info.mut_regions then
+              | RVar (Free rid) ->
+                  if BoundRegionId.Set.mem adt_rid adt_info.mut_regions then
                     update_mut_regions_with_rid mut_regions rid
                   else mut_regions)
             ty_info.mut_regions
-            (RegionVarId.mapi (fun adt_rid r -> (adt_rid, r)) generics.regions)
+            (BoundRegionId.mapi
+               (fun adt_rid r -> (adt_rid, r))
+               generics.regions)
         in
         (* Return *)
         { ty_info with mut_regions }
-    | TArrow (_regions, inputs, output) ->
+    | TArrow binder ->
+        let inputs, output = binder.binder_value in
         (* Just dive into the arrow *)
         let ty_info =
           List.fold_left
diff --git a/src/llbc/TypesUtils.ml b/src/llbc/TypesUtils.ml
index fcce64fd..5560d2b5 100644
--- a/src/llbc/TypesUtils.ml
+++ b/src/llbc/TypesUtils.ml
@@ -90,10 +90,10 @@ let ty_has_mut_borrow_for_region_in_pred (infos : TypesAnalysis.type_infos)
           | TTuple | TBuiltin (TBox | TArray | TSlice | TStr) -> ()
           | TAdtId adt_id ->
               let info = TypeDeclId.Map.find adt_id infos in
-              RegionVarId.iteri
+              BoundRegionId.iteri
                 (fun adt_rid r ->
-                  if RegionVarId.Set.mem adt_rid info.mut_regions && pred r then
-                    raise Found
+                  if BoundRegionId.Set.mem adt_rid info.mut_regions && pred r
+                  then raise Found
                   else ())
                 generics.regions
         end;
@@ -112,8 +112,8 @@ let raise_if_not_rty_visitor =
 
     method! visit_region _ r =
       match r with
-      | RBVar _ | RErased -> raise Found
-      | RStatic | RFVar _ -> ()
+      | RVar (Bound _) | RErased -> raise Found
+      | RStatic | RVar (Free _) -> ()
   end
 
 (** Return [true] if the type is a region type (i.e., it doesn't contain erased
@@ -131,7 +131,7 @@ let raise_if_not_erased_ty_visitor =
 
     method! visit_region _ r =
       match r with
-      | RStatic | RBVar _ | RFVar _ -> raise Found
+      | RStatic | RVar _ -> raise Found
       | RErased -> ()
   end
 
diff --git a/src/llbc/Values.ml b/src/llbc/Values.ml
index b9522f01..da6119b5 100644
--- a/src/llbc/Values.ml
+++ b/src/llbc/Values.ml
@@ -25,6 +25,11 @@ class ['self] iter_typed_value_base =
   object (self : 'self)
     inherit [_] iter_ty
 
+    (** Rename the charon name for consistency *)
+    method! visit_free_region_id env id = self#visit_region_id env id
+
+    method visit_region_id _ _ = ()
+
     method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit =
       fun _ _ -> ()
 
@@ -44,6 +49,11 @@ class ['self] map_typed_value_base =
   object (self : 'self)
     inherit [_] map_ty
 
+    (** Rename the charon name for consistency *)
+    method! visit_free_region_id env id = self#visit_region_id env id
+
+    method visit_region_id _ id = id
+
     method visit_symbolic_value_id
         : 'env -> symbolic_value_id -> symbolic_value_id =
       fun _ x -> x
@@ -171,8 +181,6 @@ type mvalue = typed_value [@@deriving show, ord]
  *)
 type msymbolic_value = symbolic_value [@@deriving show, ord]
 
-type region_id = RegionId.id [@@deriving show, ord]
-type region_id_set = RegionId.Set.t [@@deriving show, ord]
 type abstraction_id = AbstractionId.id [@@deriving show, ord]
 type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord]
 
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index 574a2ed6..56cd184c 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -1170,9 +1170,9 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed
       | T.RStatic -> craise_opt_span __FILE__ __LINE__ span "Unimplemented"
       | RErased ->
           craise_opt_span __FILE__ __LINE__ span "Unexpected erased region"
-      | RBVar _ ->
+      | RVar (Bound _) ->
           craise_opt_span __FILE__ __LINE__ span "Unexpected bound region"
-      | RFVar rid -> T.RegionId.Set.mem rid gr_regions
+      | RVar (Free rid) -> T.RegionId.Set.mem rid gr_regions
     in
     let inside_mut = false in
     translate_back_ty span type_infos keep_region inside_mut ty
@@ -1624,7 +1624,7 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
         let rg = RegionGroupId.nth regions_hierarchy gid in
         let region_names =
           List.map
-            (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name)
+            (fun rid -> (T.BoundRegionId.nth sg.generics.regions rid).name)
             rg.regions
         in
         let name =
@@ -3920,7 +3920,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         List.map
           (fun (c : trait_clause) ->
             let trait_decl_ref =
-              { trait_decl_id = c.trait_id; decl_generics = empty_generic_args }
+              { trait_decl_id = c.trait_id; decl_generics = c.generics }
             in
             { trait_id = Clause c.clause_id; trait_decl_ref })
           trait_clauses
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index f503d93a..35d2c395 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -76,13 +76,12 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
 
   (* Build the command *)
   let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in
-  (* If we target a specific backend and the test is known to fail, we abort
-     on error so as not to generate any files *)
+  (* Abort on error to help debugging, except for borrow-check failure cases
+     where that would be too noisy. *)
   let abort_on_error =
     match action with
-    | Skip | Normal -> []
-    | KnownFailure ->
-        if backend = Backend.BorrowCheck then [] else [ "-abort-on-error" ]
+    | KnownFailure when backend = Backend.BorrowCheck -> []
+    | _ -> [ "-abort-on-error" ]
   in
   let args = List.concat [ args; aeneas_options; abort_on_error ] in
   let cmd = Command.make args in