diff --git a/deny.toml b/deny.toml
index ab296ec67055..7661eacdae5f 100644
--- a/deny.toml
+++ b/deny.toml
@@ -14,6 +14,9 @@ ignore = [
     # `llbc` feature and not part of Kani releases.
     { id = "RUSTSEC-2024-0436", reason = "paste is unmaintained; only reached via charon" },
     { id = "RUSTSEC-2023-0089", reason = "atomic-polyfill is unmaintained; only reached via charon" },
+    # Unmaintained (not vulnerable): `unsafe-libyaml` is only reached through `serde_yaml` in
+    # compiletest, our test runner, which is not part of Kani releases.
+    { id = "RUSTSEC-2024-0449", reason = "unsafe-libyaml is unmaintained; only reached via serde_yaml in compiletest" },
 ]
 
 # This section is considered when running `cargo deny check licenses`
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
index 12ded90f6064..7027a17b6c10 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -1447,7 +1447,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 let internal = rustc_internal::internal(self.tcx, def_id);
                 let builtin = self
                     .tcx
-                    .is_lang_item(internal, rustc_hir::attrs::lang_items::LangItem::OwnedBox)
+                    .is_lang_item(internal, rustc_attr_ir::lang_items::LangItem::OwnedBox)
                     .then_some(CharonBuiltinAdt::Box);
                 CharonTy::new(CharonTyKind::Adt(CharonTypeDeclRef {
                     id: c_typedeclid,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index 9a6f33bd4027..d3f7958975df 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -7,7 +7,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::cache::{CacheEntry, cache_entry};
 use cbmc::goto_program::Location;
 use lazy_static::lazy_static;
-use rustc_hir::Attribute;
+use rustc_attr_ir::Attribute;
 use rustc_public::rustc_internal;
 use rustc_public::ty::Span as SpanStable;
 use rustc_span::Span;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 7ddb47730fef..9b8c3ce52526 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1558,6 +1558,11 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
             // `tcx.types` entry for it, and CBMC has no bfloat16 type either. rustc itself
             // declines to map this primitive back to a Rust type (`rustc_abi::layout::ty`).
             Float::F16B => unimplemented!("bfloat16 (`f16b`) is not supported by Kani"),
+            // PowerPC's double-double `long double`, which only exists on PowerPC targets. Kani
+            // supports none of them, and CBMC has no double-double type.
+            Float::PpcF128 => {
+                unimplemented!("PowerPC double-double (`ppcf128`) is not supported by Kani")
+            }
         }
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 0ff1f99b39ef..3cf72969979f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -17,7 +17,7 @@ use cbmc::goto_program::CIntType;
 use cbmc::goto_program::Symbol as GotoSymbol;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, StmtBody, SymbolValues, Type};
 use cbmc::{InternedString, goto_program::ExprValue};
-use rustc_hir::attrs::lang_items::LangItem;
+use rustc_attr_ir::lang_items::LangItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{BasicBlockIdx, Place};
diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs
index c6058a23cd7c..f91c7ff2c2ad 100644
--- a/kani-compiler/src/intrinsics.rs
+++ b/kani-compiler/src/intrinsics.rs
@@ -386,7 +386,7 @@ impl Intrinsic {
             }
             // For const eval of nullary intrinsics, see https://github.com/rust-lang/rust/pull/142839
             "needs_drop" => unreachable!(
-                "Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
+                "Expected nullary intrinsic `core::intrinsics::needs_drop` to be const-evaluated before codegen"
             ),
             // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
             "offset" => unreachable!(
@@ -438,7 +438,7 @@ impl Intrinsic {
                 Self::Transmute
             }
             "type_id" => unreachable!(
-                "Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
+                "Expected nullary intrinsic `core::intrinsics::reflection::type_id` to be const-evaluated before codegen"
             ),
             "type_name" => unreachable!(
                 "Expected nullary intrinsic `core::intrinsics::type_name` to be const-evaluated before codegen"
diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index 5c7d88a8abf8..fbfc465c1d5e 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -3,7 +3,7 @@
 
 //! This module defines all compiler extensions that form the Kani compiler.
 //!
-//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler`]),
+//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::compiler_entrypoint`]),
 //! which is used to implement stubs.
 //!
 //! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will
@@ -26,7 +26,7 @@ use crate::session::init_session;
 use clap::Parser;
 use rustc_ast::{ast, attr};
 use rustc_codegen_ssa::traits::CodegenBackend;
-use rustc_driver::{Callbacks, Compilation, run_compiler};
+use rustc_driver::{Callbacks, Compilation, compiler_entrypoint};
 use rustc_interface::Config;
 use rustc_interface::interface::Compiler;
 use rustc_middle::ty::TyCtxt;
@@ -106,7 +106,7 @@ const KANI_REQUIRED_RUSTC_ARGS: &[&str] = &[
 ];
 
 /// Run the Kani flavour of the compiler.
-/// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]).
+/// This may require multiple runs of the rustc driver ([`rustc_driver::compiler_entrypoint`]).
 pub fn run(mut args: Vec<String>) {
     args.extend(KANI_REQUIRED_RUSTC_ARGS.iter().map(|s| s.to_string()));
     let mut kani_compiler = KaniCompiler::new();
@@ -180,7 +180,7 @@ impl KaniCompiler {
     /// actually invoke the rust compiler multiple times.
     pub fn run(&mut self, args: Vec<String>) {
         debug!(?args, "run_compilation_session");
-        run_compiler(&args, self);
+        compiler_entrypoint(&args, self);
     }
 }
 
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index e04e8f6a5e53..be5302d5fe04 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -7,11 +7,10 @@ use std::collections::{BTreeMap, HashSet};
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{LitKind, MetaItem, MetaItemKind};
+use rustc_attr_ir::{AttrArgs, Attribute};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{
-    Attribute,
-    attrs::AttrArgs,
     def::DefKind,
     def_id::{DefId, LocalDefId},
 };
@@ -189,7 +188,7 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
-        // `get_all_attrs` is deprecated in favor of `rustc_hir::find_attr!`, but that
+        // `get_all_attrs` is deprecated in favor of `rustc_attr_ir::find_attr!`, but that
         // macro only matches parsed built-in attributes. Kani inspects `kanitool::*`
         // tool attributes, which are unparsed, so `get_all_attrs` is the correct API.
         #[allow(deprecated)]
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 5219243be50a..ef6a1a1be703 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -13,7 +13,7 @@
 //! definition of custom coercions for smart pointers can be found in the
 //! [RFC 982 DST Coercion](https://rust-lang.github.io/rfcs/0982-dst-coercion.html).
 
-use rustc_hir::attrs::lang_items::LangItem;
+use rustc_attr_ir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 7c24320940e6..aeb58c5e33b8 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -11,7 +11,7 @@ use crate::kani_middle::stable_fn_def;
 use quote::ToTokens;
 use rustc_hir::def::{DefKind, Res};
 use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModId};
-use rustc_hir::{ItemKind, UseKind};
+use rustc_hir::{ItemKind, UseKind, UseTree};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::ty::fast_reject::{self, TreatParams};
 use rustc_public::CrateDef;
@@ -533,11 +533,24 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> Rela
     // direct module items take precedence over foreign items.
     let result = tcx.hir_module_free_items(current_module).find_map(|item_id| {
         let item = tcx.hir_item(item_id);
+        // A `use` item is one tree of imports (`use a::{b, c::{d, *}}`), so look for `name`, and
+        // collect globs, at every level of it.
+        if let ItemKind::Use(tree) = item.kind {
+            let mut found = None;
+            visit_use_tree(&tree, &mut |tree| match tree.kind {
+                UseKind::Single(ident) if found.is_none() && ident.as_str() == name => {
+                    found =
+                        tree.prefix.res.present_items().filter_map(|res| res.opt_def_id()).next();
+                }
+                // Do not immediately try to resolve the path using this glob,
+                // since paths resolved via non-globs take precedence.
+                UseKind::Glob => glob_imports.extend(tree.prefix.res.present_items()),
+                UseKind::Single(_) | UseKind::Nested { .. } => {}
+            });
+            return found;
+        }
         if item.kind.ident().is_some_and(|ident| ident.as_str() == name) {
             match item.kind {
-                ItemKind::Use(use_path, UseKind::Single(_)) => {
-                    use_path.res.present_items().filter_map(|res| res.opt_def_id()).next()
-                }
                 ItemKind::ExternCrate(orig_name, _) => resolve_external(
                     tcx,
                     orig_name.as_ref().map(|sym| sym.as_str()).unwrap_or(name),
@@ -545,11 +558,6 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> Rela
                 _ => Some(item.owner_id.def_id.to_def_id()),
             }
         } else {
-            if let ItemKind::Use(use_path, UseKind::Glob) = item.kind {
-                // Do not immediately try to resolve the path using this glob,
-                // since paths resolved via non-globs take precedence.
-                glob_imports.extend(use_path.res.present_items());
-            }
             // Collect foreign items declared inside `extern` blocks so we can
             // search them if the name is not found as a direct module item.
             // This handles `extern "C" { fn foo(); }` where `foo` is a child
@@ -577,6 +585,18 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> Rela
     RelativeResolution::Globs(glob_imports)
 }
 
+/// Call `f` on `tree` and on every tree nested in it. Since nightly-2026-10-06, rustc keeps
+/// `use a::{b, c}` as one HIR item holding a tree of imports, where it used to lower it to one item
+/// per imported name (rust-lang/rust#161349), so every level has to be visited.
+fn visit_use_tree<'hir>(tree: &UseTree<'hir>, f: &mut impl FnMut(&UseTree<'hir>)) {
+    f(tree);
+    if let UseKind::Nested { items } = tree.kind {
+        for (nested, ..) in items {
+            visit_use_tree(nested, f);
+        }
+    }
+}
+
 /// Resolves a path relative to a local or foreign module.
 /// For local modules, if no module item matches the name we also have to traverse the list of glob
 /// imports. For foreign modules, that list should've been flatten already.
diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs
index 433968a737c8..3c68a20f5b7a 100644
--- a/kani-compiler/src/kani_middle/transform/internal_mir.rs
+++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs
@@ -546,6 +546,9 @@ impl RustcInternalMir for TerminatorKind {
         match self {
             TerminatorKind::Goto { target } => rustc_middle::mir::TerminatorKind::Goto {
                 target: rustc_middle::mir::BasicBlock::from_usize(*target),
+                // Loop hint attributes (`#[unroll]`) have no equivalent in the stable
+                // representation, and Kani-synthesized gotos carry none.
+                loop_hint_attrs: Default::default(),
             },
             TerminatorKind::SwitchInt { discr, targets } => {
                 rustc_middle::mir::TerminatorKind::SwitchInt {
@@ -607,9 +610,6 @@ impl RustcInternalMir for Terminator {
                 self.source_info.span,
             )),
             kind: self.kind.internal_mir(tcx),
-            // Terminators gained MIR-level attributes; the stable representation has no
-            // equivalent, and Kani-synthesized terminators carry none.
-            attributes: Default::default(),
         }
     }
 }
diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
index 68d8e2c4569a..f745873e3d1f 100644
--- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
@@ -13,7 +13,7 @@ use crate::kani_middle::transform::body::{
 };
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
-use rustc_hir::attrs::lang_items::LangItem;
+use rustc_attr_ir::lang_items::LangItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 77fa77176405..7c157288f71e 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -21,6 +21,7 @@
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;
+extern crate rustc_attr_ir;
 extern crate rustc_codegen_ssa;
 extern crate rustc_data_structures;
 extern crate rustc_driver;
@@ -55,7 +56,7 @@ mod kani_middle;
 mod kani_queries;
 mod session;
 
-use rustc_driver::{TimePassesCallbacks, run_compiler};
+use rustc_driver::{TimePassesCallbacks, compiler_entrypoint};
 use std::env;
 
 /// Main function. Configure arguments and run the compiler.
@@ -74,7 +75,7 @@ fn main() {
         kani_compiler::run(rustc_args);
     } else {
         let mut callbacks = TimePassesCallbacks::default();
-        run_compiler(&rustc_args, &mut callbacks);
+        compiler_entrypoint(&rustc_args, &mut callbacks);
     }
 }
 
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 9c0e54ea1a90..a585c73ebcf0 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2026-09-25"
+channel = "nightly-2026-10-11"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs
index 4c1d6b2fda42..0fc74a2f5c59 100644
--- a/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs
+++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Checks that `copy_nonoverlapping` triggers an overflow failure if the `count`
 //! argument can overflow a `usize`
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs
index bcfa5dae79a4..d3cb46ad5e06 100644
--- a/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs
+++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Check that `copy_nonoverlapping` fails if the `src`/`dst` regions overlap.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_with_overlap() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs
index 4ac12d74b708..18ce64a66598 100644
--- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs
+++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs
@@ -3,6 +3,12 @@
 
 //! Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
 
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs
index c891778d3ca2..e3bdb0b90894 100644
--- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs
+++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `copy_nonoverlapping` fails when `src` is not aligned.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs
index 744528b9c32a..01c24dfd6e2a 100644
--- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs
+++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Checks that `copy_nonoverlapping` fails when `src` is not valid for reads.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_invalid() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs
index 34c7832267e0..3634221b4929 100644
--- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs
+++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Checks that `copy_nonoverlapping` fails when `dst` is not valid for writes.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_invalid() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy/copy-overflow/main.rs b/tests/expected/intrinsics/copy/copy-overflow/main.rs
index 2688d8cffa48..8e9a0aa7591c 100644
--- a/tests/expected/intrinsics/copy/copy-overflow/main.rs
+++ b/tests/expected/intrinsics/copy/copy-overflow/main.rs
@@ -3,6 +3,13 @@
 
 // Checks that `copy` triggers an overflow failure if the `count` argument can
 // overflow a `usize`
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs b/tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs
index 4de1679a5332..10bcd67bbf99 100644
--- a/tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs
+++ b/tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `copy` fails when `dst` is not aligned.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy/copy-unaligned-src/main.rs b/tests/expected/intrinsics/copy/copy-unaligned-src/main.rs
index 15506ecd4b16..efad5ee38808 100644
--- a/tests/expected/intrinsics/copy/copy-unaligned-src/main.rs
+++ b/tests/expected/intrinsics/copy/copy-unaligned-src/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `copy` fails when `src` is not aligned.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs
index 202900933e00..5e2487b3825a 100644
--- a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs
+++ b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Checks that `copy` fails when `src` is not valid for reads.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_invalid() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs b/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs
index f68e9b2a807c..add68133df08 100644
--- a/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs
+++ b/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Checks that `copy` fails when `dst` is not valid for writes.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_invalid() {
     let arr: [i32; 3] = [0, 1, 0];
diff --git a/tests/expected/intrinsics/write_bytes/unaligned/main.rs b/tests/expected/intrinsics/write_bytes/unaligned/main.rs
index b2d207500695..93c8cc9b3ce2 100644
--- a/tests/expected/intrinsics/write_bytes/unaligned/main.rs
+++ b/tests/expected/intrinsics/write_bytes/unaligned/main.rs
@@ -4,6 +4,13 @@
 //! Checks that `write_bytes` fails when `dst` is not aligned.
 //! This test is a modified version of the example in
 //! https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 use std::intrinsics::write_bytes;
 
 #[kani::proof]
diff --git a/tests/expected/valid-value-checks/write_invalid.rs b/tests/expected/valid-value-checks/write_invalid.rs
index 677ffe4edf61..d820409bc23f 100644
--- a/tests/expected/valid-value-checks/write_invalid.rs
+++ b/tests/expected/valid-value-checks/write_invalid.rs
@@ -6,6 +6,12 @@
 //! Writing invalid bytes is not UB as long as the incorrect value is not read.
 //! However, we over-approximate for sake of simplicity and performance.
 
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 use std::num::NonZeroU8;
 
 #[kani::proof]
diff --git a/tests/kani/Intrinsics/ConstEval/type_id.rs b/tests/kani/Intrinsics/ConstEval/type_id.rs
index 9c2358997fd4..ce3b253aa8fb 100644
--- a/tests/kani/Intrinsics/ConstEval/type_id.rs
+++ b/tests/kani/Intrinsics/ConstEval/type_id.rs
@@ -4,7 +4,7 @@
 // Check that the `type_id` intrinsic is supported with common data types
 // and that there are no duplicate type IDs
 #![feature(core_intrinsics)]
-use std::intrinsics::type_id;
+use std::intrinsics::reflection::type_id;
 
 struct MyStruct {}
 
diff --git a/tests/kani/Intrinsics/Copy/copy.rs b/tests/kani/Intrinsics/Copy/copy.rs
index 9fb86b130496..f06a15014e1c 100644
--- a/tests/kani/Intrinsics/Copy/copy.rs
+++ b/tests/kani/Intrinsics/Copy/copy.rs
@@ -4,6 +4,12 @@
 // Check that `copy` works as expected: Copies a number `n` of elements from
 // pointer `src` to pointer `dst`, even if their regions overlap.
 
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_simple() {
     let mut expected_val = 42;
diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs
index bec748bfa7a3..09caad64d438 100644
--- a/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs
+++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs
@@ -5,6 +5,12 @@
 // pointer `src` to pointer `dst`. Their regions of memory do not overlap, otherwise the
 // call to `copy_nonoverlapping` would fail (a separate test checks for this).
 
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_simple() {
     let mut expected_val = 42;
diff --git a/tests/kani/Stubbing/resolve_use_nested.rs b/tests/kani/Stubbing/resolve_use_nested.rs
new file mode 100644
index 000000000000..44bf11f4da5c
--- /dev/null
+++ b/tests/kani/Stubbing/resolve_use_nested.rs
@@ -0,0 +1,116 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --harness my_mod::harness -Z stubbing
+//
+//! This tests whether we take into account names imported through use lists (`use a::{b, c}`)
+//! when resolving paths in `kani::stub` attributes, including renames, globs and nested lists
+//! inside a list. Since nightly-2026-10-06, rustc keeps such a `use` as one HIR item with a tree
+//! of imports, instead of lowering it to one item per imported name.
+
+fn magic_number13() -> u32 {
+    13
+}
+
+struct MyType {}
+
+impl MyType {
+    fn magic_number101() -> u32 {
+        101
+    }
+}
+
+mod numbers {
+    pub fn magic_number7() -> u32 {
+        7
+    }
+
+    pub mod deep {
+        pub fn magic_number9() -> u32 {
+            9
+        }
+    }
+
+    pub mod globbed {
+        pub fn magic_number5() -> u32 {
+            5
+        }
+    }
+}
+
+mod my_mod {
+    use self::inner_mod::{
+        magic_number42,
+        nested::{magic_number21, magic_number22},
+    };
+    use super::numbers::{deep::magic_number9, globbed::*, magic_number7 as seven};
+    use super::{MyType, magic_number13};
+
+    mod inner_mod {
+        pub fn magic_number42() -> u32 {
+            42
+        }
+
+        pub mod nested {
+            pub fn magic_number21() -> u32 {
+                21
+            }
+
+            pub fn magic_number22() -> u32 {
+                22
+            }
+        }
+    }
+
+    #[kani::proof]
+    #[kani::stub(zero, magic_number13)]
+    #[kani::stub(one, magic_number42)]
+    #[kani::stub(two, MyType::magic_number101)]
+    #[kani::stub(three, seven)]
+    #[kani::stub(four, magic_number9)]
+    #[kani::stub(five, magic_number5)]
+    #[kani::stub(six, magic_number21)]
+    #[kani::stub(seventh, magic_number22)]
+    fn harness() {
+        assert_eq!(zero(), magic_number13());
+        assert_eq!(one(), magic_number42());
+        assert_eq!(two(), MyType::magic_number101());
+        assert_eq!(three(), seven());
+        assert_eq!(four(), magic_number9());
+        assert_eq!(five(), magic_number5());
+        assert_eq!(six(), magic_number21());
+        assert_eq!(seventh(), magic_number22());
+    }
+
+    fn zero() -> u32 {
+        0
+    }
+
+    fn one() -> u32 {
+        1
+    }
+
+    fn two() -> u32 {
+        2
+    }
+
+    fn three() -> u32 {
+        3
+    }
+
+    fn four() -> u32 {
+        4
+    }
+
+    fn five() -> u32 {
+        5
+    }
+
+    fn six() -> u32 {
+        6
+    }
+
+    fn seventh() -> u32 {
+        7
+    }
+}
diff --git a/tests/ui/ice-size-overflow/expected b/tests/ui/ice-size-overflow/expected
index a77dcabe7552..52b4003a6450 100644
--- a/tests/ui/ice-size-overflow/expected
+++ b/tests/ui/ice-size-overflow/expected
@@ -1,6 +1,8 @@
 error[E0080]: values of the type `[u8; usize::MAX]` are too big for the target architecture\
 lib/rustlib/src/rust/library/core/src/mem/mod.rs\
 |\
+pub trait SizedTypeProperties: Sized {\
+...\
 const SIZE: usize = intrinsics::size_of::<Self>();\
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation of `<S<u8> as std::mem::SizedTypeProperties>::SIZE` failed here\