diff --git a/.gitignore b/.gitignore
index 2f7896d1..9abd5824 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,4 @@
 target/
+mir_dump/
+*.mir
+rust_out
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 56e7f16a..d29b2337 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-09-08"
+channel = "nightly-2026-03-08"
 components = [ "rustc-dev", "rust-src", "llvm-tools-preview", "rust-analyzer" ]
diff --git a/src/analyze.rs b/src/analyze.rs
index 9339b1da..1061135c 100644
--- a/src/analyze.rs
+++ b/src/analyze.rs
@@ -34,10 +34,16 @@ mod local_def;
 // TODO: organize structure and remove cross dependency between refine
 pub use did_cache::DefIdCache;
 
-pub fn mir_borrowck_skip_formula_fn(
-    tcx: rustc_middle::ty::TyCtxt<'_>,
+pub fn mir_borrowck_skip_formula_fn<'tcx>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
     local_def_id: rustc_span::def_id::LocalDefId,
-) -> rustc_middle::query::queries::mir_borrowck::ProvidedValue<'_> {
+) -> Result<
+    &'tcx rustc_data_structures::fx::FxIndexMap<
+        rustc_span::def_id::LocalDefId,
+        rustc_middle::ty::DefinitionSiteHiddenType<'tcx>,
+    >,
+    rustc_span::ErrorGuaranteed,
+> {
     // TODO: unify impl with local_def::Analyzer
     // if the def is closure defined in formula_fn
     let root_def_id = tcx.typeck_root_def_id(local_def_id.to_def_id());
@@ -52,8 +58,9 @@ pub fn mir_borrowck_skip_formula_fn(
 
     if is_annotated_as_formula_fn {
         tracing::debug!(?local_def_id, "skipping borrow check for formula fn");
-        let dummy_result = rustc_middle::mir::ConcreteOpaqueTypes(Default::default());
-        return Ok(tcx.arena.alloc(dummy_result));
+        return Ok(tcx
+            .arena
+            .alloc(rustc_data_structures::fx::FxIndexMap::default()));
     }
 
     (rustc_interface::DEFAULT_QUERY_PROVIDERS
diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index eb2e7cb9..d5d780b8 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -354,6 +354,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let ty = match &operand {
             Operand::Copy(place) | Operand::Move(place) => self.env.place_type(*place),
             Operand::Constant(operand) => self.const_ty(&operand.const_),
+            Operand::RuntimeChecks(_) => {
+                PlaceTypeBuilder::default().build(rty::Type::bool(), chc::Term::bool(false))
+            }
         };
         tracing::debug!(operand = ?operand, ty = %ty.display(), "operand_type");
         ty
@@ -485,7 +488,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             }
             Rvalue::Cast(
                 mir::CastKind::PointerCoercion(
-                    mir_ty::adjustment::PointerCoercion::ReifyFnPointer,
+                    mir_ty::adjustment::PointerCoercion::ReifyFnPointer(_),
                     _,
                 ),
                 operand,
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index 1b05008b..188c8ef2 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -294,7 +294,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             .tcx
             .opt_associated_item(self.local_def_id.to_def_id())?;
         let trait_item_id = impl_item_assoc
-            .trait_item_def_id
+            .trait_item_def_id()
             .and_then(|id| id.as_local())?;
 
         if trait_item_id == self.local_def_id {
@@ -311,11 +311,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             return None;
         }
 
-        let trait_ref = self.tcx.impl_trait_ref(impl_did)?.instantiate_identity();
+        let trait_ref = self
+            .tcx
+            .impl_opt_trait_ref(impl_did)?
+            .instantiate_identity();
         let trait_item_did = self
             .tcx
             .associated_item(self.local_def_id.to_def_id())
-            .trait_item_def_id
+            .trait_item_def_id()
             .unwrap();
         self.ctx.def_ty_with_args(trait_item_did, trait_ref.args)
     }
@@ -526,6 +529,42 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             return Some((lhs_local, *place));
         }
 
+        // nightly-2026+: CopyForDeref was replaced by plain Use(Copy(place)) for &mut T.
+        // Detect copies of &mut T reached through struct-field projections — these are deref
+        // aliases created so the result can be immediately dereffed (e.g. closure captures).
+        // We require a non-empty projection ending with a Field to avoid matching plain
+        // copies like `return_val = copy param` which are genuine transfers, not deref aliases.
+        if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
+            let proj = place.projection.as_slice();
+            if let Some(mir::ProjectionElem::Field(..)) = proj.last() {
+                let place_ty = place.ty(&self.body.local_decls, self.tcx).ty;
+                if matches!(
+                    place_ty.kind(),
+                    mir_ty::TyKind::Ref(_, _, mir::Mutability::Mut)
+                ) {
+                    return Some((lhs_local, *place));
+                }
+            }
+        }
+
+        // nightly-2026+: box deref uses plain `copy (*box_local)` instead of CopyForDeref.
+        // Box<T> is not Copy, so `lhs = copy <box-place>` in optimized MIR must be the
+        // elaborated box deref pattern (reaching through the raw pointer alias from Transmute).
+        // The box may be reached through a reference (e.g. `copy (*ref_to_box)`), so we check
+        // the type of the full place after projections, not just the local's type.
+        if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
+            if let Some((rest, [mir::ProjectionElem::Deref])) =
+                place.projection.as_slice().split_last_chunk::<1>()
+            {
+                if rest.is_empty() {
+                    let place_ty = place.ty(&self.body.local_decls, self.tcx).ty;
+                    if place_ty.is_box() {
+                        return Some((lhs_local, *place));
+                    }
+                }
+            }
+        }
+
         let unique_did = self.ctx.def_ids.unique()?;
         let nonnull_did = self.ctx.def_ids.nonnull()?;
 
@@ -533,8 +572,38 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         use rustc_abi::FieldIdx;
         const ZERO_FIELD: FieldIdx = FieldIdx::from_u32(0);
 
+        // nightly-2026+: box deref split into two statements. The pre-optimization MIR copies
+        // the NonNull field directly (instead of going through CopyForDeref/Transmute chain):
+        //   _nonnull = copy box_place.Field(0, Unique<T>).Field(0, NonNull<T>)
+        //   _ptr     = Transmute(_nonnull) as *const T
+        // Detect the first statement and map _nonnull → box_place so the Transmute can be handled.
+        if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
+            if let Some((rest, [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1)])) =
+                place.projection.as_slice().split_last_chunk::<2>()
+            {
+                let rest_place = mir::Place {
+                    local: place.local,
+                    projection: self.tcx.mk_place_elems(rest),
+                };
+                let local_ty = rest_place.ty(&self.body.local_decls, self.tcx).ty;
+                if local_ty.is_box() {
+                    if let Some(inner_ty) = local_ty.boxed_ty() {
+                        if matches!(ty0.kind(), mir_ty::TyKind::Adt(def, args)
+                                if def.did() == unique_did && args.type_at(0) == inner_ty)
+                            && matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args)
+                                if def.did() == nonnull_did && args.type_at(0) == inner_ty)
+                        {
+                            return Some((lhs_local, rest_place));
+                        }
+                    }
+                }
+            }
+        }
+
         // Box deref pattern: `(_box.0.0 as *const T) Transmute`
-        //   projection = [..., Field(0, Unique<T>), Field(0, NonNull<T>)], transmuted to *const T
+        // Two variants:
+        //   Old: projection = [..., Field(0, Unique<T>), Field(0, NonNull<T>)], transmuted to *const T
+        //   New (nightly-2026+): operand is a Box<T> local (NonNull was pre-fetched separately)
         let mir::Rvalue::Cast(mir::CastKind::Transmute, mir::Operand::Copy(place), cast_ty) =
             &rvalue
         else {
@@ -543,31 +612,33 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         if !matches!(cast_ty.kind(), mir_ty::TyKind::RawPtr(_, mutbl) if mutbl.is_not()) {
             return None;
         }
-        let Some((rest, [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1)])) =
+        // Old pattern: last two projections are Field(0,Unique).Field(0,NonNull).
+        if let Some((rest, [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1)])) =
             place.projection.as_slice().split_last_chunk::<2>()
-        else {
-            return None;
-        };
-        let rest_place = mir::Place {
-            local: place.local,
-            projection: self.tcx.mk_place_elems(rest),
-        };
-        let local_ty = rest_place.ty(&self.body.local_decls, self.tcx).ty;
-        if !local_ty.is_box() {
-            return None;
-        }
-        let inner_ty = local_ty.boxed_ty()?;
-        if !matches!(ty0.kind(), mir_ty::TyKind::Adt(def, args)
-            if def.did() == unique_did && args.type_at(0) == inner_ty)
         {
-            return None;
+            let rest_place = mir::Place {
+                local: place.local,
+                projection: self.tcx.mk_place_elems(rest),
+            };
+            let local_ty = rest_place.ty(&self.body.local_decls, self.tcx).ty;
+            if local_ty.is_box() {
+                if let Some(inner_ty) = local_ty.boxed_ty() {
+                    if matches!(ty0.kind(), mir_ty::TyKind::Adt(def, args)
+                            if def.did() == unique_did && args.type_at(0) == inner_ty)
+                        && matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args)
+                            if def.did() == nonnull_did && args.type_at(0) == inner_ty)
+                    {
+                        return Some((lhs_local, rest_place));
+                    }
+                }
+            }
         }
-        if !matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args)
-            if def.did() == nonnull_did && args.type_at(0) == inner_ty)
-        {
-            return None;
+        // New pattern (nightly-2026+): operand is already a Box<T> (after NonNull pre-fetch).
+        let place_ty = place.ty(&self.body.local_decls, self.tcx).ty;
+        if place_ty.is_box() {
+            return Some((lhs_local, *place));
         }
-        Some((lhs_local, rest_place))
+        None
     }
 
     fn unelaborate_derefs(&mut self) {
diff --git a/src/main.rs b/src/main.rs
index 960ebc1b..a6977abc 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -20,7 +20,7 @@ impl Callbacks for CompilerCalls {
         attrs.push("register_tool(thrust)".to_owned());
 
         config.override_queries = Some(|_sess, providers| {
-            providers.mir_borrowck = thrust::mir_borrowck_skip_formula_fn;
+            providers.queries.mir_borrowck = thrust::mir_borrowck_skip_formula_fn;
         });
     }
 
@@ -38,10 +38,14 @@ impl Callbacks for CompilerCalls {
             &compiler.sess.psess,
             rustc_span::FileName::Custom("thrust std injected".to_string()),
             injected.to_owned(),
+            rustc_parse::lexer::StripTokens::Nothing,
         )
         .unwrap();
         while let Some(item) = parser
-            .parse_item(rustc_parse::parser::ForceCollect::No)
+            .parse_item(
+                rustc_parse::parser::ForceCollect::No,
+                rustc_parse::parser::AllowConstBlockItems::No,
+            )
             .unwrap()
         {
             krate.items.push(item);
@@ -90,7 +94,7 @@ fn thrust_macros_path() -> Option<std::path::PathBuf> {
     None
 }
 
-pub fn main() {
+pub fn main() -> std::process::ExitCode {
     let mut args = std::env::args().collect::<Vec<_>>();
 
     use tracing_subscriber::{filter::EnvFilter, prelude::*};
@@ -112,8 +116,5 @@ pub fn main() {
         tracing::warn!("could not locate thrust_macros library");
     }
 
-    let code = rustc_driver::catch_with_exit_code(|| {
-        rustc_driver::run_compiler(&args, &mut CompilerCalls {})
-    });
-    std::process::exit(code);
+    rustc_driver::catch_with_exit_code(|| rustc_driver::run_compiler(&args, &mut CompilerCalls {}))
 }
diff --git a/src/refine/env.rs b/src/refine/env.rs
index 536e8383..4081c6d8 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -1013,10 +1013,7 @@ where
         let mut var = place.local.into();
 
         let mut it = place.projection.into_iter();
-        loop {
-            let Some(elem) = it.next() else {
-                break;
-            };
+        while let Some(elem) = it.next() {
             var = match (elem, self.flow_binding(var).expect("deref unbound var")) {
                 (PlaceElem::Deref, &FlowBinding::Box(x)) => x.into(),
                 (PlaceElem::Deref, &FlowBinding::Mut(x, _)) => x.into(),
diff --git a/src/rty.rs b/src/rty.rs
index c9a3249a..af0a7008 100644
--- a/src/rty.rs
+++ b/src/rty.rs
@@ -228,7 +228,7 @@ impl FunctionType {
             &mut self.ret,
             Box::new(RefinedType::unrefined(Type::unit())),
         );
-        self.ret = Box::new(old_ret.map_var(shift));
+        *self.ret = old_ret.map_var(shift);
         removed
     }
 }
diff --git a/tests/ui/fail/adt_discr.rs b/tests/ui/fail/adt_discr.rs
index cd9d8ac3..077959a6 100644
--- a/tests/ui/fail/adt_discr.rs
+++ b/tests/ui/fail/adt_discr.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -C debug-assertions=off
 
 pub enum X {
diff --git a/tests/ui/fail/annot_formula_fn.rs b/tests/ui/fail/annot_formula_fn.rs
index e2ae600b..1e9d778c 100644
--- a/tests/ui/fail/annot_formula_fn.rs
+++ b/tests/ui/fail/annot_formula_fn.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 
 #[thrust::formula_fn]
 fn _thrust_requires_rand_except(x: i64) -> bool {
diff --git a/tests/ui/fail/annot_preds.rs b/tests/ui/fail/annot_preds.rs
index 725e23ba..3d011da4 100644
--- a/tests/ui/fail/annot_preds.rs
+++ b/tests/ui/fail/annot_preds.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -Adead_code -C debug-assertions=off
 
 #[thrust::predicate]
diff --git a/tests/ui/fail/annot_preds_trait.rs b/tests/ui/fail/annot_preds_trait.rs
index d6e9a28f..eb857990 100644
--- a/tests/ui/fail/annot_preds_trait.rs
+++ b/tests/ui/fail/annot_preds_trait.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -Adead_code -C debug-assertions=off
 
 // A is represented as Tuple<Int> in SMT-LIB2 format.
diff --git a/tests/ui/fail/annot_preds_trait_multi.rs b/tests/ui/fail/annot_preds_trait_multi.rs
index b1156e50..a1b46161 100644
--- a/tests/ui/fail/annot_preds_trait_multi.rs
+++ b/tests/ui/fail/annot_preds_trait_multi.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -Adead_code -C debug-assertions=off
 
 #[thrust_macros::context]
diff --git a/tests/ui/fail/extern_spec_take.rs b/tests/ui/fail/extern_spec_take.rs
index 8dc17fff..22c9bacc 100644
--- a/tests/ui/fail/extern_spec_take.rs
+++ b/tests/ui/fail/extern_spec_take.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
diff --git a/tests/ui/fail/fn_poly_param_order.rs b/tests/ui/fail/fn_poly_param_order.rs
index 93af596d..5a8a2da2 100644
--- a/tests/ui/fail/fn_poly_param_order.rs
+++ b/tests/ui/fail/fn_poly_param_order.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 
 fn select<T, U, V>(a: T, b: U, c: V, which: i32) -> T {
     if which == 0 {
diff --git a/tests/ui/fail/iterators/range.rs b/tests/ui/fail/iterators/range.rs
index 1af93a70..f7de3553 100644
--- a/tests/ui/fail/iterators/range.rs
+++ b/tests/ui/fail/iterators/range.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER_ARGS=
 
diff --git a/tests/ui/fail/just_rec.rs b/tests/ui/fail/just_rec.rs
index df795468..426c74af 100644
--- a/tests/ui/fail/just_rec.rs
+++ b/tests/ui/fail/just_rec.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -C debug-assertions=off
 
 #[thrust::trusted]
diff --git a/tests/ui/fail/split.rs b/tests/ui/fail/split.rs
index c45751af..148edbe6 100644
--- a/tests/ui/fail/split.rs
+++ b/tests/ui/fail/split.rs
@@ -1,4 +1,5 @@
 //@error-in-other-file: Unsat
+//@no-rustfix
 //@compile-flags: -C debug-assertions=off
 
 #[thrust::trusted]
diff --git a/tests/ui/pass/iterators/fixed_filter_loop_none.rs b/tests/ui/pass/iterators/fixed_filter_loop_none.rs
index 393a1a30..d806f978 100644
--- a/tests/ui/pass/iterators/fixed_filter_loop_none.rs
+++ b/tests/ui/pass/iterators/fixed_filter_loop_none.rs
@@ -1,5 +1,6 @@
 //@check-pass
 //@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER_ARGS=
 
 struct Range {
     start: i64,