diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
index 0ee1e00ba6f1..c0f95a881da1 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
@@ -36,8 +36,8 @@ use rustc_middle::util::Providers;
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::rustc_internal;
 use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::fs::File;
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 2512a95f36dd..4cf5dbb10e0b 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
@@ -56,17 +56,17 @@ use charon_lib::{error_assert, error_or_panic};
 use core::panic;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::{TyCtxt, TypingEnv};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::{Instance, InstanceDef};
 use stable_mir::mir::{
     AggregateKind, BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability,
     Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator,
     TerminatorKind, UnOp, VarDebugInfoContents,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     AdtDef, AdtKind, Allocation, ConstantKind, FnDef, GenericArgKind, GenericArgs,
-    GenericParamDefKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl,
-    TraitDef, Ty, TyConst, TyConstKind, TyKind, UintTy,
+    GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef,
+    Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
 use stable_mir::{CrateDef, CrateDefType, DefId};
 use std::collections::HashMap;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index b0583056b88b..f1f05b9b2509 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -6,10 +6,10 @@ use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::{Local, VarDebugInfoContents};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 
 impl GotocCtx<'_> {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index 2cd693fa2256..a59b73ffe602 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -241,8 +241,8 @@ pub mod rustc_smir {
     use rustc_middle::mir::coverage::BasicCoverageBlock;
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::ty::TyCtxt;
-    use rustc_smir::rustc_internal;
     use stable_mir::mir::mono::Instance;
+    use stable_mir::rustc_internal;
     use stable_mir::{Filename, Opaque};
 
     type CoverageOpaque = stable_mir::Opaque;
@@ -285,7 +285,7 @@ pub mod rustc_smir {
         instance: Instance,
     ) -> Option<(SourceRegion, Filename)> {
         // We need to pull the coverage info from the internal MIR instance.
-        let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
+        let instance_def = rustc_internal::internal(tcx, instance.def.def_id());
         let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
         let filename = rustc_internal::stable(body.span).get_filename();
         // Some functions, like `std` ones, may not have coverage info attached
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 6e896ee97288..62ef4fe32b09 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -10,9 +10,9 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::ty::TypingEnv;
 use rustc_middle::ty::layout::ValidityRequirement;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Operand, Place};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 9cafc55b3974..25bc02c07594 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -6,11 +6,11 @@ use crate::kani_middle::is_anon_static;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
 use rustc_middle::ty::Const as ConstInternal;
-use rustc_smir::rustc_internal;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
 use stable_mir::mir::{Mutability, Operand};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
     TyConst, TyConstKind, TyKind, UintTy,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 721082c20bd6..f1cfbb044544 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -14,8 +14,8 @@ use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
 use rustc_abi::{TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
 use tracing::{debug, trace, warn};
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index d7fcd4e2f964..ab0565dda05e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -20,12 +20,12 @@ use cbmc::{InternString, InternedString, btree_string_map};
 use num::bigint::BigInt;
 use rustc_abi::{FieldsShape, TagEncoding, Variants};
 use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry};
-use rustc_smir::rustc_internal;
 use stable_mir::abi::{Primitive, Scalar, ValueAbi};
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     Binder, ClosureKind, ExistentialPredicate, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy,
     VariantIdx,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index 178e0b7c5d07..bfa5ac9130af 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -7,8 +7,8 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
 use lazy_static::lazy_static;
 use rustc_hir::Attribute;
-use rustc_smir::rustc_internal;
 use rustc_span::Span;
+use stable_mir::rustc_internal;
 use stable_mir::ty::Span as SpanStable;
 use std::collections::HashMap;
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index e740cdf3ab96..eaae913f46cf 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -12,7 +12,6 @@ use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{List, TypingEnv};
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::mono::{Instance, InstanceKind};
@@ -20,6 +19,7 @@ use stable_mir::mir::{
     AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
     RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
 
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 7262f55a0719..e8939405e50c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -10,9 +10,9 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::abi::LayoutOf;
 use cbmc::goto_program::Type;
 use rustc_middle::ty::layout::{LayoutOf as _, TyAndLayout};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Local, Operand, Place, Rvalue};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnSig, RigidTy, Ty, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index d950d4262300..a84a6640d11c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -20,11 +20,11 @@ use rustc_middle::ty::{
 };
 use rustc_middle::ty::{ExistentialTraitRef, GenericArgsRef};
 use rustc_middle::ty::{List, TypeFoldable};
-use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::Body;
 use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
     Ty as StableTy,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 3446267281f7..9679a726516f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -37,11 +37,11 @@ use rustc_middle::util::Providers;
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-use rustc_smir::rustc_internal;
 use rustc_span::{Symbol, sym};
 use rustc_target::spec::PanicStrategy;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::rustc_internal;
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::fmt::Write;
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 16877ff6c18d..b59ffd47af25 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -5,10 +5,10 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
 use cbmc::goto_program::Stmt;
 use rustc_middle::ty::Instance as InstanceInternal;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Local, LocalDecl, Rvalue, visit::Location, visit::MirVisitor};
+use stable_mir::rustc_internal;
 use std::collections::{HashMap, HashSet};
 
 /// This structure represents useful data about the function we are currently compiling.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index e68a9ed50af2..742b804d0130 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -17,9 +17,9 @@ use cbmc::goto_program::CIntType;
 use cbmc::goto_program::Symbol as GotoSymbol;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Place};
+use stable_mir::rustc_internal;
 use stable_mir::ty::ClosureKind;
 use stable_mir::ty::RigidTy;
 use stable_mir::{CrateDef, ty::Span};
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index c9d4511d7453..adf69aa7ae49 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -5,7 +5,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type};
 use cbmc::{InternedString, btree_string_map};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
+use stable_mir::rustc_internal;
 use stable_mir::ty::Span;
 use tracing::debug;
 
diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index 25de67e45db2..ef8f244c9549 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -29,7 +29,7 @@ use rustc_driver::{Callbacks, Compilation, run_compiler};
 use rustc_interface::Config;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::ErrorOutputType;
-use rustc_smir::rustc_internal;
+use stable_mir::rustc_internal;
 use std::sync::{Arc, Mutex};
 use tracing::debug;
 
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 911e1682c143..3a1cf971752f 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -11,10 +11,10 @@ use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId};
 use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
-use rustc_smir::rustc_internal;
 use rustc_span::{Span, Symbol};
 use stable_mir::crate_def::Attribute as AttributeStable;
 use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::rustc_internal;
 use stable_mir::{CrateDef, DefId as StableDefId, Symbol as SymbolStable};
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 9f860bf80156..1411e77c44ff 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -27,9 +27,10 @@ use regex::RegexSet;
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
-use rustc_smir::rustc_internal;
+use rustc_smir::IndexedVal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, Ty, TyKind};
+use stable_mir::rustc_internal;
+use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index cc67cc886665..63c244b4aa41 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -18,9 +18,9 @@ use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv};
-use rustc_smir::rustc_internal;
 use rustc_span::DUMMY_SP;
 use stable_mir::Symbol;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use tracing::trace;
 
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 9f32820b2f75..98646d5324da 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -9,9 +9,9 @@ use crate::kani_queries::QueryDb;
 use fxhash::FxHashMap;
 use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::TerminatorKind;
 use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind,
 };
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
index fa8521ec1499..4bf4b4c2e4d4 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
@@ -41,9 +41,9 @@ use rustc_middle::{
     ty::{Instance, InstanceKind, List, TyCtxt, TyKind, TypingEnv},
 };
 use rustc_mir_dataflow::{Analysis, Forward, JoinSemiLattice};
-use rustc_smir::rustc_internal;
 use rustc_span::{DUMMY_SP, source_map::Spanned};
 use stable_mir::mir::{Body as StableBody, mono::Instance as StableInstance};
+use stable_mir::rustc_internal;
 use std::collections::HashSet;
 
 /// Main points-to analysis object.
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
index f27c53fcc3b0..2b661d4f1210 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
@@ -9,11 +9,11 @@ use rustc_middle::{
     ty::{Instance, List, TyCtxt},
 };
 use rustc_mir_dataflow::{JoinSemiLattice, fmt::DebugWithContext};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::{
     Place as StablePlace,
     mono::{Instance as StableInstance, StaticDef},
 };
+use stable_mir::rustc_internal;
 use std::collections::{HashMap, HashSet, VecDeque};
 
 /// A node in the points-to graph, which could be a place on the stack, a heap allocation, or a static.
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index f7d8768e0554..d692d3e96b71 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -23,7 +23,6 @@ use rustc_data_structures::fx::FxHashSet;
 use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
 use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_session::config::OutputType;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateItem;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
@@ -31,6 +30,7 @@ use stable_mir::mir::{
     Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator, TerminatorKind,
     visit::Location,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
 use stable_mir::{CrateDef, ItemKind};
 use std::fmt::{Display, Formatter};
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index b19f2da89d83..8e6cdc213e34 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -18,8 +18,8 @@ use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalMo
 use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::ty::fast_reject::{self, TreatParams};
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind};
 use std::collections::HashSet;
 use std::fmt;
diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs
index 50183634637d..7517cbe58c5d 100644
--- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs
+++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs
@@ -6,9 +6,9 @@ use crate::kani_middle::resolve::{ResolveError, resolve_path, validate_kind};
 use quote::ToTokens;
 use rustc_hir::def::DefKind;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use rustc_span::def_id::LocalDefId;
 use stable_mir::mir::Mutability;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FloatTy, IntTy, Region, RegionKind, RigidTy, Ty, UintTy};
 use std::str::FromStr;
 use strum_macros::{EnumString, IntoStaticStr};
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index 9235287852e1..210f419402c8 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -13,10 +13,10 @@ use kani_metadata::HarnessMetadata;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Const;
 use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::ConstOperand;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index a0be5477bd0d..22f2eac193a3 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -16,6 +16,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use fxhash::FxHashMap;
 use rustc_middle::ty::TyCtxt;
+use rustc_smir::IndexedVal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
@@ -23,8 +24,7 @@ use stable_mir::mir::{
     Terminator, TerminatorKind,
 };
 use stable_mir::ty::{
-    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, Ty, TyKind, UintTy,
-    VariantDef,
+    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind, UintTy, VariantDef,
 };
 use tracing::debug;
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
index 3cba12bf21ee..c07962f4696d 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
@@ -13,7 +13,7 @@ use crate::kani_middle::transform::{
 };
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
+use stable_mir::rustc_internal;
 use stable_mir::{
     CrateDef,
     mir::{Body, Mutability, Place, mono::Instance},
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
index 20a98d1b8e91..ac1dd155c567 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
@@ -5,10 +5,11 @@
 
 use std::fmt::Display;
 
+use rustc_smir::IndexedVal;
 use stable_mir::{
     abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape},
     target::{MachineInfo, MachineSize},
-    ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind, UintTy, VariantIdx},
+    ty::{AdtKind, RigidTy, Ty, TyKind, UintTy, VariantIdx},
 };
 
 /// Represents a chunk of data bytes in a data structure.
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index 988e01857afb..ec79d56c34a3 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -20,7 +20,7 @@ use crate::kani_middle::transform::body::{
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::{Const, TyCtxt};
-use rustc_smir::rustc_internal;
+use rustc_smir::IndexedVal;
 use stable_mir::CrateDef;
 use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange};
 use stable_mir::mir::mono::Instance;
@@ -30,8 +30,9 @@ use stable_mir::mir::{
     Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, Rvalue,
     Statement, StatementKind, Terminator, TerminatorKind,
 };
+use stable_mir::rustc_internal;
 use stable_mir::target::{MachineInfo, MachineSize};
-use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Span, Ty, TyKind, UintTy};
+use stable_mir::ty::{AdtKind, RigidTy, Span, Ty, TyKind, UintTy};
 use std::fmt::Debug;
 use strum_macros::AsRefStr;
 use tracing::{debug, trace};
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index c34d145790d1..a04fb9d4ca4b 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -11,13 +11,13 @@ use crate::kani_queries::QueryDb;
 use cbmc::{InternString, InternedString};
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use rustc_span::Symbol;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy};
 use std::collections::HashSet;
 use std::fmt::Debug;
diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs
index ad9d0906f313..77f87ff7bde3 100644
--- a/kani-compiler/src/kani_middle/transform/internal_mir.rs
+++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs
@@ -9,7 +9,6 @@
 
 use rustc_middle::mir::CoercionSource;
 use rustc_middle::ty::{self as rustc_ty, TyCtxt};
-use rustc_smir::rustc_internal::internal;
 use stable_mir::mir::{
     AggregateKind, AssertMessage, Body, BorrowKind, CastKind, ConstOperand, CopyNonOverlapping,
     CoroutineDesugaring, CoroutineKind, CoroutineSource, FakeBorrowKind, FakeReadCause, LocalDecl,
@@ -17,6 +16,7 @@ use stable_mir::mir::{
     Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, UnwindAction,
     UserTypeProjection, Variance,
 };
+use stable_mir::rustc_internal::internal;
 
 pub trait RustcInternalMir {
     type T<'tcx>;
diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
index 6dcaa7e1d6fe..9063f58c358c 100644
--- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
@@ -14,12 +14,12 @@ use crate::kani_middle::transform::body::{
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     BasicBlockIdx, BinOp, Body, ConstOperand, LocalDecl, Operand, Rvalue, StatementKind,
     Terminator, TerminatorKind,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     FnDef, GenericArgKind, GenericArgs, IntTy, MirConst, RigidTy, Span, Ty, TyKind, UintTy,
 };
@@ -62,7 +62,7 @@ impl TransformPass for RustcIntrinsicsPass {
     }
 }
 
-fn is_panic_function(tcx: &TyCtxt, def_id: rustc_smir::stable_mir::DefId) -> bool {
+fn is_panic_function(tcx: &TyCtxt, def_id: stable_mir::DefId) -> bool {
     let def_id = rustc_internal::internal(*tcx, def_id);
     Some(def_id) == tcx.lang_items().panic_fn()
         || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str)
diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs
index 1c96be291594..21e98aac8821 100644
--- a/kani-compiler/src/kani_middle/transform/stubs.rs
+++ b/kani-compiler/src/kani_middle/transform/stubs.rs
@@ -8,11 +8,11 @@ use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
 use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
 use std::collections::HashMap;
 use std::fmt::Debug;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 9e32c0a59e99..f615cfb52b28 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-07-04"
+channel = "nightly-2025-07-10"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs
index 9840c83e1abd..c25f86482f66 100644
--- a/tools/scanner/src/analysis.rs
+++ b/tools/scanner/src/analysis.rs
@@ -8,7 +8,6 @@ use csv::WriterBuilder;
 use graph_cycles::Cycles;
 use petgraph::graph::Graph;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use serde::{Serialize, Serializer, ser::SerializeStruct};
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
@@ -16,6 +15,7 @@ use stable_mir::mir::{
     BasicBlock, Body, CastKind, MirVisitor, Mutability, NonDivergingIntrinsic, ProjectionElem,
     Rvalue, Safety, Statement, StatementKind, Terminator, TerminatorKind,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{Abi, AdtDef, AdtKind, FnDef, GenericArgs, MirConst, RigidTy, Ty, TyKind};
 use stable_mir::visitor::{Visitable, Visitor};
 use stable_mir::{CrateDef, CrateItem};
diff --git a/tools/scanner/src/lib.rs b/tools/scanner/src/lib.rs
index 83ab1207ecfa..71fcaecbc4a1 100644
--- a/tools/scanner/src/lib.rs
+++ b/tools/scanner/src/lib.rs
@@ -18,14 +18,13 @@ extern crate rustc_interface;
 extern crate rustc_middle;
 extern crate rustc_session;
 #[macro_use]
-extern crate rustc_smir;
 extern crate stable_mir;
 
 use crate::analysis::OverallStats;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
-use rustc_smir::run_with_tcx;
 use stable_mir::CompilerError;
+use stable_mir::run_with_tcx;
 use std::ops::ControlFlow;
 use std::path::{Path, PathBuf};
 use std::process::ExitCode;