diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml
index 1a7a7c796..dd84d6e02 100644
--- a/charon-ml/src/CharonVersion.ml
+++ b/charon-ml/src/CharonVersion.ml
@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.32"
+let supported_charon_version = "0.1.33"
diff --git a/charon-ml/src/Expressions.ml b/charon-ml/src/Expressions.ml
index d5a505a7e..6d118f733 100644
--- a/charon-ml/src/Expressions.ml
+++ b/charon-ml/src/Expressions.ml
@@ -20,30 +20,11 @@ module FunDeclId = Types.FunDeclId
   *)
 type var_id = VarId.id [@@deriving show, ord]
 
-(** An assumed function identifier, identifying a function coming from a
+(** An built-in function identifier, identifying a function coming from a
     standard library.
  *)
 type assumed_fun_id =
   | BoxNew  (** `alloc::boxed::Box::new` *)
-  | BoxFree
-      (** `alloc::alloc::box_free`
-          This is actually an unsafe function, but the rust compiler sometimes
-          introduces it when going to MIR.
-
-          Also, in practice, deallocation is performed as follows in MIR:
-          ```text
-          alloc::alloc::box_free::<T, std::alloc::Global>(
-              move (b.0: std::ptr::Unique<T>),
-              move (b.1: std::alloc::Global))
-          ```
-          When translating from MIR to ULLBC, we do as if the MIR was actually the
-          following (this is hardcoded - see [crate::register] and [crate::translate_functions_to_ullbc]):
-          ```text
-          alloc::alloc::box_free::<T>(move b)
-          ```
-
-          Also see the comments in [crate::assumed::type_to_used_params].
-       *)
   | ArrayIndexShared
       (** Converted from [ProjectionElem::Index].
 
@@ -421,7 +402,7 @@ type operand =
 and aggregate_kind =
   | AggregatedAdt of type_id * variant_id option * generic_args
   | AggregatedArray of ty * const_generic
-      (** We don't put this with the ADT cas because this is the only assumed type
+      (** We don't put this with the ADT cas because this is the only built-in type
           with aggregates, and it is a primitive type. In particular, it makes
           sense to treat it differently because it has a variable number of fields.
        *)
diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
index e22d5ff18..d5e917181 100644
--- a/charon-ml/src/GAstOfJson.ml
+++ b/charon-ml/src/GAstOfJson.ml
@@ -361,9 +361,9 @@ and type_id_of_json (js : json) : (type_id, string) result =
         let* adt = type_decl_id_of_json adt in
         Ok (TAdtId adt)
     | `String "Tuple" -> Ok TTuple
-    | `Assoc [ ("Assumed", assumed) ] ->
-        let* assumed = assumed_ty_of_json assumed in
-        Ok (TAssumed assumed)
+    | `Assoc [ ("Builtin", builtin) ] ->
+        let* builtin = assumed_ty_of_json builtin in
+        Ok (TAssumed builtin)
     | _ -> Error "")
 
 and const_generic_of_json (js : json) : (const_generic, string) result =
@@ -915,7 +915,6 @@ and assumed_fun_id_of_json (js : json) : (assumed_fun_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `String "BoxNew" -> Ok BoxNew
-    | `String "BoxFree" -> Ok BoxFree
     | `String "ArrayIndexShared" -> Ok ArrayIndexShared
     | `String "ArrayIndexMut" -> Ok ArrayIndexMut
     | `String "ArrayToSliceShared" -> Ok ArrayToSliceShared
@@ -931,9 +930,9 @@ and fun_id_of_json (js : json) : (fun_id, string) result =
     | `Assoc [ ("Regular", regular) ] ->
         let* regular = fun_decl_id_of_json regular in
         Ok (FRegular regular)
-    | `Assoc [ ("Assumed", assumed) ] ->
-        let* assumed = assumed_fun_id_of_json assumed in
-        Ok (FAssumed assumed)
+    | `Assoc [ ("Builtin", builtin) ] ->
+        let* builtin = assumed_fun_id_of_json builtin in
+        Ok (FAssumed builtin)
     | _ -> Error "")
 
 and fun_id_or_trait_method_ref_of_json (js : json) :
diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml
index 77c2ca3d0..2d5ca0f7c 100644
--- a/charon-ml/src/NameMatcher.ml
+++ b/charon-ml/src/NameMatcher.ml
@@ -612,7 +612,6 @@ and match_expr_with_const_generic (ctx : ctx) (c : match_config) (m : maps)
 let assumed_fun_id_to_string (fid : E.assumed_fun_id) : string =
   match fid with
   | BoxNew -> "alloc::boxed::{Box<@T, alloc::alloc::Global>}::new"
-  | BoxFree -> "alloc::alloc::box_free"
   | ArrayIndexShared -> "ArrayIndexShared"
   | ArrayIndexMut -> "ArrayIndexMut"
   | ArrayToSliceShared -> "ArrayToSliceShared"
@@ -655,9 +654,6 @@ let match_fn_ptr (ctx : ctx) (c : match_config) (p : pattern) (func : E.fn_ptr)
                   true
               | _ -> false)
           | _ -> false)
-      | BoxFree ->
-          let name = to_name [ "alloc"; "alloc"; "box_free" ] in
-          match_name_with_generics ctx c p name func.generics
       | _ ->
           let name = assumed_fun_id_to_string fid in
           match_name_with_generics ctx c p (to_name [ name ]) func.generics)
@@ -998,12 +994,6 @@ let fn_ptr_to_pattern (ctx : ctx) (c : to_pat_config)
               PImpl (EComp box_impl);
               PIdent ("new", args);
             ]
-        | BoxFree ->
-            [
-              PIdent ("alloc", []);
-              PIdent ("alloc", []);
-              PIdent ("box_free", args);
-            ]
         | _ ->
             let fid = assumed_fun_id_to_string fid in
             [ PIdent (fid, args) ])
diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml
index 36228d63c..aa8bfc47d 100644
--- a/charon-ml/src/PrintExpressions.ml
+++ b/charon-ml/src/PrintExpressions.ml
@@ -100,7 +100,6 @@ let binop_to_string (binop : binop) : string =
 let assumed_fun_id_to_string (aid : assumed_fun_id) : string =
   match aid with
   | BoxNew -> "alloc::boxed::Box::new"
-  | BoxFree -> "alloc::alloc::box_free"
   | ArrayIndexShared -> "@ArrayIndexShared"
   | ArrayIndexMut -> "@ArrayIndexMut"
   | ArrayToSliceShared -> "@ArrayToSliceShared"
diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml
index dd0420c7e..77ee5830e 100644
--- a/charon-ml/src/Types.ml
+++ b/charon-ml/src/Types.ml
@@ -283,16 +283,16 @@ class virtual ['self] map_ty_base =
         { index; name }
   end
 
-(** Assumed types identifiers.
+(** Builtin types identifiers.
 
-    WARNING: for now, all the assumed types are covariant in the generic
+    WARNING: for now, all the built-in types are covariant in the generic
     parameters (if there are). Adding types which don't satisfy this
     will require to update the code abstracting the signatures (to properly
     take into account the lifetime constraints).
 
     TODO: update to not hardcode the types (except `Box` maybe) and be more
     modular.
-    TODO: move to assumed.rs?
+    TODO: move to builtins.rs?
  *)
 type assumed_ty =
   | TBox  (** Boxes are de facto a primitive type. *)
@@ -302,7 +302,7 @@ type assumed_ty =
 
 (** Type identifier.
 
-    Allows us to factorize the code for assumed types, adts and tuples
+    Allows us to factorize the code for built-in types, adts and tuples
  *)
 and type_id =
   | TAdtId of type_decl_id
@@ -313,12 +313,12 @@ and type_id =
        *)
   | TTuple
   | TAssumed of assumed_ty
-      (** Assumed type. Either a primitive type like array or slice, or a
+      (** Built-in type. Either a primitive type like array or slice, or a
           non-primitive type coming from a standard library
           and that we handle like a primitive type. Types falling into this
           category include: Box, Vec, Cell...
           The Array and Slice types were initially modelled as primitive in
-          the [Ty] type. We decided to move them to assumed types as it allows
+          the [Ty] type. We decided to move them to built-in types as it allows
           for more uniform treatment throughout the codebase.
        *)
 
@@ -335,7 +335,7 @@ and ty =
           Note that here ADTs are very general. They can be:
           - user-defined ADTs
           - tuples (including `unit`, which is a 0-tuple)
-          - assumed types (includes some primitive types, e.g., arrays or slices)
+          - built-in types (includes some primitive types, e.g., arrays or slices)
           The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
           The last list is used encode const generics, e.g., the size of an array
 
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 7a9f8c115..567db60a5 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -173,7 +173,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.32"
+version = "0.1.33"
 dependencies = [
  "anyhow",
  "assert_cmd",
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
index 6b596b815..6c83e4734 100644
--- a/charon/Cargo.toml
+++ b/charon/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.32"
+version = "0.1.33"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"
diff --git a/charon/src/ast/assumed.rs b/charon/src/ast/builtins.rs
similarity index 54%
rename from charon/src/ast/assumed.rs
rename to charon/src/ast/builtins.rs
index 59dc14d60..b675420e8 100644
--- a/charon/src/ast/assumed.rs
+++ b/charon/src/ast/builtins.rs
@@ -1,4 +1,4 @@
-//! This file contains information about the assumed functions/types/traits definitions
+//! This file contains information about the builtin functions/types/traits definitions
 //!
 //! **IMPORTANT**:
 //! When checking whether names are equal to one of the reference names below,
@@ -14,7 +14,7 @@ use macros::EnumIsA;
 // We treat this one specially in the `inline_local_panic_functions` pass. See there for details.
 pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit"];
 
-/// We redefine identifiers for assumed functions here, instead of reusing the
+/// We redefine identifiers for built-in functions here, instead of reusing the
 /// identifiers from [ullbc_ast], because:
 /// - some of the functions (the panic functions) will actually not be translated
 ///   to functions: there are thus missing identifiers.
@@ -24,63 +24,42 @@ pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit
 pub enum BuiltinFun {
     Panic,
     BoxNew,
-    BoxFree,
-}
-
-pub struct FunInfo {
-    pub used_type_params: Vec<bool>,
-    // TODO: rename. "value_args"?
-    pub used_args: Vec<bool>,
 }
 
 impl BuiltinFun {
     /// Converts to the ullbc equivalent. Panics if `self` is `Panic` as this should be handled
     /// separately.
-    pub fn to_ullbc_builtin_fun(self) -> ast::AssumedFunId {
+    pub fn to_ullbc_builtin_fun(self) -> ast::BuiltinFunId {
         match self {
-            BuiltinFun::BoxNew => ast::AssumedFunId::BoxNew,
-            BuiltinFun::BoxFree => ast::AssumedFunId::BoxFree,
+            BuiltinFun::BoxNew => ast::BuiltinFunId::BoxNew,
             BuiltinFun::Panic => panic!(),
         }
     }
-
-    /// See the comments for [type_to_used_params]
-    pub fn to_fun_info(self) -> Option<FunInfo> {
-        match self {
-            BuiltinFun::Panic => None,
-            BuiltinFun::BoxNew => None,
-            BuiltinFun::BoxFree => Some(FunInfo {
-                used_type_params: vec![true, false],
-                used_args: vec![true, false],
-            }),
-        }
-    }
 }
 
-impl AssumedTy {
+impl BuiltinTy {
     pub fn get_name(self) -> Name {
         let name: &[_] = match self {
-            AssumedTy::Box => &["alloc", "boxed", "Box"],
-            AssumedTy::Str => &["Str"],
-            AssumedTy::Array => &["Array"],
-            AssumedTy::Slice => &["Slice"],
+            BuiltinTy::Box => &["alloc", "boxed", "Box"],
+            BuiltinTy::Str => &["Str"],
+            BuiltinTy::Array => &["Array"],
+            BuiltinTy::Slice => &["Slice"],
         };
         Name::from_path(name)
     }
 }
 
-/// When translating from MIR to ULLBC, we ignore some type parameters for some
-/// assumed types.
+/// When translating from MIR to ULLBC, we ignore some type parameters for some builtin types.
 /// For instance, many types like box or vec are parameterized (in MIR) by an allocator
 /// (`std::alloc::Allocator`): we ignore it.
-pub fn type_to_used_params(id: AssumedTy) -> Vec<bool> {
+pub fn type_to_used_params(id: BuiltinTy) -> Vec<bool> {
     match id {
-        AssumedTy::Box => {
+        BuiltinTy::Box => {
             vec![true, false]
         }
-        AssumedTy::Str => {
+        BuiltinTy::Str => {
             vec![]
         }
-        AssumedTy::Array | AssumedTy::Slice => vec![true],
+        BuiltinTy::Array | BuiltinTy::Slice => vec![true],
     }
 }
diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs
index e4fe1a7b3..389a41fec 100644
--- a/charon/src/ast/expressions.rs
+++ b/charon/src/ast/expressions.rs
@@ -268,10 +268,11 @@ pub enum FunId {
     /// A primitive function, coming from a standard library (for instance:
     /// `alloc::boxed::Box::new`).
     /// TODO: rename to "Primitive"
-    Assumed(AssumedFunId),
+    #[charon::rename("FAssumed")]
+    Builtin(BuiltinFunId),
 }
 
-/// An assumed function identifier, identifying a function coming from a
+/// An built-in function identifier, identifying a function coming from a
 /// standard library.
 #[derive(
     Debug,
@@ -287,27 +288,10 @@ pub enum FunId {
     Drive,
     DriveMut,
 )]
-pub enum AssumedFunId {
+#[charon::rename("AssumedFunId")]
+pub enum BuiltinFunId {
     /// `alloc::boxed::Box::new`
     BoxNew,
-    /// `alloc::alloc::box_free`
-    /// This is actually an unsafe function, but the rust compiler sometimes
-    /// introduces it when going to MIR.
-    ///
-    /// Also, in practice, deallocation is performed as follows in MIR:
-    /// ```text
-    /// alloc::alloc::box_free::<T, std::alloc::Global>(
-    ///     move (b.0: std::ptr::Unique<T>),
-    ///     move (b.1: std::alloc::Global))
-    /// ```
-    /// When translating from MIR to ULLBC, we do as if the MIR was actually the
-    /// following (this is hardcoded - see [crate::register] and [crate::translate_functions_to_ullbc]):
-    /// ```text
-    /// alloc::alloc::box_free::<T>(move b)
-    /// ```
-    ///
-    /// Also see the comments in [crate::assumed::type_to_used_params].
-    BoxFree,
     /// Converted from [ProjectionElem::Index].
     ///
     /// Signature: `fn<T,N>(&[T;N], usize) -> &T`
@@ -565,7 +549,7 @@ pub enum Rvalue {
 #[charon::variants_prefix("Aggregated")]
 pub enum AggregateKind {
     Adt(TypeId, Option<VariantId>, GenericArgs),
-    /// We don't put this with the ADT cas because this is the only assumed type
+    /// We don't put this with the ADT cas because this is the only built-in type
     /// with aggregates, and it is a primitive type. In particular, it makes
     /// sense to treat it differently because it has a variable number of fields.
     Array(Ty, ConstGeneric),
diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs
index 8d6bdaad5..e68e87c16 100644
--- a/charon/src/ast/gast_utils.rs
+++ b/charon/src/ast/gast_utils.rs
@@ -18,8 +18,8 @@ pub fn make_locals_generator(locals: &mut Vector<VarId, Var>) -> impl FnMut(Ty)
 }
 
 impl FunIdOrTraitMethodRef {
-    pub fn mk_assumed(aid: AssumedFunId) -> Self {
-        Self::Fun(FunId::Assumed(aid))
+    pub fn mk_builtin(aid: BuiltinFunId) -> Self {
+        Self::Fun(FunId::Builtin(aid))
     }
 }
 
diff --git a/charon/src/ast/mod.rs b/charon/src/ast/mod.rs
index 298a7cf49..f61b8a364 100644
--- a/charon/src/ast/mod.rs
+++ b/charon/src/ast/mod.rs
@@ -1,4 +1,4 @@
-pub mod assumed;
+pub mod builtins;
 pub mod expressions;
 pub mod expressions_utils;
 pub mod gast;
@@ -18,7 +18,7 @@ pub mod values;
 pub mod values_utils;
 
 // Re-export everything except llbc/ullbc, for convenience.
-pub use assumed::*;
+pub use builtins::*;
 pub use expressions::*;
 pub use gast::*;
 pub use krate::*;
diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs
index 13a508b79..f862a9289 100644
--- a/charon/src/ast/types.rs
+++ b/charon/src/ast/types.rs
@@ -537,7 +537,7 @@ pub enum RefKind {
 
 /// Type identifier.
 ///
-/// Allows us to factorize the code for assumed types, adts and tuples
+/// Allows us to factorize the code for built-in types, adts and tuples
 #[derive(
     Debug,
     PartialEq,
@@ -564,14 +564,15 @@ pub enum TypeId {
     #[charon::rename("TAdtId")]
     Adt(TypeDeclId),
     Tuple,
-    /// Assumed type. Either a primitive type like array or slice, or a
+    /// Built-in type. Either a primitive type like array or slice, or a
     /// non-primitive type coming from a standard library
     /// and that we handle like a primitive type. Types falling into this
     /// category include: Box, Vec, Cell...
     /// The Array and Slice types were initially modelled as primitive in
-    /// the [Ty] type. We decided to move them to assumed types as it allows
+    /// the [Ty] type. We decided to move them to built-in types as it allows
     /// for more uniform treatment throughout the codebase.
-    Assumed(AssumedTy),
+    #[charon::rename("TAssumed")]
+    Builtin(BuiltinTy),
 }
 
 /// Types of primitive values. Either an integer, bool, char
@@ -651,7 +652,7 @@ pub enum Ty {
     /// Note that here ADTs are very general. They can be:
     /// - user-defined ADTs
     /// - tuples (including `unit`, which is a 0-tuple)
-    /// - assumed types (includes some primitive types, e.g., arrays or slices)
+    /// - built-in types (includes some primitive types, e.g., arrays or slices)
     /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
     /// The last list is used encode const generics, e.g., the size of an array
     ///
@@ -705,16 +706,16 @@ pub enum Ty {
     Arrow(Vector<RegionId, RegionVar>, Vec<Ty>, Box<Ty>),
 }
 
-/// Assumed types identifiers.
+/// Builtin types identifiers.
 ///
-/// WARNING: for now, all the assumed types are covariant in the generic
+/// WARNING: for now, all the built-in types are covariant in the generic
 /// parameters (if there are). Adding types which don't satisfy this
 /// will require to update the code abstracting the signatures (to properly
 /// take into account the lifetime constraints).
 ///
 /// TODO: update to not hardcode the types (except `Box` maybe) and be more
 /// modular.
-/// TODO: move to assumed.rs?
+/// TODO: move to builtins.rs?
 #[derive(
     Debug,
     PartialEq,
@@ -733,7 +734,8 @@ pub enum Ty {
     PartialOrd,
 )]
 #[charon::variants_prefix("T")]
-pub enum AssumedTy {
+#[charon::rename("AssumedTy")]
+pub enum BuiltinTy {
     /// Boxes are de facto a primitive type.
     Box,
     /// Primitive type
diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs
index 037cc6b0d..9e7555d1b 100644
--- a/charon/src/ast/types_utils.rs
+++ b/charon/src/ast/types_utils.rs
@@ -283,7 +283,7 @@ impl Ty {
     /// Return true if the type is Box
     pub fn is_box(&self) -> bool {
         match self {
-            Ty::Adt(TypeId::Assumed(AssumedTy::Box), generics) => {
+            Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                 assert!(generics.regions.is_empty());
                 assert!(generics.types.len() == 1);
                 assert!(generics.const_generics.is_empty());
@@ -295,7 +295,7 @@ impl Ty {
 
     pub fn as_box(&self) -> Option<&Ty> {
         match self {
-            Ty::Adt(TypeId::Assumed(AssumedTy::Box), generics) => {
+            Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                 assert!(generics.regions.is_empty());
                 assert!(generics.types.len() == 1);
                 assert!(generics.const_generics.is_empty());
diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs
index b02a95e11..c76c51189 100644
--- a/charon/src/bin/charon-driver/driver.rs
+++ b/charon/src/bin/charon-driver/driver.rs
@@ -129,7 +129,7 @@ impl RunCompilerNormallyCallbacks {
     }
 }
 
-/// Returns the values of the command-line options that match `find_arg`. The options are assumed
+/// Returns the values of the command-line options that match `find_arg`. The options are built-in
 /// to be of the form `--arg=value` or `--arg value`.
 pub fn arg_values<'a, T: Deref<Target = str>>(
     args: &'a [T],
diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
index 412d4aa06..34afd1e8f 100644
--- a/charon/src/bin/charon-driver/translate/translate_ctx.rs
+++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -1086,10 +1086,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         self.blocks_map.get(&rid)
     }
 
-    pub(crate) fn get_var_from_id(&self, var_id: VarId) -> Option<&ast::Var> {
-        self.vars.get(var_id)
-    }
-
     pub(crate) fn register_type_decl_id(
         &mut self,
         span: rustc_span::Span,
diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
index dac0317b2..3624be733 100644
--- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -319,7 +319,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             Ty::Ref(_, _, _) => {
                                 projection.push(ProjectionElem::Deref);
                             }
-                            Ty::Adt(TypeId::Assumed(AssumedTy::Box), generics) => {
+                            Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                                 // This case only happens in some MIR levels
                                 assert!(!boxes_are_desugared(self.t_ctx.options.mir_level));
                                 assert!(generics.regions.is_empty());
@@ -367,7 +367,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                                         ProjectionElem::Field(proj_kind, field_id)
                                     }
-                                    Ty::Adt(TypeId::Assumed(AssumedTy::Box), generics) => {
+                                    Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                                         assert!(!boxes_are_desugared(self.t_ctx.options.mir_level));
 
                                         // Some more sanity checks
@@ -466,38 +466,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         Ok(self.translate_operand_with_type(span, operand)?.0)
     }
 
-    /// Translate an operand which should be `move b.0` where `b` is a box (such
-    /// operands are sometimes introduced here and there).
-    /// This is a degenerate case where we can't use
-    /// [`translate_operand`](translate_operand) on this kind of operands because
-    /// it will panic, due to the fact that we precisely track the type of the
-    /// values we go through during the path exploration.
-    /// We also prefer not to tweak `translate_operand` to account for this
-    /// ad-hoc behaviour (which comes from the fact that we abstract boxes, while
-    /// the rust compiler is too precise when manipulating those boxes, which
-    /// reveals implementation details).
-    fn translate_move_box_first_projector_operand(
-        &mut self,
-        span: rustc_span::Span,
-        operand: &hax::Operand,
-    ) -> Result<Operand, Error> {
-        trace!();
-        match operand {
-            hax::Operand::Move(place) => {
-                let place = self.translate_place(span, place)?;
-
-                // Sanity check
-                let var = self.get_var_from_id(place.var_id).unwrap();
-                assert!(var.ty.is_box());
-
-                Ok(Operand::Move(place))
-            }
-            _ => {
-                unreachable!();
-            }
-        }
-    }
-
     /// Translate an rvalue
     fn translate_rvalue(
         &mut self,
@@ -540,7 +508,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let (place, ty) = self.translate_place_with_type(span, place)?;
                 let cg = match &ty {
                     Ty::Adt(
-                        TypeId::Assumed(aty @ (AssumedTy::Array | AssumedTy::Slice)),
+                        TypeId::Builtin(aty @ (BuiltinTy::Array | BuiltinTy::Slice)),
                         generics,
                     ) => {
                         if aty.is_array() {
@@ -599,12 +567,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let unop = if let (
                             Ty::Ref(
                                 _,
-                                deref!(Ty::Adt(TypeId::Assumed(AssumedTy::Array), generics)),
+                                deref!(Ty::Adt(TypeId::Builtin(BuiltinTy::Array), generics)),
                                 kind1,
                             ),
                             Ty::Ref(
                                 _,
-                                deref!(Ty::Adt(TypeId::Assumed(AssumedTy::Slice), generics1)),
+                                deref!(Ty::Adt(TypeId::Builtin(BuiltinTy::Slice), generics1)),
                                 kind2,
                             ),
                         ) = (&src_ty, &tgt_ty)
@@ -804,9 +772,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             || panic_names.iter().any(|panic| name.equals_ref_name(panic))
         {
             Ok(Some(BuiltinFun::Panic))
-        } else if name.equals_ref_name(&["alloc", "alloc", "box_free"]) {
-            // TODO: check if this is still something that happens
-            Ok(Some(BuiltinFun::BoxFree))
         } else {
             Ok(None)
         }
@@ -816,7 +781,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     /// Translate a function id applied with some substitutions and some optional
     /// arguments.
     ///
-    /// We use a special function because the function might be assumed, and
+    /// We use a special function because the function might be built-in, and
     /// some parameters/arguments might need to be filtered.
     /// We return the fun id, its generics, and filtering information for the
     /// arguments.
@@ -834,7 +799,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         trait_info: &Option<hax::ImplExpr>,
     ) -> Result<SubstFunIdOrPanic, Error> {
         let rust_id = DefId::from(def_id);
-        let is_local = rust_id.is_local();
 
         let builtin_fun = self.recognize_builtin_fun(def_id)?;
         if matches!(builtin_fun, Some(BuiltinFun::Panic)) {
@@ -842,164 +806,103 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             return Ok(SubstFunIdOrPanic::Panic(name));
         }
 
-        // There is something annoying: when going to MIR, the rust compiler
-        // sometimes introduces very low-level functions, which we need to
-        // catch early - in particular, before we start translating types and
-        // arguments, because we won't be able to translate some of them.
-        let sfid = if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) {
-            assert!(!is_local);
-
-            // This deallocates a box.
-            // It should have two type parameters:
-            // - the type of the boxed value
-            // - the type of a global allocator (which we ignore)
-            assert!(substs.len() == 2);
-            assert!(trait_refs.is_empty());
-
-            // Translate the type parameter
-            let t_ty = if let hax::GenericArg::Type(ty) = substs.get(0).unwrap() {
-                self.translate_ty(span, erase_regions, ty)?
-            } else {
-                unreachable!()
-            };
+        // Translate the type parameters
+        let generics =
+            self.translate_substs_and_trait_refs(span, erase_regions, None, substs, trait_refs)?;
 
-            let args = args
-                .map(|args| {
-                    assert!(args.len() == 2);
-                    // Translate the first argument - note that we use a special
-                    // function to translate it: the operand should be of the form:
-                    // `move b.0`, and if it is the case it will return `move b`
-                    let arg = &args[0].node;
-                    let t_arg = self.translate_move_box_first_projector_operand(span, arg)?;
-                    Ok(vec![t_arg])
-                })
-                .transpose()?;
+        // Translate the arguments
+        let args = args
+            .map(|args| self.translate_arguments(span, args))
+            .transpose()?;
+
+        // Trait information
+        trace!(
+            "Trait information:\n- def_id: {:?}\n- impl source:\n{:?}",
+            rust_id,
+            trait_info
+        );
+        trace!(
+            "Method traits:\n- def_id: {:?}\n- traits:\n{:?}",
+            rust_id,
+            trait_refs
+        );
 
-            // Return
-            let func = FnPtr {
-                func: FunIdOrTraitMethodRef::mk_assumed(AssumedFunId::BoxFree),
-                generics: GenericArgs::new_from_types(vec![t_ty].into()),
+        // Check if the function is considered primitive: primitive
+        // functions benefit from special treatment.
+        let func = if let Some(builtin_fun) = builtin_fun {
+            // Primitive function.
+            //
+            // Note that there are subtleties with regards to the way types parameters
+            // are translated, because some functions are actually traits, where the
+            // types are used for the resolution. For instance, the following:
+            // `core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref`
+            // is translated to:
+            // `box_deref<T>`
+            // (the type parameter is not `Box<T>` but `T`).
+            assert!(trait_info.is_none());
+
+            let aid = builtin_fun.to_ullbc_builtin_fun();
+
+            // Note that some functions are actually traits (deref, index, etc.):
+            // we assume that they are called only on a limited set of types
+            // (ex.: box, vec...).
+            // For those trait functions, we need a custom treatment to retrieve
+            // and check the type information.
+            // For instance, derefencing boxes generates MIR of the following form:
+            // ```
+            // _2 = <Box<u32> as Deref>::deref(move _3)
+            // ```
+            // We have to retrieve the type `Box<u32>` and check that it is of the
+            // form `Box<T>` (and we generate `box_deref<u32>`).
+            match aid {
+                BuiltinFunId::BoxNew => {
+                    // Nothing to do
+                }
+                BuiltinFunId::ArrayIndexShared
+                | BuiltinFunId::ArrayIndexMut
+                | BuiltinFunId::ArrayToSliceShared
+                | BuiltinFunId::ArrayToSliceMut
+                | BuiltinFunId::ArrayRepeat
+                | BuiltinFunId::SliceIndexShared
+                | BuiltinFunId::SliceIndexMut => {
+                    // Those cases are introduced later, in micro-passes, by desugaring
+                    // projections (for ArrayIndex and ArrayIndexMut for instnace) and=
+                    // operations (for ArrayToSlice for instance) to function calls.
+                    unreachable!()
+                }
             };
-            SubstFunId { func, args }
-        } else {
-            // Retrieve the lists of used parameters, in case of non-local
-            // definitions
-            let (used_type_args, used_args) = if let Some(builtin_fun) = builtin_fun {
-                builtin_fun
-                    .to_fun_info()
-                    .map(|used| (used.used_type_params, used.used_args))
-            } else {
-                None
-            }
-            .unzip();
-
-            // Translate the type parameters
-            let generics = self.translate_substs_and_trait_refs(
-                span,
-                erase_regions,
-                used_type_args,
-                substs,
-                trait_refs,
-            )?;
-
-            // Translate the arguments
-            let args = args
-                .map(|args| self.translate_arguments(span, used_args, args))
-                .transpose()?;
-
-            // Trait information
-            trace!(
-                "Trait information:\n- def_id: {:?}\n- impl source:\n{:?}",
-                rust_id,
-                trait_info
-            );
-            trace!(
-                "Method traits:\n- def_id: {:?}\n- traits:\n{:?}",
-                rust_id,
-                trait_refs
-            );
-
-            // Check if the function is considered primitive: primitive
-            // functions benefit from special treatment.
-            let func = if let Some(builtin_fun) = builtin_fun {
-                // Primitive function.
-                //
-                // Note that there are subtleties with regards to the way types parameters
-                // are translated, because some functions are actually traits, where the
-                // types are used for the resolution. For instance, the following:
-                // `core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref`
-                // is translated to:
-                // `box_deref<T>`
-                // (the type parameter is not `Box<T>` but `T`).
-                assert!(trait_info.is_none());
-
-                let aid = builtin_fun.to_ullbc_builtin_fun();
-
-                // Note that some functions are actually traits (deref, index, etc.):
-                // we assume that they are called only on a limited set of types
-                // (ex.: box, vec...).
-                // For those trait functions, we need a custom treatment to retrieve
-                // and check the type information.
-                // For instance, derefencing boxes generates MIR of the following form:
-                // ```
-                // _2 = <Box<u32> as Deref>::deref(move _3)
-                // ```
-                // We have to retrieve the type `Box<u32>` and check that it is of the
-                // form `Box<T>` (and we generate `box_deref<u32>`).
-                match aid {
-                    AssumedFunId::BoxNew => {
-                        // Nothing to do
-                    }
-                    AssumedFunId::BoxFree => {
-                        // Special case handled elsewhere
-                        unreachable!();
-                    }
-                    AssumedFunId::ArrayIndexShared
-                    | AssumedFunId::ArrayIndexMut
-                    | AssumedFunId::ArrayToSliceShared
-                    | AssumedFunId::ArrayToSliceMut
-                    | AssumedFunId::ArrayRepeat
-                    | AssumedFunId::SliceIndexShared
-                    | AssumedFunId::SliceIndexMut => {
-                        // Those cases are introduced later, in micro-passes, by desugaring
-                        // projections (for ArrayIndex and ArrayIndexMut for instnace) and=
-                        // operations (for ArrayToSlice for instance) to function calls.
-                        unreachable!()
-                    }
-                };
 
-                FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid))
-            } else {
-                // Two cases depending on whether we call a trait method or not
-                match trait_info {
-                    None => {
-                        // "Regular" function call
-                        let def_id = self.register_fun_decl_id(span, rust_id);
-                        FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id))
-                    }
-                    Some(trait_info) => {
-                        // Trait method
-                        let rust_id = DefId::from(def_id);
-                        let impl_expr =
-                            self.translate_trait_impl_expr(span, erase_regions, trait_info)?;
-                        // The impl source should be Some(...): trait markers (that we may
-                        // eliminate) don't have methods.
-                        let impl_expr = impl_expr.unwrap();
+            FunIdOrTraitMethodRef::Fun(FunId::Builtin(aid))
+        } else {
+            // Two cases depending on whether we call a trait method or not
+            match trait_info {
+                None => {
+                    // "Regular" function call
+                    let def_id = self.register_fun_decl_id(span, rust_id);
+                    FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id))
+                }
+                Some(trait_info) => {
+                    // Trait method
+                    let rust_id = DefId::from(def_id);
+                    let impl_expr =
+                        self.translate_trait_impl_expr(span, erase_regions, trait_info)?;
+                    // The impl source should be Some(...): trait markers (that we may
+                    // eliminate) don't have methods.
+                    let impl_expr = impl_expr.unwrap();
 
-                        trace!("{:?}", rust_id);
+                    trace!("{:?}", rust_id);
 
-                        let trait_method_fun_id = self.register_fun_decl_id(span, rust_id);
-                        let method_name = self.t_ctx.translate_trait_item_name(rust_id)?;
+                    let trait_method_fun_id = self.register_fun_decl_id(span, rust_id);
+                    let method_name = self.t_ctx.translate_trait_item_name(rust_id)?;
 
-                        FunIdOrTraitMethodRef::Trait(impl_expr, method_name, trait_method_fun_id)
-                    }
+                    FunIdOrTraitMethodRef::Trait(impl_expr, method_name, trait_method_fun_id)
                 }
-            };
-            SubstFunId {
-                func: FnPtr { func, generics },
-                args,
             }
         };
+        let sfid = SubstFunId {
+            func: FnPtr { func, generics },
+            args,
+        };
         Ok(SubstFunIdOrPanic::Fun(sfid))
     }
 
@@ -1345,7 +1248,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 // this is rather an issue for the statement which creates
                 // the function pointer, by refering to a top-level function
                 // for instance.
-                let args = self.translate_arguments(span, None, args)?;
+                let args = self.translate_arguments(span, args)?;
                 let call = Call {
                     func: FnOperand::Move(p),
                     args,
@@ -1364,28 +1267,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     fn translate_arguments(
         &mut self,
         span: rustc_span::Span,
-        used_args: Option<Vec<bool>>,
         args: &Vec<hax::Spanned<hax::Operand>>,
     ) -> Result<Vec<Operand>, Error> {
-        let unspanned_args = args.iter().map(|x| &x.node);
-        let args: Vec<&hax::Operand> = match used_args {
-            None => unspanned_args.collect(),
-            Some(used_args) => {
-                assert!(args.len() == used_args.len());
-                unspanned_args
-                    .zip(used_args.into_iter())
-                    .filter_map(|(param, used)| if used { Some(param) } else { None })
-                    .collect()
-            }
-        };
-
         let mut t_args: Vec<Operand> = Vec::new();
-        for arg in args {
+        for arg in args.iter().map(|x| &x.node) {
             // Translate
             let op = self.translate_operand(span, arg)?;
             t_args.push(op);
         }
-
         Ok(t_args)
     }
 
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index b1f52b1dc..868dc08be 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -1,8 +1,8 @@
 use crate::translate::translate_traits::PredicateLocation;
 
 use super::translate_ctx::*;
-use charon_lib::assumed;
 use charon_lib::ast::*;
+use charon_lib::builtins;
 use charon_lib::common::*;
 use charon_lib::formatter::IntoFormatter;
 use charon_lib::ids::Vector;
@@ -190,8 +190,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let type_id = self.translate_type_id(span, def_id)?;
 
                 // Retrieve the list of used arguments
-                let used_params = if let TypeId::Assumed(assumed_ty) = type_id {
-                    Some(assumed::type_to_used_params(assumed_ty))
+                let used_params = if let TypeId::Builtin(builtin_ty) = type_id {
+                    Some(builtins::type_to_used_params(builtin_ty))
                 } else {
                     None
                 };
@@ -211,7 +211,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             hax::Ty::Str => {
                 trace!("Str");
 
-                let id = TypeId::Assumed(AssumedTy::Str);
+                let id = TypeId::Builtin(BuiltinTy::Str);
                 Ok(Ty::Adt(id, GenericArgs::empty()))
             }
             hax::Ty::Array(ty, const_param) => {
@@ -220,7 +220,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let c = self.translate_constant_expr_to_const_generic(span, const_param)?;
                 let tys = vec![self.translate_ty(span, erase_regions, ty)?].into();
                 let cgs = vec![c].into();
-                let id = TypeId::Assumed(AssumedTy::Array);
+                let id = TypeId::Builtin(BuiltinTy::Array);
                 Ok(Ty::Adt(
                     id,
                     GenericArgs::new(Vector::new(), tys, cgs, Vector::new()),
@@ -230,7 +230,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 trace!("Slice");
 
                 let tys = vec![self.translate_ty(span, erase_regions, ty)?].into();
-                let id = TypeId::Assumed(AssumedTy::Slice);
+                let id = TypeId::Builtin(BuiltinTy::Slice);
                 Ok(Ty::Adt(id, GenericArgs::new_from_types(tys)))
             }
             hax::Ty::Ref(region, ty, mutability) => {
@@ -448,12 +448,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     }
 
     /// Checks whether the given id corresponds to a built-in type.
-    fn recognize_builtin_type(&mut self, def_id: &hax::DefId) -> Result<Option<AssumedTy>, Error> {
+    fn recognize_builtin_type(&mut self, def_id: &hax::DefId) -> Result<Option<BuiltinTy>, Error> {
         use rustc_hir::lang_items::LangItem;
         let tcx = self.t_ctx.tcx;
         let rust_id = DefId::from(def_id);
         let ty = if tcx.is_lang_item(rust_id, LangItem::OwnedBox) {
-            Some(AssumedTy::Box)
+            Some(BuiltinTy::Box)
         } else {
             None
         };
@@ -468,7 +468,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     ) -> Result<TypeId, Error> {
         trace!("{:?}", def_id);
         let type_id = match self.recognize_builtin_type(def_id)? {
-            Some(id) => TypeId::Assumed(id),
+            Some(id) => TypeId::Builtin(id),
             None => {
                 let rust_id: DefId = def_id.into();
                 TypeId::Adt(self.register_type_decl_id(span, rust_id))
diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs
index 861fe88c1..e886bb4aa 100644
--- a/charon/src/bin/generate-ml/main.rs
+++ b/charon/src/bin/generate-ml/main.rs
@@ -13,7 +13,7 @@ use charon_lib::export::CrateData;
 use charon_lib::meta::ItemMeta;
 use charon_lib::names::{Name, PathElem};
 use charon_lib::types::{
-    AssumedTy, Field, LiteralTy, Ty, TypeDecl, TypeDeclId, TypeDeclKind, TypeId,
+    BuiltinTy, Field, LiteralTy, Ty, TypeDecl, TypeDeclId, TypeDeclKind, TypeId,
 };
 use convert_case::{Case, Casing};
 use derive_visitor::Drive;
@@ -137,7 +137,7 @@ fn type_to_ocaml_call(ctx: &GenerateCtx, ty: &Ty) -> String {
                     }
                     expr.insert(0, first + "_of_json");
                 }
-                TypeId::Assumed(AssumedTy::Box) => {}
+                TypeId::Builtin(BuiltinTy::Box) => {}
                 TypeId::Tuple => {
                     let name = match generics.types.len() {
                         2 => "pair_of_json".to_string(),
@@ -210,7 +210,7 @@ fn type_to_ocaml_name(ctx: &GenerateCtx, ty: &Ty) -> String {
                     };
                     format!("{args} {base_ty}")
                 }
-                TypeId::Assumed(AssumedTy::Box) => args[0].clone(),
+                TypeId::Builtin(BuiltinTy::Box) => args[0].clone(),
                 TypeId::Tuple => args.iter().join("*"),
                 _ => unimplemented!("{ty:?}"),
             }
@@ -711,7 +711,7 @@ fn main() -> Result<()> {
             template: dir.join("templates/Expressions.ml"),
             target: dir.join("generated/Expressions.ml"),
             markers: &[
-                (GenerationKind::TypeDecl(false), &["AssumedFunId", "AbortKind"]),
+                (GenerationKind::TypeDecl(false), &["BuiltinFunId", "AbortKind"]),
                 (GenerationKind::TypeDecl(false), &["FieldProjKind", "ProjectionElem", "Projection", "Place"]),
                 (GenerationKind::TypeDecl(false), &["BorrowKind", "BinOp"]),
                 (GenerationKind::TypeDecl(false), &[
@@ -740,7 +740,7 @@ fn main() -> Result<()> {
             target: dir.join("generated/Types.ml"),
             markers: &[
                 (GenerationKind::TypeDecl(false), &[
-                    "AssumedTy",
+                    "BuiltinTy",
                     "TypeId",
                     "ExistentialPredicate",
                     "Ty",
@@ -805,7 +805,7 @@ fn main() -> Result<()> {
                     "LiteralTy",
                     "ConstGenericVar",
                     "RefKind",
-                    "AssumedTy",
+                    "BuiltinTy",
                     "TypeId",
                     "ConstGeneric",
                     "Ty",
@@ -842,7 +842,7 @@ fn main() -> Result<()> {
                     "UnOp",
                     "BinOp",
                     "Literal",
-                    "AssumedFunId",
+                    "BuiltinFunId",
                     "FunId",
                     "FunIdOrTraitMethodRef",
                     "FnPtr",
diff --git a/charon/src/lib.rs b/charon/src/lib.rs
index 7a62693df..f6dcce97f 100644
--- a/charon/src/lib.rs
+++ b/charon/src/lib.rs
@@ -43,7 +43,7 @@ pub mod pretty;
 pub mod transform;
 
 // Re-export all the ast modules so we can keep the old import structure.
-pub use ast::{assumed, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values};
+pub use ast::{builtins, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values};
 pub use pretty::formatter;
 pub use transform::{graphs, reorder_decls, ullbc_to_llbc};
 
diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs
index fd921317b..a815bb407 100644
--- a/charon/src/name_matcher/mod.rs
+++ b/charon/src/name_matcher/mod.rs
@@ -91,8 +91,8 @@ impl Pattern {
                 };
                 self.matches_with_generics(ctx, type_name, args)
             }
-            Ty::Adt(TypeId::Assumed(assumed_ty), args) => {
-                let name = assumed_ty.get_name();
+            Ty::Adt(TypeId::Builtin(builtin_ty), args) => {
+                let name = builtin_ty.get_name();
                 self.matches_with_generics(ctx, &name, args)
             }
             Ty::Adt(TypeId::Tuple, _)
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index 5c43624bf..82e539501 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -195,8 +195,8 @@ impl<C: AstFormatter> FmtWithCtx<C> for FnPtr {
             FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)) => {
                 format!("{}", ctx.format_object(*def_id),)
             }
-            FunIdOrTraitMethodRef::Fun(FunId::Assumed(assumed)) => {
-                format!("@{}", assumed.variant_name())
+            FunIdOrTraitMethodRef::Fun(FunId::Builtin(builtin)) => {
+                format!("@{}", builtin.variant_name())
             }
             FunIdOrTraitMethodRef::Trait(trait_ref, method_id, _) => {
                 format!("{}::{}", trait_ref.fmt_with_ctx(ctx), &method_id.0)
@@ -842,7 +842,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for Rvalue {
                     AggregateKind::Adt(def_id, variant_id, _) => {
                         match def_id {
                             TypeId::Tuple => format!("({})", ops_s.join(", ")),
-                            TypeId::Assumed(_) => unreachable!(),
+                            TypeId::Builtin(_) => unreachable!(),
                             TypeId::Adt(def_id) => {
                                 // Format every field
                                 let mut fields = vec![];
@@ -1427,7 +1427,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TypeId {
         match self {
             TypeId::Tuple => "".to_string(),
             TypeId::Adt(def_id) => ctx.format_object(*def_id),
-            TypeId::Assumed(aty) => aty.get_name().fmt_with_ctx(ctx),
+            TypeId::Builtin(aty) => aty.get_name().fmt_with_ctx(ctx),
         }
     }
 }
diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs
index ce67c54b7..f7e3c894c 100644
--- a/charon/src/transform/check_generics.rs
+++ b/charon/src/transform/check_generics.rs
@@ -62,7 +62,7 @@ impl CheckGenericsVisitor<'_, '_> {
                     self.error("Mismatched generics: generics for a tuple should be only types")
                 }
             }
-            TypeId::Assumed(..) => {
+            TypeId::Builtin(..) => {
                 // TODO: check generics for built-in types
                 self.discharged_one_generics()
             }
@@ -90,7 +90,7 @@ impl CheckGenericsVisitor<'_, '_> {
             | FunIdOrTraitMethodRef::Trait(_, _, id) => {
                 self.generics_should_match_item(args, *id);
             }
-            FunIdOrTraitMethodRef::Fun(FunId::Assumed(..)) => {
+            FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {
                 // TODO: check generics for built-in types
                 self.discharged_one_generics()
             }
diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs
index 1b7951dd9..9b187c5f0 100644
--- a/charon/src/transform/index_to_function_calls.rs
+++ b/charon/src/transform/index_to_function_calls.rs
@@ -51,19 +51,19 @@ impl<'a> Visitor<'a> {
             if let ProjectionElem::Index(arg_index, buf_ty) = pe {
                 let (id, generics) = buf_ty.as_adt();
                 let cgs: Vector<_, ConstGeneric> = generics.const_generics.clone();
-                let index_id = match id.as_assumed() {
-                    AssumedTy::Array => {
+                let index_id = match id.as_builtin() {
+                    BuiltinTy::Array => {
                         if mut_access {
-                            AssumedFunId::ArrayIndexMut
+                            BuiltinFunId::ArrayIndexMut
                         } else {
-                            AssumedFunId::ArrayIndexShared
+                            BuiltinFunId::ArrayIndexShared
                         }
                     }
-                    AssumedTy::Slice => {
+                    BuiltinTy::Slice => {
                         if mut_access {
-                            AssumedFunId::SliceIndexMut
+                            BuiltinFunId::SliceIndexMut
                         } else {
-                            AssumedFunId::SliceIndexShared
+                            BuiltinFunId::SliceIndexShared
                         }
                     }
                     _ => unreachable!(),
@@ -105,7 +105,7 @@ impl<'a> Visitor<'a> {
                 let elem_borrow_var = self.fresh_var(None, elem_borrow_ty);
                 let arg_buf = Operand::Move(Place::new(buf_borrow_var));
                 let index_dest = Place::new(elem_borrow_var);
-                let index_id = FunIdOrTraitMethodRef::mk_assumed(index_id);
+                let index_id = FunIdOrTraitMethodRef::mk_builtin(index_id);
                 let generics = GenericArgs::new(
                     vec![Region::Erased].into(),
                     vec![elem_ty].into(),
diff --git a/charon/src/transform/inline_local_panic_functions.rs b/charon/src/transform/inline_local_panic_functions.rs
index 7dd21fec6..2fd4d13c3 100644
--- a/charon/src/transform/inline_local_panic_functions.rs
+++ b/charon/src/transform/inline_local_panic_functions.rs
@@ -13,7 +13,7 @@ use std::collections::HashSet;
 
 use super::{ctx::LlbcPass, TransformCtx};
 use crate::{
-    assumed,
+    builtins,
     llbc_ast::{
         AbortKind, Call, FnOperand, FnPtr, FunId, FunIdOrTraitMethodRef, RawStatement, Statement,
     },
@@ -30,7 +30,7 @@ impl LlbcPass for Transform {
                 let body = body.as_structured().unwrap();
                 // If the whole body is only a call to this specific panic function.
                 if let RawStatement::Abort(AbortKind::Panic(name)) = &body.body.content {
-                    if name.equals_ref_name(assumed::EXPLICIT_PANIC_NAME) {
+                    if name.equals_ref_name(builtins::EXPLICIT_PANIC_NAME) {
                         // FIXME: also check that the name of the function is
                         // `panic_cold_explicit`?
                         panic_fns.insert(decl.def_id);
@@ -39,7 +39,7 @@ impl LlbcPass for Transform {
             }
         });
 
-        let panic_name = Name::from_path(assumed::EXPLICIT_PANIC_NAME);
+        let panic_name = Name::from_path(builtins::EXPLICIT_PANIC_NAME);
         let panic_statement = RawStatement::Abort(AbortKind::Panic(panic_name));
 
         // Replace each call to one such function with a `Panic`.
diff --git a/charon/src/transform/ops_to_function_calls.rs b/charon/src/transform/ops_to_function_calls.rs
index 26fd712f6..704c7ca75 100644
--- a/charon/src/transform/ops_to_function_calls.rs
+++ b/charon/src/transform/ops_to_function_calls.rs
@@ -14,10 +14,10 @@ fn transform_st(s: &mut Statement) -> Option<Vec<Statement>> {
             // We could avoid the clone operations below if we take the content of
             // the statement. In practice, this shouldn't have much impact.
             let id = match ref_kind {
-                RefKind::Mut => AssumedFunId::ArrayToSliceMut,
-                RefKind::Shared => AssumedFunId::ArrayToSliceShared,
+                RefKind::Mut => BuiltinFunId::ArrayToSliceMut,
+                RefKind::Shared => BuiltinFunId::ArrayToSliceShared,
             };
-            let func = FunIdOrTraitMethodRef::mk_assumed(id);
+            let func = FunIdOrTraitMethodRef::mk_builtin(id);
             let generics = GenericArgs::new(
                 vec![Region::Erased].into(),
                 vec![ty.clone()].into(),
@@ -37,8 +37,8 @@ fn transform_st(s: &mut Statement) -> Option<Vec<Statement>> {
         RawStatement::Assign(p, Rvalue::Repeat(op, ty, cg)) => {
             // We could avoid the clone operations below if we take the content of
             // the statement. In practice, this shouldn't have much impact.
-            let id = AssumedFunId::ArrayRepeat;
-            let func = FunIdOrTraitMethodRef::mk_assumed(id);
+            let id = BuiltinFunId::ArrayRepeat;
+            let func = FunIdOrTraitMethodRef::mk_builtin(id);
             let generics = GenericArgs::new(
                 vec![Region::Erased].into(),
                 vec![ty.clone()].into(),
diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out
index e8d3c6b8e..409b52fa7 100644
--- a/charon/tests/ui/unsupported/advanced-const-generics.out
+++ b/charon/tests/ui/unsupported/advanced-const-generics.out
@@ -1,4 +1,4 @@
-thread 'rustc' panicked at src/ast/types.rs:641:5:
+thread 'rustc' panicked at src/ast/types.rs:642:5:
 internal error: entered unreachable code: Ty::to_literal: Not the proper variant
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `test_crate::foo`.