diff --git a/mir-state-analysis/src/free_pcs/check/checker.rs b/mir-state-analysis/src/free_pcs/check/checker.rs
index d19cd9b8b43..e3299398fb7 100644
--- a/mir-state-analysis/src/free_pcs/check/checker.rs
+++ b/mir-state-analysis/src/free_pcs/check/checker.rs
@@ -137,7 +137,7 @@ impl<'tcx> RepackOp<'tcx> {
                 assert!(place.is_prefix_exact(guide), "{self:?}");
                 let curr_state = state[place.local].get_allocated_mut();
                 let mut removed = curr_state
-                    .drain_filter(|p, _| place.related_to(*p))
+                    .extract_if(|p, _| place.related_to(*p))
                     .collect::<FxHashMap<_, _>>();
 
                 let (p, mut others, _) = place.expand_one_level(guide, rp);
diff --git a/mir-state-analysis/src/free_pcs/impl/engine.rs b/mir-state-analysis/src/free_pcs/impl/engine.rs
index 8d15e967ae7..05d3a1040fd 100644
--- a/mir-state-analysis/src/free_pcs/impl/engine.rs
+++ b/mir-state-analysis/src/free_pcs/impl/engine.rs
@@ -6,7 +6,7 @@
 
 use prusti_rustc_interface::{
     dataflow::{Analysis, AnalysisDomain, CallReturnPlaces},
-    index::vec::Idx,
+    index::Idx,
     middle::{
         mir::{
             visit::Visitor, BasicBlock, Body, Local, Location, Statement, Terminator, RETURN_PLACE,
@@ -65,7 +65,7 @@ impl<'a, 'tcx> AnalysisDomain<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> {
 
 impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> {
     fn apply_statement_effect(
-        &self,
+        &mut self,
         state: &mut Self::Domain,
         statement: &Statement<'tcx>,
         location: Location,
@@ -75,7 +75,7 @@ impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> {
     }
 
     fn apply_terminator_effect(
-        &self,
+        &mut self,
         state: &mut Self::Domain,
         terminator: &Terminator<'tcx>,
         location: Location,
@@ -85,7 +85,7 @@ impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> {
     }
 
     fn apply_call_return_effect(
-        &self,
+        &mut self,
         _state: &mut Self::Domain,
         _block: BasicBlock,
         _return_places: CallReturnPlaces<'_, 'tcx>,
diff --git a/mir-state-analysis/src/free_pcs/impl/fpcs.rs b/mir-state-analysis/src/free_pcs/impl/fpcs.rs
index 54a405e64a0..b5bc981b678 100644
--- a/mir-state-analysis/src/free_pcs/impl/fpcs.rs
+++ b/mir-state-analysis/src/free_pcs/impl/fpcs.rs
@@ -8,7 +8,7 @@ use std::fmt::{Debug, Formatter, Result};
 
 use derive_more::{Deref, DerefMut};
 use prusti_rustc_interface::{
-    dataflow::fmt::DebugWithContext, index::vec::IndexVec, middle::mir::Local,
+    dataflow::fmt::DebugWithContext, index::IndexVec, middle::mir::Local,
 };
 
 use crate::{
diff --git a/mir-state-analysis/src/free_pcs/impl/local.rs b/mir-state-analysis/src/free_pcs/impl/local.rs
index f7b3b069754..313d82fb228 100644
--- a/mir-state-analysis/src/free_pcs/impl/local.rs
+++ b/mir-state-analysis/src/free_pcs/impl/local.rs
@@ -143,7 +143,7 @@ impl<'tcx> CapabilityProjections<'tcx> {
         others.push(to);
         let mut ops = Vec::new();
         for (from, to, kind) in expanded {
-            let others = others.drain_filter(|other| !to.is_prefix(*other));
+            let others = others.extract_if(|other| !to.is_prefix(*other));
             self.extend(others.map(|p| (p, perm)));
             if kind.is_box() && perm.is_shallow_exclusive() {
                 ops.push(RepackOp::DerefShallowInit(from, to));
@@ -183,13 +183,13 @@ impl<'tcx> CapabilityProjections<'tcx> {
             for (to, _, kind) in &collapsed {
                 if kind.is_shared_ref() {
                     let mut is_prefixed = false;
-                    exclusive_at.drain_filter(|old| {
+                    exclusive_at.extract_if(|old| {
                         let cmp = to.either_prefix(*old);
                         if matches!(cmp, Some(false)) {
                             is_prefixed = true;
                         }
                         cmp.unwrap_or_default()
-                    });
+                    }).for_each(drop);
                     if !is_prefixed {
                         exclusive_at.push(*to);
                     }
@@ -199,7 +199,7 @@ impl<'tcx> CapabilityProjections<'tcx> {
         let mut ops = Vec::new();
         for (to, from, _) in collapsed {
             let removed_perms: Vec<_> =
-                old_caps.drain_filter(|old, _| to.is_prefix(*old)).collect();
+                old_caps.extract_if(|old, _| to.is_prefix(*old)).collect();
             let perm = removed_perms
                 .iter()
                 .fold(CapabilityKind::Exclusive, |acc, (_, p)| {
diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs
index 973271987cd..c12e425e5fd 100644
--- a/mir-state-analysis/src/free_pcs/impl/triple.rs
+++ b/mir-state-analysis/src/free_pcs/impl/triple.rs
@@ -58,6 +58,7 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
                 self.ensures_unalloc(local);
             }
             &Retag(_, box place) => self.requires_exclusive(place),
+            &PlaceMention(box place) => self.requires_write(place),
             AscribeUserType(..) | Coverage(..) | Intrinsic(..) | ConstEvalCounter | Nop => (),
         };
     }
@@ -69,7 +70,7 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
             Goto { .. }
             | SwitchInt { .. }
             | Resume
-            | Abort
+            | Terminate
             | Unreachable
             | Assert { .. }
             | GeneratorDrop
@@ -91,10 +92,6 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
                 self.requires_write(place);
                 self.ensures_write(place);
             }
-            &DropAndReplace { place, .. } => {
-                self.requires_write(place);
-                self.ensures_exclusive(place);
-            }
             &Call { destination, .. } => {
                 self.requires_write(destination);
                 self.ensures_exclusive(destination);
@@ -132,10 +129,6 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
                     self.requires_read(place);
                     // self.ensures_blocked_read(place);
                 }
-                BorrowKind::Unique => {
-                    self.requires_exclusive(place);
-                    // self.ensures_blocked_exclusive(place);
-                }
                 BorrowKind::Mut { .. } => {
                     self.requires_exclusive(place);
                     // self.ensures_blocked_exclusive(place);
diff --git a/mir-state-analysis/src/free_pcs/results/cursor.rs b/mir-state-analysis/src/free_pcs/results/cursor.rs
index 928341cb6f3..06f93fae2a8 100644
--- a/mir-state-analysis/src/free_pcs/results/cursor.rs
+++ b/mir-state-analysis/src/free_pcs/results/cursor.rs
@@ -53,7 +53,7 @@ impl<'mir, 'tcx> FreePcsAnalysis<'mir, 'tcx> {
     fn body(&self) -> &'mir Body<'tcx> {
         self.cursor.analysis().0.body()
     }
-    pub(crate) fn repacker(&self) -> PlaceRepacker<'mir, 'tcx> {
+    pub(crate) fn repacker(&mut self) -> PlaceRepacker<'mir, 'tcx> {
         self.cursor.results().analysis.0
     }
 
@@ -81,8 +81,8 @@ impl<'mir, 'tcx> FreePcsAnalysis<'mir, 'tcx> {
         self.end_stmt = None;
 
         // TODO: cleanup
-        let state = self.cursor.get();
         let rp: PlaceRepacker = self.repacker();
+        let state = self.cursor.get().clone();
         let block = &self.body()[location.block];
         let succs = block
             .terminator()
diff --git a/mir-state-analysis/src/lib.rs b/mir-state-analysis/src/lib.rs
index 217b198fc77..84c6fb4dcb2 100644
--- a/mir-state-analysis/src/lib.rs
+++ b/mir-state-analysis/src/lib.rs
@@ -5,7 +5,7 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 #![feature(rustc_private)]
-#![feature(box_patterns, hash_drain_filter, drain_filter)]
+#![feature(box_patterns, hash_extract_if, extract_if)]
 
 pub mod free_pcs;
 pub mod utils;
diff --git a/mir-state-analysis/src/utils/mutable.rs b/mir-state-analysis/src/utils/mutable.rs
index 118c80244f5..a733acdc139 100644
--- a/mir-state-analysis/src/utils/mutable.rs
+++ b/mir-state-analysis/src/utils/mutable.rs
@@ -7,9 +7,10 @@
 use prusti_rustc_interface::{
     hir,
     middle::{
-        mir::{Field, Mutability, ProjectionElem},
+        mir::{Mutability, ProjectionElem},
         ty::{CapturedPlace, TyKind, UpvarCapture},
     },
+    target::abi::FieldIdx,
 };
 
 use super::{root_place::RootPlace, Place, PlaceRepacker};
@@ -213,7 +214,7 @@ impl<'tcx> Place<'tcx> {
         self,
         upvars: &[Upvar<'tcx>],
         repacker: PlaceRepacker<'_, 'tcx>,
-    ) -> Option<Field> {
+    ) -> Option<FieldIdx> {
         let mut place_ref = *self;
         let mut by_ref = false;
 
diff --git a/mir-state-analysis/src/utils/repacker.rs b/mir-state-analysis/src/utils/repacker.rs
index b8b59e312c1..182fb09a46e 100644
--- a/mir-state-analysis/src/utils/repacker.rs
+++ b/mir-state-analysis/src/utils/repacker.rs
@@ -10,11 +10,12 @@ use prusti_rustc_interface::{
     index::bit_set::BitSet,
     middle::{
         mir::{
-            tcx::PlaceTy, Body, Field, HasLocalDecls, Local, Mutability, Place as MirPlace,
+            tcx::PlaceTy, Body, HasLocalDecls, Local, Mutability, Place as MirPlace,
             ProjectionElem,
         },
         ty::{TyCtxt, TyKind},
     },
+    target::abi::FieldIdx,
 };
 
 use super::Place;
@@ -237,7 +238,7 @@ impl<'tcx> Place<'tcx> {
                     .unwrap_or_else(|| def.non_enum_variant());
                 for (index, field_def) in variant.fields.iter().enumerate() {
                     if Some(index) != without_field {
-                        let field = Field::from_usize(index);
+                        let field = FieldIdx::from_usize(index);
                         let field_place = repacker.tcx.mk_place_field(
                             self.to_rust_place(repacker),
                             field,
@@ -250,7 +251,7 @@ impl<'tcx> Place<'tcx> {
             TyKind::Tuple(slice) => {
                 for (index, arg) in slice.iter().enumerate() {
                     if Some(index) != without_field {
-                        let field = Field::from_usize(index);
+                        let field = FieldIdx::from_usize(index);
                         let field_place =
                             repacker
                                 .tcx
@@ -260,9 +261,9 @@ impl<'tcx> Place<'tcx> {
                 }
             }
             TyKind::Closure(_, substs) => {
-                for (index, subst_ty) in substs.as_closure().upvar_tys().enumerate() {
+                for (index, subst_ty) in substs.as_closure().upvar_tys().iter().enumerate() {
                     if Some(index) != without_field {
-                        let field = Field::from_usize(index);
+                        let field = FieldIdx::from_usize(index);
                         let field_place = repacker.tcx.mk_place_field(
                             self.to_rust_place(repacker),
                             field,
@@ -273,9 +274,9 @@ impl<'tcx> Place<'tcx> {
                 }
             }
             TyKind::Generator(_, substs, _) => {
-                for (index, subst_ty) in substs.as_generator().upvar_tys().enumerate() {
+                for (index, subst_ty) in substs.as_generator().upvar_tys().iter().enumerate() {
                     if Some(index) != without_field {
-                        let field = Field::from_usize(index);
+                        let field = FieldIdx::from_usize(index);
                         let field_place = repacker.tcx.mk_place_field(
                             self.to_rust_place(repacker),
                             field,