diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index 964286984fc6..2bd3e1ff7c35 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -39,7 +39,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let mut instance_under_contract = items.iter().filter_map(|i| match i {
             MonoItem::Fn(instance @ Instance { def, .. })
-                if wrapped_fn == rustc_internal::internal(def.def_id()) =>
+                if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) =>
             {
                 Some(*instance)
             }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 0709682afa65..6c711e3d20e4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -3,7 +3,7 @@
 //! this module handles intrinsics
 use super::typ;
 use super::{bb_label, PropertyClass};
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, pretty_ty};
+use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::{utils, GotocCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{
@@ -646,7 +646,7 @@ impl<'tcx> GotocCtx<'tcx> {
             span,
             format!(
                 "Type check failed for intrinsic `{name}`: Expected {expected}, found {}",
-                pretty_ty(actual)
+                self.pretty_ty(actual)
             ),
         );
         self.tcx.dcx().abort_if_errors();
@@ -779,12 +779,16 @@ impl<'tcx> GotocCtx<'tcx> {
         if layout.abi.is_uninhabited() {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
-                &format!("attempted to instantiate uninhabited type `{}`", pretty_ty(*target_ty)),
+                &format!(
+                    "attempted to instantiate uninhabited type `{}`",
+                    self.pretty_ty(*target_ty)
+                ),
                 span,
             );
         }
 
-        let param_env_and_type = ParamEnv::reveal_all().and(rustc_internal::internal(target_ty));
+        let param_env_and_type =
+            ParamEnv::reveal_all().and(rustc_internal::internal(self.tcx, target_ty));
 
         // Then we check if the type allows "raw" initialization for the cases
         // where memory is zero-initialized or entirely uninitialized
@@ -798,7 +802,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 PropertyClass::SafetyCheck,
                 &format!(
                     "attempted to zero-initialize type `{}`, which is invalid",
-                    pretty_ty(*target_ty)
+                    self.pretty_ty(*target_ty)
                 ),
                 span,
             );
@@ -817,7 +821,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 PropertyClass::SafetyCheck,
                 &format!(
                     "attempted to leave type `{}` uninitialized, which is invalid",
-                    pretty_ty(*target_ty)
+                    self.pretty_ty(*target_ty)
                 ),
                 span,
             );
@@ -1285,7 +1289,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 _ => {
                     let err_msg = format!(
                         "simd_shuffle index must be an array of `u32`, got `{}`",
-                        pretty_ty(farg_types[2])
+                        self.pretty_ty(farg_types[2])
                     );
                     utils::span_err(self.tcx, span, err_msg);
                     // Return a dummy value
@@ -1378,7 +1382,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
                 // Packed types ignore the alignment of their fields.
                 if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() {
-                    if rustc_internal::internal(def).repr().packed() {
+                    if rustc_internal::internal(self.tcx, def).repr().packed() {
                         unsized_align = sized_align.clone();
                     }
                 }
@@ -1426,9 +1430,9 @@ impl<'tcx> GotocCtx<'tcx> {
         if rust_ret_type != vector_base_type {
             let err_msg = format!(
                 "expected return type `{}` (element of input `{}`), found `{}`",
-                pretty_ty(vector_base_type),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_ret_type)
+                self.pretty_ty(vector_base_type),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_ret_type)
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1466,9 +1470,9 @@ impl<'tcx> GotocCtx<'tcx> {
         if vector_base_type != rust_arg_types[2] {
             let err_msg = format!(
                 "expected inserted type `{}` (element of input `{}`), found `{}`",
-                pretty_ty(vector_base_type),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_arg_types[2]),
+                self.pretty_ty(vector_base_type),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_arg_types[2]),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1534,8 +1538,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 "expected return type with length {} (same as input type `{}`), \
                 found `{}` with length {}",
                 arg1.typ().len().unwrap(),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_ret_type),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_ret_type),
                 ret_typ.len().unwrap()
             );
             utils::span_err(self.tcx, span, err_msg);
@@ -1545,8 +1549,8 @@ impl<'tcx> GotocCtx<'tcx> {
             let (_, rust_base_type) = self.simd_size_and_type(rust_ret_type);
             let err_msg = format!(
                 "expected return type with integer elements, found `{}` with non-integer `{}`",
-                pretty_ty(rust_ret_type),
-                pretty_ty(rust_base_type),
+                self.pretty_ty(rust_ret_type),
+                self.pretty_ty(rust_base_type),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1740,7 +1744,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if ret_type_len != n {
             let err_msg = format!(
                 "expected return type of length {n}, found `{}` with length {ret_type_len}",
-                pretty_ty(rust_ret_type),
+                self.pretty_ty(rust_ret_type),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1748,10 +1752,10 @@ impl<'tcx> GotocCtx<'tcx> {
             let err_msg = format!(
                 "expected return element type `{}` (element of input `{}`), \
                  found `{}` with element type `{}`",
-                pretty_ty(vec_subtype),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_ret_type),
-                pretty_ty(ret_type_subtype),
+                self.pretty_ty(vec_subtype),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_ret_type),
+                self.pretty_ty(ret_type_subtype),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index fd9ff33e164e..9296b713c862 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -260,7 +260,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         Ok(parent_expr.member(Self::tuple_fld_name(field_idx), &self.symbol_table))
                     }
                     TyKind::RigidTy(RigidTy::Adt(def, _))
-                        if rustc_internal::internal(def).repr().simd() =>
+                        if rustc_internal::internal(self.tcx, def).repr().simd() =>
                     {
                         Ok(self.codegen_simd_field(
                             parent_expr,
@@ -415,7 +415,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 };
 
                 let inner_mir_typ_internal =
-                    std_pointee_type(rustc_internal::internal(base_type)).unwrap();
+                    std_pointee_type(rustc_internal::internal(self.tcx, base_type)).unwrap();
                 let inner_mir_typ = rustc_internal::stable(inner_mir_typ_internal);
                 let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self
                     .use_thin_pointer(inner_mir_typ_internal)
@@ -436,6 +436,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     );
                     assert!(
                         self.use_fat_pointer(rustc_internal::internal(
+                            self.tcx,
                             pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()
                         )),
                         "Unexpected type: {:?} -- {:?}",
@@ -582,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         (variant.name().into(), TypeOrVariant::Variant(variant))
                     }
                     TyKind::RigidTy(RigidTy::Coroutine(..)) => {
-                        let idx_internal = rustc_internal::internal(idx);
+                        let idx_internal = rustc_internal::internal(self.tcx, idx);
                         (
                             self.coroutine_variant_name(idx_internal),
                             TypeOrVariant::CoroutineVariant(*idx),
@@ -593,7 +594,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         &ty.kind()
                     ),
                 };
-                let layout = self.layout_of(rustc_internal::internal(ty));
+                let layout = self.layout_of(rustc_internal::internal(self.tcx, ty));
                 let expr = match &layout.variants {
                     Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index c4ea258fe79e..e7501df3aac4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
             let layout = self.layout_of_stable(res_ty);
             let fields = match &layout.variants {
                 Variants::Single { index } => {
-                    if *index != rustc_internal::internal(variant_index) {
+                    if *index != rustc_internal::internal(self.tcx, variant_index) {
                         // This may occur if all variants except for the one pointed by
                         // index can never be constructed. Generic code might still try
                         // to initialize the non-existing invariant.
@@ -565,7 +565,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     &layout.fields
                 }
                 Variants::Multiple { variants, .. } => {
-                    &variants[rustc_internal::internal(variant_index)].fields
+                    &variants[rustc_internal::internal(self.tcx, variant_index)].fields
                 }
             };
 
@@ -716,7 +716,10 @@ impl<'tcx> GotocCtx<'tcx> {
                             .offset_of_subfield(
                                 self,
                                 fields.iter().map(|(var_idx, field_idx)| {
-                                    (rustc_internal::internal(var_idx), (*field_idx).into())
+                                    (
+                                        rustc_internal::internal(self.tcx, var_idx),
+                                        (*field_idx).into(),
+                                    )
                                 }),
                             )
                             .bytes(),
@@ -1180,7 +1183,7 @@ impl<'tcx> GotocCtx<'tcx> {
             if self.vtable_ctx.emit_vtable_restrictions {
                 // Add to the possible method names for this trait type
                 self.vtable_ctx.add_possible_method(
-                    self.normalized_trait_name(rustc_internal::internal(ty)).into(),
+                    self.normalized_trait_name(rustc_internal::internal(self.tcx, ty)).into(),
                     idx,
                     fn_name.into(),
                 );
@@ -1205,7 +1208,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate a function pointer to drop_in_place for entry into the vtable
     fn codegen_vtable_drop_in_place(&mut self, ty: Ty, trait_ty: Ty) -> Expr {
-        let trait_ty = rustc_internal::internal(trait_ty);
+        let trait_ty = rustc_internal::internal(self.tcx, trait_ty);
         let drop_instance = Instance::resolve_drop_in_place(ty);
         let drop_sym_name: InternedString = drop_instance.mangled_name().into();
 
@@ -1296,7 +1299,7 @@ impl<'tcx> GotocCtx<'tcx> {
             _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
         };
 
-        let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type));
+        let src_name = self.ty_mangled_name(rustc_internal::internal(self.tcx, src_mir_type));
         // The name needs to be the same as inserted in typ.rs
         let vtable_name = self.vtable_name_stable(trait_type).intern();
         let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}");
@@ -1310,7 +1313,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Build the vtable, using Rust's vtable_entries to determine field order
                 let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() {
                     let trait_ref_binder = principal.with_self_ty(src_mir_type);
-                    ctx.tcx.vtable_entries(rustc_internal::internal(trait_ref_binder))
+                    ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder))
                 } else {
                     TyCtxt::COMMON_VTABLE_ENTRIES
                 };
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index c06d64d298c4..d06829822274 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -31,7 +31,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location {
-        self.codegen_caller_span(&rustc_internal::internal(sp))
+        self.codegen_caller_span(&rustc_internal::internal(self.tcx, sp))
     }
 
     /// Get the location of the caller. This will attempt to reach the macro caller.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 3a62a3f91d1a..05eb1bc41dc7 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -220,8 +220,8 @@ impl<'tcx> GotocCtx<'tcx> {
         location: Location,
     ) -> Stmt {
         // this requires place points to an enum type.
-        let dest_ty_internal = rustc_internal::internal(dest_ty);
-        let variant_index_internal = rustc_internal::internal(variant_index);
+        let dest_ty_internal = rustc_internal::internal(self.tcx, dest_ty);
+        let variant_index_internal = rustc_internal::internal(self.tcx, variant_index);
         let layout = self.layout_of(dest_ty_internal);
         match &layout.variants {
             Variants::Single { .. } => Stmt::skip(location),
@@ -533,7 +533,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let instance = Instance::resolve(def, &subst).unwrap();
 
                 // TODO(celina): Move this check to be inside codegen_funcall_args.
-                if self.ty_needs_untupled_args(rustc_internal::internal(funct)) {
+                if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) {
                     self.codegen_untupled_args(instance, &mut fargs, args.last());
                 }
 
@@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr {
         // Generate an expression that indexes the pointer.
         let expr = self
-            .receiver_data_path(rustc_internal::internal(arg_ty))
+            .receiver_data_path(rustc_internal::internal(self.tcx, arg_ty))
             .fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table));
 
         trace!(?arg_ty, gotoc_ty=?expr.typ(), gotoc_expr=?expr.value(), "extract_ptr");
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
index c4f03e6c2cef..0130beffe84b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -20,11 +20,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type {
-        self.codegen_ty(rustc_internal::internal(ty))
+        self.codegen_ty(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn codegen_ty_ref_stable(&mut self, ty: Ty) -> Type {
-        self.codegen_ty_ref(rustc_internal::internal(ty))
+        self.codegen_ty_ref(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn local_ty_stable(&self, local: Local) -> Ty {
@@ -36,11 +36,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn is_zst_stable(&self, ty: Ty) -> bool {
-        self.is_zst(rustc_internal::internal(ty))
+        self.is_zst(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn layout_of_stable(&self, ty: Ty) -> TyAndLayout<'tcx> {
-        self.layout_of(rustc_internal::internal(ty))
+        self.layout_of(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type {
@@ -53,27 +53,27 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.use_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.use_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn use_thin_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.use_thin_pointer(rustc_internal::internal(pointer_ty))
+        self.use_thin_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn is_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.is_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.is_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn is_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.is_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.is_vtable_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn use_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.use_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.use_vtable_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn vtable_name_stable(&self, ty: Ty) -> String {
-        self.vtable_name(rustc_internal::internal(ty))
+        self.vtable_name(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty {
@@ -81,12 +81,12 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) {
-        let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx);
+        let (sz, ty) = rustc_internal::internal(self.tcx, ty).simd_size_and_type(self.tcx);
         (sz, rustc_internal::stable(ty))
     }
 
     pub fn codegen_enum_discr_typ_stable(&self, ty: Ty) -> Ty {
-        rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(ty)))
+        rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(self.tcx, ty)))
     }
 
     pub fn codegen_function_sig_stable(&mut self, sig: FnSig) -> Type {
@@ -107,6 +107,14 @@ impl<'tcx> GotocCtx<'tcx> {
             Type::code_with_unnamed_parameters(params, self.codegen_ty_stable(sig.output()))
         }
     }
+
+    /// Convert a type into a user readable type representation.
+    ///
+    /// This should be replaced by StableMIR `pretty_ty()` after
+    /// <https://github.com/rust-lang/rust/pull/118364> is merged.
+    pub fn pretty_ty(&self, ty: Ty) -> String {
+        rustc_internal::internal(self.tcx, ty).to_string()
+    }
 }
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
@@ -117,14 +125,6 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
     }
 }
 
-/// Convert a type into a user readable type representation.
-///
-/// This should be replaced by StableMIR `pretty_ty()` after
-/// <https://github.com/rust-lang/rust/pull/118364> is merged.
-pub fn pretty_ty(ty: Ty) -> String {
-    rustc_internal::internal(ty).to_string()
-}
-
 pub fn pointee_type_stable(ty: Ty) -> Option<Ty> {
     match ty.kind() {
         TyKind::RigidTy(RigidTy::Ref(_, pointee_ty, _))
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 83ec6c3374ae..62b5cbedd95a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1101,7 +1101,7 @@ impl<'tcx> GotocCtx<'tcx> {
             .map(|(_, arg_abi)| {
                 let arg_ty_stable = arg_abi.ty;
                 let kind = arg_ty_stable.kind();
-                let arg_ty = rustc_internal::internal(arg_ty_stable);
+                let arg_ty = rustc_internal::internal(self.tcx, arg_ty_stable);
                 if is_first {
                     is_first = false;
                     debug!(self_type=?arg_ty, ?fn_abi, "codegen_dynamic_function_sig");
@@ -1686,7 +1686,7 @@ impl<'tcx> GotocCtx<'tcx> {
         instance: InstanceStable,
         fn_abi: &'a FnAbi,
     ) -> impl Iterator<Item = (usize, &'a ArgAbi)> {
-        let instance_internal = rustc_internal::internal(instance);
+        let instance_internal = rustc_internal::internal(self.tcx, instance);
         let requires_caller_location = instance_internal.def.requires_caller_location(self.tcx);
         let num_args = fn_abi.args.len();
         fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 1cfff307f856..810c5707aad4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -307,7 +307,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     let main_instance =
                         stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
                     let local_reachable = filter_crate_items(tcx, |_, instance| {
-                        let def_id = rustc_internal::internal(instance.def.def_id());
+                        let def_id = rustc_internal::internal(tcx, instance.def.def_id());
                         Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)
                     })
                     .into_iter()
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
index b8251b153e5a..adac294e30eb 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -4,8 +4,8 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Stmt;
 use cbmc::InternedString;
-use rustc_middle::mir::Body as InternalBody;
-use rustc_middle::ty::Instance as InternalInstance;
+use rustc_middle::mir::Body as BodyInternal;
+use rustc_middle::ty::Instance as InstanceInternal;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Local, LocalDecl};
@@ -22,7 +22,9 @@ pub struct CurrentFnCtx<'tcx> {
     /// The crate this function is from
     krate: String,
     /// The MIR for the current instance. This is using the internal representation.
-    mir: &'tcx InternalBody<'tcx>,
+    mir: &'tcx BodyInternal<'tcx>,
+    /// The current instance. This is using the internal representation.
+    instance_internal: InstanceInternal<'tcx>,
     /// A list of local declarations used to retrieve MIR component types.
     locals: Vec<LocalDecl>,
     /// A list of pretty names for locals that corrspond to user variables.
@@ -38,7 +40,7 @@ pub struct CurrentFnCtx<'tcx> {
 /// Constructor
 impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self {
-        let internal_instance = rustc_internal::internal(instance);
+        let instance_internal = rustc_internal::internal(gcx.tcx, instance);
         let readable_name = instance.name();
         let name =
             if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() };
@@ -51,7 +53,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
         Self {
             block: vec![],
             instance,
-            mir: gcx.tcx.instance_mir(internal_instance.def),
+            mir: gcx.tcx.instance_mir(instance_internal.def),
+            instance_internal,
             krate: instance.def.krate().name,
             locals,
             local_names,
@@ -83,8 +86,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
 /// Getters
 impl<'tcx> CurrentFnCtx<'tcx> {
     /// The function we are currently compiling
-    pub fn instance(&self) -> InternalInstance<'tcx> {
-        rustc_internal::internal(self.instance)
+    pub fn instance(&self) -> InstanceInternal<'tcx> {
+        self.instance_internal
     }
 
     pub fn instance_stable(&self) -> Instance {
@@ -92,7 +95,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     }
 
     /// The internal MIR for the function we are currently compiling using internal APIs.
-    pub fn body_internal(&self) -> &'tcx InternalBody<'tcx> {
+    pub fn body_internal(&self) -> &'tcx BodyInternal<'tcx> {
         self.mir
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 97606688d1ed..0141c2886539 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -38,7 +38,7 @@ pub trait GotocHook {
 fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool {
     let attr_sym = rustc_span::symbol::Symbol::intern(attr_name);
     if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) {
-        if rustc_internal::internal(instance.def.def_id()) == *attr_id {
+        if rustc_internal::internal(tcx, instance.def.def_id()) == *attr_id {
             debug!("matched: {:?} {:?}", attr_id, attr_sym);
             return true;
         }
@@ -196,7 +196,7 @@ struct Panic;
 
 impl GotocHook for Panic {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        let def_id = rustc_internal::internal(instance.def.def_id());
+        let def_id = rustc_internal::internal(tcx, instance.def.def_id());
         Some(def_id) == tcx.lang_items().panic_fn()
             || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str)
             || Some(def_id) == tcx.lang_items().panic_fmt()
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index d81839ea097c..e369f64beda9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -194,5 +194,5 @@ impl<'tcx> GotocCtx<'tcx> {
 }
 
 pub fn span_err(tcx: TyCtxt, span: Span, msg: String) {
-    tcx.dcx().span_err(rustc_internal::internal(span), msg);
+    tcx.dcx().span_err(rustc_internal::internal(tcx, span), msg);
 }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index e9edbedfcd82..32425204d76a 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -141,7 +141,7 @@ impl<'tcx> KaniAttributes<'tcx> {
 
     /// Look up the attributes by a stable MIR DefID
     pub fn for_def_id(tcx: TyCtxt<'tcx>, def_id: StableDefId) -> Self {
-        KaniAttributes::for_item(tcx, rustc_internal::internal(def_id))
+        KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, def_id))
     }
 
     pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
@@ -671,7 +671,7 @@ pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool {
 /// Same as [`KaniAttributes::is_harness`] but more efficient because less
 /// attribute parsing is performed.
 pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {
-    let def_id = rustc_internal::internal(instance.def.def_id());
+    let def_id = rustc_internal::internal(tcx, instance.def.def_id());
     has_kani_attribute(tcx, def_id, |a| {
         matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract)
     })
@@ -679,14 +679,14 @@ pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {
 
 /// Does this `def_id` have `#[rustc_test_marker]`?
 pub fn is_test_harness_description(tcx: TyCtxt, item: impl CrateDef) -> bool {
-    let def_id = rustc_internal::internal(item.def_id());
+    let def_id = rustc_internal::internal(tcx, item.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker)
 }
 
 /// Extract the test harness name from the `#[rustc_test_maker]`
 pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String {
-    let def_id = rustc_internal::internal(def.def_id());
+    let def_id = rustc_internal::internal(tcx, def.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap();
     parse_str_value(&marker).unwrap()
@@ -944,7 +944,7 @@ fn parse_integer(attr: &Attribute) -> Option<u128> {
     if attr_args.len() == 1 {
         let x = attr_args[0].lit()?;
         match x.kind {
-            LitKind::Int(y, ..) => Some(y),
+            LitKind::Int(y, ..) => Some(y.get()),
             _ => None,
         }
     }
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 85d59215d661..94879b5b65e6 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -66,8 +66,8 @@ pub fn extract_unsize_casting_stable(
 ) -> CoercionBaseStable {
     let CoercionBase { src_ty, dst_ty } = extract_unsize_casting(
         tcx,
-        rustc_internal::internal(src_ty),
-        rustc_internal::internal(dst_ty),
+        rustc_internal::internal(tcx, src_ty),
+        rustc_internal::internal(tcx, dst_ty),
     );
     CoercionBaseStable {
         src_ty: rustc_internal::stable(src_ty),
@@ -90,11 +90,11 @@ pub fn extract_unsize_casting<'tcx>(
     .last()
     .unwrap();
     // Extract the pointee type that is being coerced.
-    let src_pointee_ty = extract_pointee(coerce_info.src_ty).expect(&format!(
+    let src_pointee_ty = extract_pointee(tcx, coerce_info.src_ty).expect(&format!(
         "Expected source to be a pointer. Found {:?} instead",
         coerce_info.src_ty
     ));
-    let dst_pointee_ty = extract_pointee(coerce_info.dst_ty).expect(&format!(
+    let dst_pointee_ty = extract_pointee(tcx, coerce_info.dst_ty).expect(&format!(
         "Expected destination to be a pointer. Found {:?} instead",
         coerce_info.dst_ty
     ));
@@ -216,8 +216,8 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
 
                 let CustomCoerceUnsized::Struct(coerce_index) = custom_coerce_unsize_info(
                     self.tcx,
-                    rustc_internal::internal(src_ty),
-                    rustc_internal::internal(dst_ty),
+                    rustc_internal::internal(self.tcx, src_ty),
+                    rustc_internal::internal(self.tcx, dst_ty),
                 );
                 let coerce_index = coerce_index.as_usize();
                 assert!(coerce_index < src_fields.len());
@@ -229,7 +229,7 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
             _ => {
                 // Base case is always a pointer (Box, raw_pointer or reference).
                 assert!(
-                    extract_pointee(src_ty).is_some(),
+                    extract_pointee(self.tcx, src_ty).is_some(),
                     "Expected a pointer, but found {src_ty:?}"
                 );
                 None
@@ -262,6 +262,6 @@ fn custom_coerce_unsize_info<'tcx>(
 }
 
 /// Extract pointee type from builtin pointer types.
-fn extract_pointee<'tcx>(typ: TyStable) -> Option<Ty<'tcx>> {
-    rustc_internal::internal(typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
+fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option<Ty<'_>> {
+    rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
 }
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 66fb2ca0aa33..e65befc9624e 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -92,7 +92,10 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
         // We don't short circuit here since this is a type check and can shake
         // out differently depending on generic parameters.
         if let MonoItem::Fn(instance) = item {
-            if attributes::is_function_contract_generated(tcx, rustc_internal::internal(def_id)) {
+            if attributes::is_function_contract_generated(
+                tcx,
+                rustc_internal::internal(tcx, def_id),
+            ) {
                 check_is_contract_safe(tcx, *instance);
             }
         }
@@ -167,7 +170,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
     for var in &bound_fn_sig.bound_vars {
         if let BoundVariableKind::Ty(t) = var {
             tcx.dcx().span_err(
-                rustc_internal::internal(instance.def.span()),
+                rustc_internal::internal(tcx, instance.def.span()),
                 format!("Found a bound type variable {t:?} after monomorphization"),
             );
         }
@@ -211,7 +214,8 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
         // For each def_id, dump their MIR
         for (item, def_id) in items.iter().filter_map(visible_item) {
             writeln!(writer, "// Item: {item:?}").unwrap();
-            write_mir_pretty(tcx, Some(rustc_internal::internal(def_id)), &mut writer).unwrap();
+            write_mir_pretty(tcx, Some(rustc_internal::internal(tcx, def_id)), &mut writer)
+                .unwrap();
         }
     }
 }
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 424077a622f9..63ed41bfd4c1 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -75,7 +75,7 @@ where
         .filter_map(|item| {
             // Only collect monomorphic items.
             // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released.
-            let def_id = rustc_internal::internal(item.def_id());
+            let def_id = rustc_internal::internal(tcx, item.def_id());
             (matches!(tcx.def_kind(def_id), rustc_hir::def::DefKind::Ctor(..))
                 || matches!(item.kind(), ItemKind::Fn))
             .then(|| {
@@ -237,7 +237,8 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
             let poly_trait_ref = principal.with_self_ty(concrete_ty);
 
             // Walk all methods of the trait, including those of its supertraits
-            let entries = self.tcx.vtable_entries(rustc_internal::internal(&poly_trait_ref));
+            let entries =
+                self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref));
             let methods = entries.iter().filter_map(|entry| match entry {
                 VtblEntry::MetadataAlign
                 | VtblEntry::MetadataDropInPlace
@@ -395,9 +396,10 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                             let caller = CrateItem::try_from(*self.instance).unwrap().name();
                             let callee = fn_def.name();
                             // Check if the current function has been stubbed.
-                            if let Some(stub) =
-                                get_stub(self.tcx, rustc_internal::internal(self.instance).def_id())
-                            {
+                            if let Some(stub) = get_stub(
+                                self.tcx,
+                                rustc_internal::internal(self.tcx, self.instance).def_id(),
+                            ) {
                                 // During the MIR stubbing transformation, we do not
                                 // force type variables in the stub's signature to
                                 // implement the same traits as those in the
@@ -413,7 +415,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                 let sep = callee.rfind("::").unwrap();
                                 let trait_ = &callee[..sep];
                                 self.tcx.dcx().span_err(
-                                    rustc_internal::internal(terminator.span),
+                                    rustc_internal::internal(self.tcx, terminator.span),
                                     format!(
                                         "`{}` doesn't implement \
                                         `{}`. The function `{}` \
@@ -465,8 +467,8 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
 fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) {
     let CoercionBase { src_ty, dst_ty } = coercion::extract_unsize_casting(
         tcx,
-        rustc_internal::internal(orig_ty),
-        rustc_internal::internal(dst_trait),
+        rustc_internal::internal(tcx, orig_ty),
+        rustc_internal::internal(tcx, dst_trait),
     );
     (rustc_internal::stable(src_ty), rustc_internal::stable(dst_ty))
 }
@@ -476,7 +478,7 @@ fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty)
 fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint {
     tcx.with_stable_hashing_context(|mut hcx| {
         let mut hasher = StableHasher::new();
-        rustc_internal::internal(item).hash_stable(&mut hcx, &mut hasher);
+        rustc_internal::internal(tcx, item).hash_stable(&mut hcx, &mut hasher);
         hasher.finish()
     })
 }
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index e88485ebc6d7..53670bfd482d 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -399,8 +399,11 @@ fn resolve_in_type<'tcx>(
     name: &str,
 ) -> Result<DefId, ResolveError<'tcx>> {
     debug!(?name, ?type_id, "resolve_in_type");
+    let missing_item_err =
+        || ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() };
     // Try the inherent `impl` blocks (i.e., non-trait `impl`s).
     tcx.inherent_impls(type_id)
+        .map_err(|_| missing_item_err())?
         .iter()
         .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id))
         .cloned()
@@ -409,9 +412,5 @@ fn resolve_in_type<'tcx>(
             let last = item_path.split("::").last().unwrap();
             last == name
         })
-        .ok_or_else(|| ResolveError::MissingItem {
-            tcx,
-            base: type_id,
-            unresolved: name.to_string(),
-        })
+        .ok_or_else(missing_item_err)
 }
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index 9dda0144eda4..0db518ceef9f 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -27,7 +27,7 @@ pub fn harness_stub_map(
     harness: Instance,
     metadata: &HarnessMetadata,
 ) -> BTreeMap<DefPathHash, DefPathHash> {
-    let def_id = rustc_internal::internal(harness.def.def_id());
+    let def_id = rustc_internal::internal(tcx, harness.def.def_id());
     let attrs = &metadata.attributes;
     let mut stub_pairs = BTreeMap::default();
     for stubs in &attrs.stubs {
@@ -44,7 +44,7 @@ pub fn harness_stub_map(
 /// In stable MIR, trying to retrieve an `Instance::body()` will ICE if we cannot evaluate a
 /// constant as expected. For now, use internal APIs to anticipate this issue.
 pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
-    let internal_instance = rustc_internal::internal(instance);
+    let internal_instance = rustc_internal::internal(tcx, instance);
     if get_stub(tcx, internal_instance.def_id()).is_some() {
         debug!(?instance, "validate_instance");
         let item = CrateItem::try_from(instance).unwrap();
@@ -87,7 +87,7 @@ impl<'tcx> StubConstChecker<'tcx> {
 impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
     /// Collect constants that are represented as static variables.
     fn visit_constant(&mut self, constant: &Constant, location: Location) {
-        let const_ = self.monomorphize(rustc_internal::internal(&constant.literal));
+        let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.literal));
         debug!(?constant, ?location, ?const_, "visit_constant");
         match const_ {
             Const::Val(..) | Const::Ty(..) => {}
@@ -109,7 +109,7 @@ impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
                         tcx.def_path_str(trait_),
                         self.source.name()
                     );
-                    tcx.dcx().span_err(rustc_internal::internal(location.span()), msg);
+                    tcx.dcx().span_err(rustc_internal::internal(self.tcx, location.span()), msg);
                     self.is_valid = false;
                 }
             }
diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index f02eaa627477..98f52c19d9e7 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -11,7 +11,7 @@ use syn::ItemFn;
 use super::{
     helpers::*,
     shared::{attach_require_kani_any, identifier_for_generated_function},
-    ContractConditionsData, ContractConditionsHandler,
+    ContractConditionsHandler,
 };
 
 impl<'a> ContractConditionsHandler<'a> {
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 2914c0609c1a..510d3e13b50b 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-01-17"
+channel = "nightly-2024-01-23"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs
index 9e76a55a2cb3..ba482248898c 100644
--- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs
+++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs
@@ -30,13 +30,13 @@ fn main() {
         assert!(min_align_of_val(&0i16) == 2);
         assert!(min_align_of_val(&0i32) == 4);
         assert!(min_align_of_val(&0i64) == 8);
-        assert!(min_align_of_val(&0i128) == 8);
+        assert!(min_align_of_val(&0i128) == 16);
         assert!(min_align_of_val(&0isize) == 8);
         assert!(min_align_of_val(&0u8) == 1);
         assert!(min_align_of_val(&0u16) == 2);
         assert!(min_align_of_val(&0u32) == 4);
         assert!(min_align_of_val(&0u64) == 8);
-        assert!(min_align_of_val(&0u128) == 8);
+        assert!(min_align_of_val(&0u128) == 16);
         assert!(min_align_of_val(&0usize) == 8);
         assert!(min_align_of_val(&0f32) == 4);
         assert!(min_align_of_val(&0f64) == 8);
diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs
index e1b3e1dd4491..426f09de1a59 100644
--- a/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs
+++ b/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs
@@ -19,7 +19,7 @@ fn check_align_simple() {
     let a = A { id: 0 };
     let t: &dyn T = &a;
     #[cfg(target_arch = "x86_64")]
-    assert_eq!(align_of_val(t), 8);
+    assert_eq!(align_of_val(t), 16);
     #[cfg(target_arch = "aarch64")]
     assert_eq!(align_of_val(t), 16);
     assert_eq!(align_of_val(&t), 8);
diff --git a/tests/kani/Intrinsics/ConstEval/min_align_of.rs b/tests/kani/Intrinsics/ConstEval/min_align_of.rs
index eed572b8dc9f..425f27084076 100644
--- a/tests/kani/Intrinsics/ConstEval/min_align_of.rs
+++ b/tests/kani/Intrinsics/ConstEval/min_align_of.rs
@@ -19,13 +19,13 @@ fn main() {
         assert!(min_align_of::<i16>() == 2);
         assert!(min_align_of::<i32>() == 4);
         assert!(min_align_of::<i64>() == 8);
-        assert!(min_align_of::<i128>() == 8);
+        assert!(min_align_of::<i128>() == 16);
         assert!(min_align_of::<isize>() == 8);
         assert!(min_align_of::<u8>() == 1);
         assert!(min_align_of::<u16>() == 2);
         assert!(min_align_of::<u32>() == 4);
         assert!(min_align_of::<u64>() == 8);
-        assert!(min_align_of::<u128>() == 8);
+        assert!(min_align_of::<u128>() == 16);
         assert!(min_align_of::<usize>() == 8);
         assert!(min_align_of::<f32>() == 4);
         assert!(min_align_of::<f64>() == 8);
diff --git a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs
index 22ff342a8198..d495bffef5f8 100644
--- a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs
+++ b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs
@@ -19,13 +19,13 @@ fn main() {
         assert!(unsafe { pref_align_of::<i16>() } == 2);
         assert!(unsafe { pref_align_of::<i32>() } == 4);
         assert!(unsafe { pref_align_of::<i64>() } == 8);
-        assert!(unsafe { pref_align_of::<i128>() } == 8);
+        assert!(unsafe { pref_align_of::<i128>() } == 16);
         assert!(unsafe { pref_align_of::<isize>() } == 8);
         assert!(unsafe { pref_align_of::<u8>() } == 1);
         assert!(unsafe { pref_align_of::<u16>() } == 2);
         assert!(unsafe { pref_align_of::<u32>() } == 4);
         assert!(unsafe { pref_align_of::<u64>() } == 8);
-        assert!(unsafe { pref_align_of::<u128>() } == 8);
+        assert!(unsafe { pref_align_of::<u128>() } == 16);
         assert!(unsafe { pref_align_of::<usize>() } == 8);
         assert!(unsafe { pref_align_of::<f32>() } == 4);
         assert!(unsafe { pref_align_of::<f64>() } == 8);
diff --git a/tests/perf/hashset/expected b/tests/perf/hashset/expected
index 8ba783d580f9..1fbcbbd13c25 100644
--- a/tests/perf/hashset/expected
+++ b/tests/perf/hashset/expected
@@ -1 +1 @@
-4 successfully verified harnesses, 0 failures, 4 total
+3 successfully verified harnesses, 0 failures, 3 total
diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs
index fb29db5c7ed6..e2f1fc16666a 100644
--- a/tests/perf/hashset/src/lib.rs
+++ b/tests/perf/hashset/src/lib.rs
@@ -1,11 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --enable-stubbing --enable-unstable
+// kani-flags: -Z stubbing
 //! Try to verify HashSet basic behavior.
 
 use std::collections::{hash_map::RandomState, HashSet};
 use std::mem::{size_of, size_of_val, transmute};
 
+#[allow(dead_code)]
 fn concrete_state() -> RandomState {
     let keys: [u64; 2] = [0, 0];
     assert_eq!(size_of_val(&keys), size_of::<RandomState>());
@@ -14,7 +15,7 @@ fn concrete_state() -> RandomState {
 
 #[kani::proof]
 #[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(kissat)]
 fn check_insert() {
     let mut set: HashSet<i32> = HashSet::default();
@@ -26,41 +27,29 @@ fn check_insert() {
 
 #[kani::proof]
 #[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(kissat)]
 fn check_contains() {
     let first = kani::any();
-    let mut set: HashSet<i8> = HashSet::from([first]);
+    let set: HashSet<i8> = HashSet::from([first]);
     assert!(set.contains(&first));
 }
 
 #[kani::proof]
 #[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
+#[kani::solver(kissat)]
 fn check_contains_str() {
-    let mut set = HashSet::from(["s"]);
+    let set = HashSet::from(["s"]);
     assert!(set.contains(&"s"));
 }
 
-#[kani::proof]
-#[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
-#[kani::solver(kissat)]
-fn check_insert_two_concrete() {
-    let mut set: HashSet<i32> = HashSet::default();
-    let first = 10;
-    let second = 20;
-    set.insert(first);
-    set.insert(second);
-    assert_eq!(set.len(), 2);
-}
-
 // too slow so don't run in the regression for now
 #[cfg(slow)]
 mod slow {
     #[kani::proof]
     #[kani::stub(RandomState::new, concrete_state)]
-    #[kani::unwind(3)]
+    #[kani::unwind(5)]
     fn check_insert_two_elements() {
         let mut set: HashSet<i8> = HashSet::default();
         let first = kani::any();
@@ -71,4 +60,17 @@ mod slow {
 
         if first == second { assert_eq!(set.len(), 1) } else { assert_eq!(set.len(), 2) }
     }
+
+    #[kani::proof]
+    #[kani::stub(RandomState::new, concrete_state)]
+    #[kani::unwind(5)]
+    #[kani::solver(kissat)]
+    fn check_insert_two_concrete() {
+        let mut set: HashSet<i32> = HashSet::default();
+        let first = 10;
+        let second = 20;
+        set.insert(first);
+        set.insert(second);
+        assert_eq!(set.len(), 2);
+    }
 }