diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index ae6ecb9b425..3a45032ffc8 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -4,85 +4,84 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use crate::encoder::mir::spans::interface::SpanInterface;
-use crate::encoder::builtin_encoder::{BuiltinMethodKind};
-use crate::encoder::errors::{
-    SpannedEncodingError, ErrorCtxt, EncodingError, WithSpan,
-    EncodingResult, SpannedEncodingResult
+use super::{
+    counterexamples::DiscriminantsStateInterface, high::generics::HighGenericsEncoderInterface,
 };
-use crate::encoder::errors::error_manager::PanicCause;
-use crate::encoder::foldunfold;
-use crate::encoder::high::types::HighTypeEncoderInterface;
-use crate::encoder::initialisation::InitInfo;
-use crate::encoder::loop_encoder::{LoopEncoder, LoopEncoderError};
-use crate::encoder::mir_encoder::{MirEncoder, FakeMirEncoder, PlaceEncoder, PlaceEncoding, ExprOrArrayBase};
-use crate::encoder::mir_encoder::PRECONDITION_LABEL;
-use crate::encoder::mir_successor::MirSuccessor;
-use crate::encoder::places::{Local, LocalVariableManager, Place};
-use crate::encoder::Encoder;
-use crate::encoder::resources::interface::ResourcesEncoderInterface;
-use crate::encoder::snapshot::interface::SnapshotEncoderInterface;
-use crate::encoder::mir::procedures::encoder::specification_blocks::SpecificationBlocks;
-use crate::error_unsupported;
+use crate::{
+    encoder::{
+        builtin_encoder::BuiltinMethodKind,
+        errors::{
+            error_manager::PanicCause, EncodingError, EncodingErrorKind, EncodingResult, ErrorCtxt,
+            SpannedEncodingError, SpannedEncodingResult, WithSpan,
+        },
+        foldunfold,
+        high::types::HighTypeEncoderInterface,
+        initialisation::InitInfo,
+        loop_encoder::{LoopEncoder, LoopEncoderError},
+        mir::{
+            contracts::{ContractsEncoderInterface, ProcedureContract},
+            procedures::encoder::specification_blocks::SpecificationBlocks,
+            pure::{PureFunctionEncoderInterface, SpecificationEncoderInterface},
+            sequences::MirSequencesEncoderInterface,
+            spans::interface::SpanInterface,
+            specifications::SpecificationsInterface,
+            type_invariants::TypeInvariantEncoderInterface,
+            types::MirTypeEncoderInterface,
+        },
+        mir_encoder::{
+            ExprOrArrayBase, FakeMirEncoder, MirEncoder, PlaceEncoder, PlaceEncoding,
+            PRECONDITION_LABEL,
+        },
+        mir_successor::MirSuccessor,
+        places::{Local, LocalVariableManager, Place},
+        resources,
+        resources::interface::ResourcesEncoderInterface,
+        snapshot::interface::SnapshotEncoderInterface,
+        Encoder,
+    },
+    error_unsupported,
+    utils::is_reference,
+};
+use ::log::{debug, trace};
 use prusti_common::{
     config,
     utils::to_string::ToString,
-    vir::{ToGraphViz, fixes::fix_ghost_vars},
-    vir_local, vir_expr, vir_stmt
-};
-use vir_crate::{
-    polymorphic::{
-        self as vir,
-        compute_identifier,
-        borrows::Borrow,
-        collect_assigned_vars,
-        CfgBlockIndex, ExprIterator, Successor, Type},
+    vir::{fixes::fix_ghost_vars, ToGraphViz},
+    vir_expr, vir_local, vir_stmt,
 };
 use prusti_interface::{
     data::ProcedureDefId,
     environment::{
-        borrowck::facts,
+        borrowck::{facts, regions::PlaceRegionsError},
+        mir_utils::SliceOrArrayRef,
         polonius_info::{
             LoanPlaces, PoloniusInfo, PoloniusInfoError, ReborrowingDAG, ReborrowingDAGNode,
             ReborrowingKind, ReborrowingZombity,
         },
         BasicBlockIndex, LoopAnalysisError, PermissionKind, Procedure,
     },
-    PrustiError,
+    specs::{
+        typed,
+        typed::{Pledge, SpecificationItem},
+    },
+    utils, PrustiError,
 };
-use std::collections::{BTreeMap};
-use prusti_interface::utils;
-use prusti_rustc_interface::middle::mir::Mutability;
-use prusti_rustc_interface::middle::mir;
-use prusti_rustc_interface::middle::mir::{TerminatorKind};
-use prusti_rustc_interface::middle::ty::{self, subst::SubstsRef};
-use prusti_rustc_interface::target::abi::Integer;
-use rustc_hash::{FxHashMap, FxHashSet};
-use prusti_rustc_interface::span::Span;
-use prusti_rustc_interface::errors::MultiSpan;
-use prusti_interface::specs::typed;
-use ::log::{trace, debug};
-use prusti_interface::environment::borrowck::regions::PlaceRegionsError;
-use crate::encoder::errors::EncodingErrorKind;
-use std::convert::TryInto;
-use prusti_interface::specs::typed::{Pledge, SpecificationItem};
-use vir_crate::polymorphic::Float;
-use crate::utils::is_reference;
-use crate::encoder::mir::{
-    sequences::MirSequencesEncoderInterface,
-    contracts::{
-        ContractsEncoderInterface,
-        ProcedureContract,
+use prusti_rustc_interface::{
+    errors::MultiSpan,
+    middle::{
+        mir,
+        mir::{Mutability, TerminatorKind},
+        ty::{self, subst::SubstsRef},
     },
-    pure::PureFunctionEncoderInterface,
-    types::MirTypeEncoderInterface,
-    pure::SpecificationEncoderInterface,
-    specifications::SpecificationsInterface,
-    type_invariants::TypeInvariantEncoderInterface,
+    span::Span,
+    target::abi::Integer,
+};
+use rustc_hash::{FxHashMap, FxHashSet};
+use std::{collections::BTreeMap, convert::TryInto, iter::once};
+use vir_crate::polymorphic::{
+    self as vir, borrows::Borrow, collect_assigned_vars, compute_identifier, CfgBlockIndex,
+    ExprIterator, Float, Successor, Type,
 };
-use super::high::generics::HighGenericsEncoderInterface;
-use super::counterexamples::DiscriminantsStateInterface;
-use prusti_interface::environment::mir_utils::SliceOrArrayRef;
 
 pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> {
     encoder: &'p Encoder<'v, 'tcx>,
@@ -121,7 +120,8 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> {
         FxHashMap<mir::Location, (ProcedureContract<'tcx>, FxHashMap<vir::Expr, vir::Expr>)>,
     /// A map that stores local variables used to preserve the value of a place accross the loop
     /// when we cannot do that by using permissions.
-    pure_var_for_preserving_value_map: FxHashMap<BasicBlockIndex, FxHashMap<vir::Expr, vir::LocalVar>>,
+    pure_var_for_preserving_value_map:
+        FxHashMap<BasicBlockIndex, FxHashMap<vir::Expr, vir::LocalVar>>,
     /// Information about which places are definitely initialised.
     init_info: InitInfo,
     /// Mapping from old expressions to ghost variables with which they were replaced.
@@ -138,7 +138,7 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> {
 impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     pub fn new(
         encoder: &'p Encoder<'v, 'tcx>,
-        procedure: &'p Procedure<'tcx>
+        procedure: &'p Procedure<'tcx>,
     ) -> SpannedEncodingResult<Self> {
         debug!("ProcedureEncoder constructor");
 
@@ -150,7 +150,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let init_info = InitInfo::new(mir, tcx, proc_def_id, &mir_encoder)
             .with_default_span(procedure.get_span())?;
 
-        let specification_blocks = SpecificationBlocks::build(encoder.env().query, mir, procedure, false);
+        let specification_blocks =
+            SpecificationBlocks::build(encoder.env().query, mir, procedure, false);
 
         let cfg_method = vir::CfgMethod::new(
             // method name
@@ -222,7 +223,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<()> {
         let block = &self.mir[bb];
         let _ = self.try_encode_assert(bb, block, encoded_statements)?
-        || self.try_encode_assume(bb, block, encoded_statements)?;
+            || self.try_encode_assume(bb, block, encoded_statements)?;
         Ok(())
     }
 
@@ -238,16 +239,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
             )) = stmt.kind
             {
-                if self.encoder.get_prusti_assumption(cl_def_id.to_def_id()).is_none() {
+                if self
+                    .encoder
+                    .get_prusti_assumption(cl_def_id.to_def_id())
+                    .is_none()
+                {
                     return Ok(false);
                 }
-                let assume_expr = self.encoder.encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?;
+                let assume_expr =
+                    self.encoder
+                        .encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?;
 
-                let assume_stmt = vir::Stmt::Inhale(
-                    vir::Inhale {
-                        expr: assume_expr
-                    }
-                );
+                let assume_stmt = vir::Stmt::Inhale(vir::Inhale { expr: assume_expr });
 
                 encoded_statements.push(assume_stmt);
 
@@ -278,14 +281,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     .encoder
                     .get_definition_span(assertion.assertion.to_def_id());
 
-                let assert_expr = self.encoder.encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?;
+                let assert_expr =
+                    self.encoder
+                        .encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?;
 
-                let assert_stmt = vir::Stmt::Assert(
-                    vir::Assert {
-                        expr: assert_expr,
-                        position: self.register_error(span, ErrorCtxt::Panic(PanicCause::Assert))
-                    }
-                );
+                let assert_stmt = vir::Stmt::Assert(vir::Assert {
+                    expr: assert_expr,
+                    position: self.register_error(span, ErrorCtxt::Panic(PanicCause::Assert)),
+                });
 
                 encoded_statements.push(assert_stmt);
 
@@ -302,11 +305,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 variable,
             } => {
                 let msg = if self.mir.local_decls[variable].is_user_variable() {
-                    "creation of loan 'FIXME: extract variable name' in loop is unsupported".to_string()
+                    "creation of loan 'FIXME: extract variable name' in loop is unsupported"
+                        .to_string()
                 } else {
                     "creation of temporary loan in loop is unsupported".to_string()
                 };
-                SpannedEncodingError::unsupported(msg, self.mir_encoder.get_span_of_basic_block(loop_head))
+                SpannedEncodingError::unsupported(
+                    msg,
+                    self.mir_encoder.get_span_of_basic_block(loop_head),
+                )
             }
 
             PoloniusInfoError::LoansInNestedLoops(location1, _loop1, _location2, _loop2) => {
@@ -324,11 +331,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 )
             }
 
-            PoloniusInfoError::MultipleMagicWandsPerLoop(location) => SpannedEncodingError::unsupported(
-                "the creation of loans in this loop is not supported \
+            PoloniusInfoError::MultipleMagicWandsPerLoop(location) => {
+                SpannedEncodingError::unsupported(
+                    "the creation of loans in this loop is not supported \
                     (MultipleMagicWandsPerLoop)",
-                self.mir.source_info(location).span,
-            ),
+                    self.mir.source_info(location).span,
+                )
+            }
 
             PoloniusInfoError::MagicWandHasNoRepresentativeLoan(location) => {
                 SpannedEncodingError::unsupported(
@@ -338,10 +347,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 )
             }
 
-            PoloniusInfoError::PlaceRegionsError(
-                PlaceRegionsError::Unsupported(msg),
-                span,
-            ) => {
+            PoloniusInfoError::PlaceRegionsError(PlaceRegionsError::Unsupported(msg), span) => {
                 SpannedEncodingError::unsupported(msg, span)
             }
 
@@ -364,7 +370,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let mir_span = self.mir.span;
 
         // Retrieve the contract
-        let procedure_contract = self.encoder
+        let procedure_contract = self
+            .encoder
             .get_procedure_contract_for_def(self.proc_def_id, self.substs)
             .with_span(mir_span)?;
         assert_one_magic_wand(procedure_contract.borrow_infos.len()).with_span(mir_span)?;
@@ -375,9 +382,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let name = self.mir_encoder.encode_local_var_name(local);
             let typ = self
                 .encoder
-                .encode_type(self.mir_encoder.get_local_ty(local)).unwrap(); // will panic if attempting to encode unsupported type
-            self.cfg_method
-                .add_formal_return(&name, typ)
+                .encode_type(self.mir_encoder.get_local_ty(local))
+                .unwrap(); // will panic if attempting to encode unsupported type
+            self.cfg_method.add_formal_return(&name, typ)
         }
 
         // Preprocess loops
@@ -399,8 +406,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         // Load Polonius info
         self.polonius_info = Some(
-            PoloniusInfo::new(self.encoder.env(), self.procedure, &self.cached_loop_invariant_block)
-                .map_err(|err| self.translate_polonius_error(err))?,
+            PoloniusInfo::new(
+                self.encoder.env(),
+                self.procedure,
+                &self.cached_loop_invariant_block,
+            )
+            .map_err(|err| self.translate_polonius_error(err))?,
         );
 
         // Initialize CFG blocks
@@ -432,7 +443,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 .register_span(self.mir_encoder.get_span_of_basic_block(bbi));
             self.cfg_method.add_stmt(
                 start_cfg_block,
-                vir::Stmt::Assign( vir::Assign {
+                vir::Stmt::Assign(vir::Assign {
                     target: vir::Expr::local(executed_flag_var.clone()).set_pos(bb_pos),
                     source: false.into(),
                     kind: vir::AssignKind::Copy,
@@ -450,12 +461,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             &self.procedure.get_reachable_nonspec_cfg_blocks(),
             0,
             return_cfg_block,
+            &[-1],
         )?;
         if !unresolved_edges.is_empty() {
             return Err(SpannedEncodingError::internal(
-                format!(
-                    "there are unresolved CFG edges in the encoding: {unresolved_edges:?}"
-                ),
+                format!("there are unresolved CFG edges in the encoding: {unresolved_edges:?}"),
                 mir_span,
             ));
         }
@@ -467,15 +477,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         );
 
         // Prepare assertions to check specification refinement
-        let (precondition_weakening, postcondition_strengthening)
-            = self.encode_spec_refinement(PRECONDITION_LABEL)?;
+        let (precondition_weakening, postcondition_strengthening) =
+            self.encode_spec_refinement(PRECONDITION_LABEL)?;
 
         // Encode preconditions
         self.encode_preconditions(start_cfg_block, precondition_weakening)?;
 
         if config::time_reasoning() {
             // consume a time credits and produce a time receipt in the body of the function
-            self.cfg_method.add_stmts(start_cfg_block, self.get_tick_call(self.mir.span, 1));
+            self.cfg_method
+                .add_stmts(start_cfg_block, self.get_tick_call(self.mir.span, 1, &[-1]));
         }
 
         // Encode postcondition
@@ -490,8 +501,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let local_ty = self.locals.get_type(*local);
             let typ = self.encoder.encode_type(local_ty).unwrap(); // will panic if attempting to encode unsupported type
             let var_name = self.locals.get_name(*local);
-            self.cfg_method
-                .add_local_var(&var_name, typ);
+            self.cfg_method.add_local_var(&var_name, typ);
         }
 
         self.check_vir()?;
@@ -511,7 +521,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         }
 
         // Patch snapshots
-        self.cfg_method = self.encoder.patch_snapshots_method(self.cfg_method)
+        self.cfg_method = self
+            .encoder
+            .patch_snapshots_method(self.cfg_method)
             .with_span(mir_span)?;
 
         // Add fold/unfold
@@ -521,10 +533,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .iter()
             .map(|(loan, location)| (loan.index().into(), *location))
             .collect();
-        let method_pos = self.register_error(
-                self.mir.span,
-                ErrorCtxt::Unexpected
-            );
+        let method_pos = self.register_error(self.mir.span, ErrorCtxt::Unexpected);
         let method_with_fold_unfold = foldunfold::add_fold_unfold(
             self.encoder,
             self.cfg_method,
@@ -532,19 +541,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             &self.cfg_blocks_map,
             method_pos,
         )
-        .map_err(|foldunfold_error| {
-            match foldunfold_error {
-                foldunfold::FoldUnfoldError::Unsupported(msg) => {
-                    SpannedEncodingError::unsupported(msg, mir_span)
-                }
-
-                _ => SpannedEncodingError::internal(
-                    format!(
-                        "cannot generate fold-unfold Viper statements. {foldunfold_error}",
-                    ),
-                    mir_span,
-                ),
+        .map_err(|foldunfold_error| match foldunfold_error {
+            foldunfold::FoldUnfoldError::Unsupported(msg) => {
+                SpannedEncodingError::unsupported(msg, mir_span)
             }
+            _ => SpannedEncodingError::internal(
+                format!("cannot generate fold-unfold Viper statements. {foldunfold_error}",),
+                mir_span,
+            ),
         })?;
 
         // Fix variable declarations.
@@ -574,6 +578,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         ordered_group_blocks: &[BasicBlockIndex],
         group_loop_depth: usize,
         return_block: CfgBlockIndex,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(Option<CfgBlockIndex>, Vec<(CfgBlockIndex, BasicBlockIndex)>)> {
         // Encode the CFG blocks
         let mut bb_map: FxHashMap<_, _> = FxHashMap::default();
@@ -583,13 +588,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let curr_loop_depth = loop_info.get_loop_depth(curr_bb);
             let (curr_block, curr_edges) = if curr_loop_depth == group_loop_depth {
                 // This block is not in a nested loop
-                self.encode_block(label_prefix, curr_bb, return_block)?
+                self.encode_block(label_prefix, curr_bb, return_block, scope_ids)?
             } else {
                 debug_assert!(curr_loop_depth > group_loop_depth);
                 let is_loop_head = loop_info.is_loop_head(curr_bb);
                 if curr_loop_depth == group_loop_depth + 1 && is_loop_head {
                     // Encode a nested loop
-                    self.encode_loop(label_prefix, curr_bb, return_block)?
+                    self.encode_loop(label_prefix, curr_bb, return_block, scope_ids)?
                 } else {
                     debug_assert!(curr_loop_depth > group_loop_depth + 1 || !is_loop_head);
                     // Skip the inner block of a nested loop
@@ -647,7 +652,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             matches!(
                 expr,
                 vir::Expr::Const(vir::ConstExpr {
-                    value: vir::Const::Bool(true), ..
+                    value: vir::Const::Bool(true),
+                    ..
                 })
             )
         }
@@ -669,14 +675,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         }
         impl<'a, 'b, 'c> ExprFolder for FindFnApps<'a, 'b, 'c> {
             fn fold_func_app(&mut self, expr: vir::FuncApp) -> vir::Expr {
-                let vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. } = expr;
+                let vir::FuncApp {
+                    function_name,
+                    type_arguments,
+                    arguments,
+                    formal_arguments,
+                    return_type,
+                    ..
+                } = expr;
                 if self.recurse {
-                    let identifier: vir::FunctionIdentifier =
-                                compute_identifier(&function_name, &type_arguments, &formal_arguments, &return_type).into();
+                    let identifier: vir::FunctionIdentifier = compute_identifier(
+                        &function_name,
+                        &type_arguments,
+                        &formal_arguments,
+                        &return_type,
+                    )
+                    .into();
                     let pres = self.encoder.get_function(&identifier).unwrap().pres.clone();
                     // Avoid recursively collecting preconditions: they should be self-framing anyway
                     self.recurse = false;
-                    let pres: vir::Expr = pres.into_iter().fold(true.into(), |acc, expr| vir_expr! { [acc] && [expr] });
+                    let pres: vir::Expr = pres
+                        .into_iter()
+                        .fold(true.into(), |acc, expr| vir_expr! { [acc] && [expr] });
                     self.push_precond(pres, Some(function_name));
                     self.recurse = true;
 
@@ -690,16 +710,27 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 // We only care about the exhale part (e.g. for `walk_exhale`)
                 self.fold(*expr.exhale_expr)
             }
-            fn fold_predicate_access_predicate(&mut self, expr: vir::PredicateAccessPredicate) -> vir::Expr {
+            fn fold_predicate_access_predicate(
+                &mut self,
+                expr: vir::PredicateAccessPredicate,
+            ) -> vir::Expr {
                 self.fold(*expr.argument);
                 true.into()
             }
-            fn fold_field_access_predicate(&mut self, expr: vir::FieldAccessPredicate) -> vir::Expr {
+            fn fold_field_access_predicate(
+                &mut self,
+                expr: vir::FieldAccessPredicate,
+            ) -> vir::Expr {
                 self.fold(*expr.base);
                 true.into()
             }
             fn fold_bin_op(&mut self, expr: vir::BinOp) -> vir::Expr {
-                let vir::BinOp { op_kind, left, right, position } = expr;
+                let vir::BinOp {
+                    op_kind,
+                    left,
+                    right,
+                    position,
+                } = expr;
                 let left = self.fold_boxed(left);
                 let right = self.fold_boxed(right);
                 match op_kind {
@@ -708,27 +739,38 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     vir::BinaryOpKind::Or if is_const_true(&left) => *left,
                     vir::BinaryOpKind::Or if is_const_true(&right) => *right,
                     _ => vir::Expr::BinOp(vir::BinOp {
-                        op_kind, left, right, position,
+                        op_kind,
+                        left,
+                        right,
+                        position,
                     }),
                 }
             }
         }
         let mut walker = FindFnApps {
-            recurse: true, preconds: Vec::new(), encoder: self.encoder
+            recurse: true,
+            preconds: Vec::new(),
+            encoder: self.encoder,
         };
         walker.walk(stmt);
         walker.preconds
     }
     fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<(Option<String>, vir::Expr)> {
         let bb = &self.cfg_method.basic_blocks[block.block_index];
-        let mut preconds: Vec<_> = bb.stmts.iter().flat_map(|stmt| self.stmt_preconditions(stmt)).collect();
+        let mut preconds: Vec<_> = bb
+            .stmts
+            .iter()
+            .flat_map(|stmt| self.stmt_preconditions(stmt))
+            .collect();
         match &bb.successor {
             Successor::Undefined => (),
             Successor::Return => (),
             Successor::Goto(cbi) => preconds.extend(self.block_preconditions(cbi)),
             Successor::GotoSwitch(succs, def) => {
                 preconds.extend(
-                    succs.iter().flat_map(|cond_bb| self.block_preconditions(&cond_bb.1))
+                    succs
+                        .iter()
+                        .flat_map(|cond_bb| self.block_preconditions(&cond_bb.1)),
                 );
                 preconds.extend(self.block_preconditions(def));
             }
@@ -789,6 +831,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         label_prefix: &str,
         loop_head: BasicBlockIndex,
         return_block: CfgBlockIndex,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(CfgBlockIndex, Vec<(CfgBlockIndex, BasicBlockIndex)>)> {
         let loop_info = self.loop_encoder.loops();
         debug_assert!(loop_info.is_loop_head(loop_head));
@@ -801,9 +844,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .get_loop_body(loop_head)
             .iter()
             .copied()
-            .filter(
-                |&bb| self.procedure.is_reachable_block(bb) && !self.procedure.is_spec_block(bb)
-            )
+            .filter(|&bb| {
+                self.procedure.is_reachable_block(bb) && !self.procedure.is_spec_block(bb)
+            })
             .collect();
 
         // Identify important blocks
@@ -811,13 +854,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let loop_exit_blocks_set: FxHashSet<_> = loop_exit_blocks.iter().cloned().collect();
         let before_invariant_block: BasicBlockIndex = self.cached_loop_invariant_block[&loop_head];
         let before_inv_block_pos = loop_body
-            .iter().copied()
+            .iter()
+            .copied()
             .position(|bb| bb == before_invariant_block)
             .unwrap();
         let after_inv_block_pos = 1 + before_inv_block_pos;
         // Find boolean switch exit blocks before the invariant
         let boolean_exit_blocks_before_inv: Vec<_> = loop_body[0..after_inv_block_pos]
-            .iter().copied()
+            .iter()
+            .copied()
             .filter(|bb| loop_exit_blocks_set.contains(bb))
             .filter(|&bb| self.procedure.successors(bb).len() == 2)
             .collect();
@@ -886,6 +931,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             loop_guard_evaluation,
             loop_depth,
             return_block,
+            scope_ids,
         )?;
         heads.push(first_g_head);
 
@@ -895,12 +941,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             loop_body_before_inv,
             loop_depth,
             return_block,
+            scope_ids,
         )?;
         heads.push(first_b1_head);
 
         // Calculate if `G` and `B1` are safe to include as the first `body_invariant!(...)`
-        let mut preconds = first_g_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default();
-        preconds.extend(first_b1_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default());
+        let mut preconds = first_g_head
+            .map(|cbi| self.block_preconditions(&cbi))
+            .unwrap_or_default();
+        preconds.extend(
+            first_b1_head
+                .map(|cbi| self.block_preconditions(&cbi))
+                .unwrap_or_default(),
+        );
 
         // Build the "invariant" CFG block (start - G - B1 - *invariant* - B2 - G - B1 - end)
         // (1) checks the loop invariant on entry
@@ -925,25 +978,43 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         );
         heads.push(Some(inv_pre_block));
         self.cfg_method
-                .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block_perms));
+            .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block_perms));
         {
-            let stmts =
-                self.encode_loop_invariant_exhale_stmts(loop_head, before_invariant_block, false)?;
+            let stmts = self.encode_loop_invariant_exhale_stmts(
+                loop_head,
+                before_invariant_block,
+                false,
+                scope_ids,
+            )?;
             self.cfg_method.add_stmts(inv_pre_block, stmts);
         }
+        let scope_ids: Vec<isize> = scope_ids
+            .iter()
+            .copied()
+            .chain(once(loop_head.index() as isize))
+            .collect();
         // We'll add later more statements at the end of inv_pre_block, to havoc local variables
         let fnspec_span = {
-            let (mut stmts, fnspec_span) =
-                self.encode_loop_invariant_inhale_fnspec_stmts(loop_head, before_invariant_block, false)?;
+            let (mut stmts, fnspec_span) = self.encode_loop_invariant_inhale_fnspec_stmts(
+                loop_head,
+                before_invariant_block,
+                false,
+                &scope_ids,
+            )?;
             if config::time_reasoning() {
                 // consume a time credit and produce a time receipt at each iteration of the loop
-                stmts.extend(self.get_tick_call(fnspec_span.clone(), 1).into_iter());   
+                stmts.extend(
+                    self.get_tick_call(fnspec_span.clone(), 1, &scope_ids)
+                        .into_iter(),
+                );
             }
-            self.cfg_method.add_stmts(inv_post_block_fnspc, stmts); fnspec_span
+            self.cfg_method.add_stmts(inv_post_block_fnspc, stmts);
+            fnspec_span
         };
         {
-            let stmts =
-                self.encode_loop_invariant_inhale_perm_stmts(loop_head, before_invariant_block, false).with_span(fnspec_span)?;
+            let stmts = self
+                .encode_loop_invariant_inhale_perm_stmts(loop_head, before_invariant_block, false)
+                .with_span(fnspec_span)?;
             self.cfg_method.add_stmts(inv_post_block_perms, stmts);
         }
 
@@ -954,6 +1025,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 loop_guard_evaluation,
                 loop_depth,
                 return_block,
+                &scope_ids,
             )?;
             if let Some(mid_g_head) = &mid_g.0 {
                 self.block_assert_to_assume(mid_g_head);
@@ -965,6 +1037,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 loop_body_before_inv,
                 loop_depth,
                 return_block,
+                &scope_ids,
             )?;
             if let Some(mid_b1_head) = &mid_b1.0 {
                 self.block_assert_to_assume(mid_b1_head);
@@ -973,24 +1046,45 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             Some((mid_g, mid_b1))
         } else {
             // Cannot add loop guard to loop invariant
-            let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
-                name.strip_prefix("m_").unwrap_or(name)
-            }).collect();
+            let fn_names: Vec<_> = preconds
+                .iter()
+                .filter_map(|(name, _)| name.as_ref())
+                .map(|name| name.strip_prefix("m_").unwrap_or(name))
+                .collect();
             let warning_msg = if fn_names.is_empty() {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
             } else {
                 "the loop guard was not automatically added as a `body_invariant!(...)`, \
-                due to the following pure functions with preconditions: [".to_string() + &fn_names.join(", ") + "]"
+                due to the following pure functions with preconditions: ["
+                    .to_string()
+                    + &fn_names.join(", ")
+                    + "]"
             };
             // Span of loop guard
-            let span_lg = loop_guard_evaluation.last().map(|bb| self.mir_encoder.get_span_of_basic_block(*bb));
+            let span_lg = loop_guard_evaluation
+                .last()
+                .map(|bb| self.mir_encoder.get_span_of_basic_block(*bb));
             // Span of entire loop body before inv; the last elem (if any) will be the `body_invariant!(...)` bb
-            let span_lb = loop_body_before_inv.iter().rev().skip(1).map(|bb| self.mir_encoder.get_span_of_basic_block(*bb))
-                .fold(None, |acc: Option<Span>, span| Some(acc.map(|other|
-                    if span.ctxt() == other.ctxt() { span.to(other) } else { other }
-                ).unwrap_or(span)) );
+            let span_lb = loop_body_before_inv
+                .iter()
+                .rev()
+                .skip(1)
+                .map(|bb| self.mir_encoder.get_span_of_basic_block(*bb))
+                .fold(None, |acc: Option<Span>, span| {
+                    Some(
+                        acc.map(|other| {
+                            if span.ctxt() == other.ctxt() {
+                                span.to(other)
+                            } else {
+                                other
+                            }
+                        })
+                        .unwrap_or(span),
+                    )
+                });
             // Multispan to highlight both
-            let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().flatten().collect());
+            let span =
+                MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().flatten().collect());
             // It's only a warning so we might as well emit it straight away
             PrustiError::warning(warning_msg, span).emit(&self.encoder.env().diagnostic);
             None
@@ -1002,6 +1096,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             loop_body_after_inv,
             loop_depth,
             return_block,
+            &scope_ids,
         )?;
         heads.push(last_b2_head);
 
@@ -1011,6 +1106,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             loop_guard_evaluation,
             loop_depth,
             return_block,
+            &scope_ids,
         )?;
         heads.push(last_g_head);
 
@@ -1020,6 +1116,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             loop_body_before_inv,
             loop_depth,
             return_block,
+            &scope_ids,
         )?;
         heads.push(last_b1_head);
 
@@ -1036,13 +1133,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let stmts = self.encode_loop_invariant_exhale_stmts(
                 loop_head,
                 before_invariant_block,
-                true
+                true,
+                &scope_ids,
             )?;
             self.cfg_method.add_stmts(end_body_block, stmts);
         }
         self.cfg_method.add_stmt(
             end_body_block,
-            vir::Stmt::Inhale( vir::Inhale {expr: false.into()} ),
+            vir::Stmt::Inhale(vir::Inhale { expr: false.into() }),
         );
         heads.push(Some(end_body_block));
 
@@ -1077,20 +1175,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         if let Some(((mid_g_head, mid_g_edges), (mid_b1_head, mid_b1_edges))) = mid_groups {
             let mid_b1_block = mid_b1_head.unwrap_or(inv_post_block_fnspc);
             // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - G - B1 - invariant_fnspec - B2 - G - B1 - end)
-            self.cfg_method
-                .set_successor(inv_post_block_perms, vir::Successor::Goto(mid_g_head.unwrap_or(mid_b1_block)));
+            self.cfg_method.set_successor(
+                inv_post_block_perms,
+                vir::Successor::Goto(mid_g_head.unwrap_or(mid_b1_block)),
+            );
 
             // We know that there is at least one loop iteration of B2, thus it is safe to assume
             // that anything beforehand couldn't have exited the loop. Here we use
             // `self.cfg_method.set_successor(..., Successor::Return)` as the same as `assume false`
             for (curr_block, target) in &mid_g_edges {
                 if self.loop_encoder.get_loop_depth(*target) < loop_depth {
-                    self.cfg_method.set_successor(*curr_block, Successor::Return);
+                    self.cfg_method
+                        .set_successor(*curr_block, Successor::Return);
                 }
             }
-            let mid_g_edges = mid_g_edges.into_iter().filter(|(_, target)|
-                self.loop_encoder.get_loop_depth(*target) >= loop_depth
-            ).collect::<Vec<_>>();
+            let mid_g_edges = mid_g_edges
+                .into_iter()
+                .filter(|(_, target)| self.loop_encoder.get_loop_depth(*target) >= loop_depth)
+                .collect::<Vec<_>>();
             // Link edges from the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end)
             still_unresolved_edges.extend(self.encode_unresolved_edges(mid_g_edges, |bb| {
                 if bb == after_guard_block {
@@ -1104,12 +1206,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             // that anything beforehand couldn't have exited the loop.
             for (curr_block, target) in &mid_b1_edges {
                 if self.loop_encoder.get_loop_depth(*target) < loop_depth {
-                    self.cfg_method.set_successor(*curr_block, Successor::Return);
+                    self.cfg_method
+                        .set_successor(*curr_block, Successor::Return);
                 }
             }
-            let mid_b1_edges = mid_b1_edges.into_iter().filter(|(_, target)|
-                self.loop_encoder.get_loop_depth(*target) >= loop_depth
-            ).collect::<Vec<_>>();
+            let mid_b1_edges = mid_b1_edges
+                .into_iter()
+                .filter(|(_, target)| self.loop_encoder.get_loop_depth(*target) >= loop_depth)
+                .collect::<Vec<_>>();
             // Link edges from the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end)
             still_unresolved_edges.extend(self.encode_unresolved_edges(mid_b1_edges, |bb| {
                 if bb == after_inv_block {
@@ -1120,8 +1224,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             })?);
         } else {
             // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - invariant_fnspec - B2 - G - B1 - end)
-            self.cfg_method
-                .set_successor(inv_post_block_perms, vir::Successor::Goto(inv_post_block_fnspc));
+            self.cfg_method.set_successor(
+                inv_post_block_perms,
+                vir::Successor::Goto(inv_post_block_fnspc),
+            );
         }
 
         // Link edges of "invariant" (start - G - B1 - *invariant* - B2 - G - B1 - end)
@@ -1178,13 +1284,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 vir::Type::Snapshot(_) => BuiltinMethodKind::HavocRef,
                 vir::Type::Seq(_) => BuiltinMethodKind::HavocRef,
                 vir::Type::Map(_) => BuiltinMethodKind::HavocRef,
-                vir::Type::Ref => return Err(SpannedEncodingError::internal(
-                    format!("unexpected type of local variable {var:?}"),
-                    self.mir.span,
-                )),
+                vir::Type::Ref => {
+                    return Err(SpannedEncodingError::internal(
+                        format!("unexpected type of local variable {var:?}"),
+                        self.mir.span,
+                    ))
+                }
             };
-            let stmt = vir::Stmt::MethodCall( vir::MethodCall {
-                method_name: self.encoder.encode_builtin_method_use(builtin_method).with_span(loop_head_span)?,
+            let stmt = vir::Stmt::MethodCall(vir::MethodCall {
+                method_name: self
+                    .encoder
+                    .encode_builtin_method_use(builtin_method)
+                    .with_span(loop_head_span)?,
                 arguments: vec![],
                 targets: vec![var],
             });
@@ -1205,6 +1316,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         label_prefix: &str,
         bbi: BasicBlockIndex,
         return_block: CfgBlockIndex,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(CfgBlockIndex, Vec<(CfgBlockIndex, BasicBlockIndex)>)> {
         debug_assert!(!self.procedure.is_spec_block(bbi));
 
@@ -1220,19 +1332,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .insert(curr_block);
 
         if self.loop_encoder.is_loop_head(bbi) {
-            self.cfg_method.add_stmt(
-                curr_block,
-                vir::Stmt::comment("This is a loop head"),
-            );
+            self.cfg_method
+                .add_stmt(curr_block, vir::Stmt::comment("This is a loop head"));
         }
 
         self.encode_execution_flag(bbi, curr_block)?;
-        let opt_successor = self.encode_block_statements(bbi, curr_block)?;
+        let opt_successor = self.encode_block_statements(bbi, curr_block, scope_ids)?;
         let mir_successor: MirSuccessor = if let Some(successor) = opt_successor {
             // In case of unsupported statements, we do not encode the terminator
             successor
         } else {
-            self.encode_block_terminator(bbi, curr_block)?
+            self.encode_block_terminator(bbi, curr_block, scope_ids)?
         };
 
         // Make sure that the
@@ -1286,7 +1396,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let executed_flag_var = self.cfg_block_has_been_executed[&bbi].clone();
         self.cfg_method.add_stmt(
             cfg_block,
-            vir::Stmt::Assign( vir::Assign {
+            vir::Stmt::Assign(vir::Assign {
                 target: vir::Expr::local(executed_flag_var).set_pos(pos),
                 source: true.into(),
                 kind: vir::AssignKind::Copy,
@@ -1301,6 +1411,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         &mut self,
         bbi: BasicBlockIndex,
         cfg_block: CfgBlockIndex,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<Option<MirSuccessor>> {
         debug_assert!(!self.procedure.is_spec_block(bbi));
         let bb_data = &self.mir.basic_blocks[bbi];
@@ -1312,7 +1423,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 statement_index: stmt_index,
             };
             {
-                let (stmts, opt_succ) = self.encode_statement_at(location)?;
+                let (stmts, opt_succ) = self.encode_statement_at(location, scope_ids)?;
                 debug_assert!(matches!(opt_succ, None | Some(MirSuccessor::Kill)));
                 self.cfg_method.add_stmts(cfg_block, stmts);
                 if opt_succ.is_some() {
@@ -1335,6 +1446,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         &mut self,
         bbi: BasicBlockIndex,
         curr_block: CfgBlockIndex,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<MirSuccessor> {
         trace!("Encode terminator of {:?}", bbi);
         let bb_data = &self.mir.basic_blocks[bbi];
@@ -1342,7 +1454,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             block: bbi,
             statement_index: bb_data.statements.len(),
         };
-        let (stmts, opt_mir_successor) = self.encode_statement_at(location)?;
+        let (stmts, opt_mir_successor) = self.encode_statement_at(location, scope_ids)?;
         self.cfg_method.add_stmts(curr_block, stmts);
         Ok(opt_mir_successor.unwrap())
     }
@@ -1352,6 +1464,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     fn encode_statement_at(
         &mut self,
         location: mir::Location,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(Vec<vir::Stmt>, Option<MirSuccessor>)> {
         debug!("Encode location {:?}", location);
 
@@ -1364,7 +1477,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 .map(|stmts| (stmts, None))
         } else {
             let mir_term = bb_data.terminator();
-            self.encode_terminator(mir_term, location)
+            self.encode_terminator(mir_term, location, scope_ids)
                 .map(|(stmts, succ)| (stmts, Some(succ)))
         };
 
@@ -1374,9 +1487,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             Err(err) => {
                 let unsupported_msg = match err.kind() {
                     EncodingErrorKind::Unsupported(msg)
-                        if config::allow_unreachable_unsupported_code() => {
+                        if config::allow_unreachable_unsupported_code() =>
+                    {
                         msg.to_string()
-                    },
+                    }
                     _ => {
                         // Propagate the error
                         return Err(err);
@@ -1392,13 +1506,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 };
                 let stmts = vec![
                     vir::Stmt::comment(head_stmt),
-                    vir::Stmt::comment(
-                        format!("Unsupported feature: {unsupported_msg}")
-                    ),
-                    vir::Stmt::Assert( vir::Assert {
+                    vir::Stmt::comment(format!("Unsupported feature: {unsupported_msg}")),
+                    vir::Stmt::Assert(vir::Assert {
                         expr: false.into(),
                         position: pos,
-                    })
+                    }),
                 ];
                 (stmts, Some(MirSuccessor::Kill))
             }
@@ -1431,48 +1543,54 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             mir::StatementKind::Assign(box (lhs, ref rhs)) => {
                 // Array access on the LHS should always be mutable (idx is always calculated
                 // before, and just a separate local variable here)
-                let (lhs_place_encoding, ty, _) = self.mir_encoder.encode_place(lhs).with_span(span)?;
+                let (lhs_place_encoding, ty, _) =
+                    self.mir_encoder.encode_place(lhs).with_span(span)?;
                 match lhs_place_encoding {
-                    PlaceEncoding::SliceAccess { box base, index, rust_slice_ty: rust_ty, .. } |
-                    PlaceEncoding::ArrayAccess { box base, index, rust_array_ty: rust_ty, .. } => {
+                    PlaceEncoding::SliceAccess {
+                        box base,
+                        index,
+                        rust_slice_ty: rust_ty,
+                        ..
+                    }
+                    | PlaceEncoding::ArrayAccess {
+                        box base,
+                        index,
+                        rust_array_ty: rust_ty,
+                        ..
+                    } => {
                         // Current stmt is of the form `arr[idx] = val`. This does not have an expiring
                         // temporary variable, so we encode it differently from indexing into an array.
-                        self.encode_array_direct_assign(
-                            base,
-                            index,
-                            rust_ty,
-                            rhs,
-                            location,
-                        )?
+                        self.encode_array_direct_assign(base, index, rust_ty, rhs, location)?
                     }
                     _ => {
-                        let (encoded_lhs, pre_stmts) = self.postprocess_place_encoding(lhs_place_encoding, ArrayAccessKind::Mutable(None, location))
+                        let (encoded_lhs, pre_stmts) = self
+                            .postprocess_place_encoding(
+                                lhs_place_encoding,
+                                ArrayAccessKind::Mutable(None, location),
+                            )
                             .with_span(span)?;
                         stmts.extend(pre_stmts);
-                        self.encode_assign(
-                            encoded_lhs,
-                            rhs,
-                            ty,
-                            location,
-                        )?
+                        self.encode_assign(encoded_lhs, rhs, ty, location)?
                     }
                 }
             }
-            ref x => return Err(SpannedEncodingError::unsupported(
-                format!("unsupported statement kind: {x:?}"),
-                span,
-            )),
+            ref x => {
+                return Err(SpannedEncodingError::unsupported(
+                    format!("unsupported statement kind: {x:?}"),
+                    span,
+                ))
+            }
         };
         stmts.extend(encoding_stmts);
         Ok(self.set_stmts_default_pos(stmts, stmt.source_info.span))
     }
 
     fn set_stmts_default_pos(&self, stmts: Vec<vir::Stmt>, default_span: Span) -> Vec<vir::Stmt> {
-        let pos = self.encoder.error_manager().register_span(self.proc_def_id, default_span);
-        stmts
-            .into_iter()
-            .map(|s| s.set_default_pos(pos))
-            .collect()
+        let pos = self
+            .encoder
+            .error_manager()
+            .register_span(self.proc_def_id, default_span);
+        stmts.into_iter().map(|s| s.set_default_pos(pos)).collect()
     }
 
     /// Encode assignment of RHS to LHS, depending on what kind of thing the RHS is
@@ -1490,106 +1608,51 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 self.encode_assign_operand(&encoded_lhs, operand, location)?
             }
             mir::Rvalue::Aggregate(ref aggregate, ref operands) => {
-                self.encode_assign_aggregate(
-                    &encoded_lhs,
-                    ty,
-                    aggregate,
-                    operands,
-                    location
-                )?
-            },
+                self.encode_assign_aggregate(&encoded_lhs, ty, aggregate, operands, location)?
+            }
             mir::Rvalue::BinaryOp(op, box (ref left, ref right)) => {
-                self.encode_assign_binary_op(
-                    op,
-                    left,
-                    right,
-                    encoded_lhs,
-                    ty,
-                    location
-                )?
+                self.encode_assign_binary_op(op, left, right, encoded_lhs, ty, location)?
+            }
+            mir::Rvalue::CheckedBinaryOp(op, box (ref left, ref right)) => {
+                self.encode_assign_checked_binary_op(op, left, right, encoded_lhs, ty, location)?
             }
-            mir::Rvalue::CheckedBinaryOp(op, box (ref left, ref right)) => self
-                .encode_assign_checked_binary_op(
-                    op,
-                    left,
-                    right,
-                    encoded_lhs,
-                    ty,
-                    location,
-                )?,
             mir::Rvalue::UnaryOp(op, ref operand) => {
-                self.encode_assign_unary_op(
-                    op,
-                    operand,
-                    encoded_lhs,
-                    ty,
-                    location
-                )?
+                self.encode_assign_unary_op(op, operand, encoded_lhs, ty, location)?
             }
             mir::Rvalue::NullaryOp(op, op_ty) => {
-                self.encode_assign_nullary_op(
-                    op,
-                    op_ty,
-                    encoded_lhs,
-                    ty,
-                    location
-                )?
+                self.encode_assign_nullary_op(op, op_ty, encoded_lhs, ty, location)?
             }
             mir::Rvalue::Discriminant(src) => {
-                self.encode_assign_discriminant(
-                    src,
-                    location,
-                    encoded_lhs,
-                    ty
-                )?
+                self.encode_assign_discriminant(src, location, encoded_lhs, ty)?
             }
             mir::Rvalue::Ref(_region, mir_borrow_kind, place) => {
-                self.encode_assign_ref(
-                    mir_borrow_kind,
-                    place,
-                    location,
-                    encoded_lhs,
-                    ty
-                )?
+                self.encode_assign_ref(mir_borrow_kind, place, location, encoded_lhs, ty)?
             }
-            mir::Rvalue::Cast(mir::CastKind::PointerExposeAddress, ref operand, dst_ty) |
-            mir::Rvalue::Cast(mir::CastKind::PointerFromExposedAddress, ref operand, dst_ty) |
-            mir::Rvalue::Cast(mir::CastKind::IntToInt, ref operand, dst_ty) => {
-                self.encode_cast(
-                    operand,
-                    dst_ty,
-                    encoded_lhs,
-                    ty,
-                    location,
-                )?
+            mir::Rvalue::Cast(mir::CastKind::PointerExposeAddress, ref operand, dst_ty)
+            | mir::Rvalue::Cast(mir::CastKind::PointerFromExposedAddress, ref operand, dst_ty)
+            | mir::Rvalue::Cast(mir::CastKind::IntToInt, ref operand, dst_ty) => {
+                self.encode_cast(operand, dst_ty, encoded_lhs, ty, location)?
             }
             mir::Rvalue::Len(place) => {
-                self.encode_assign_sequence_len(
-                    encoded_lhs,
-                    place,
-                    ty,
-                    location,
-                )?
+                self.encode_assign_sequence_len(encoded_lhs, place, ty, location)?
             }
-            mir::Rvalue::Repeat(ref operand, times) => {
-                self.encode_assign_array_repeat_initializer(
+            mir::Rvalue::Repeat(ref operand, times) => self
+                .encode_assign_array_repeat_initializer(
                     encoded_lhs,
                     operand,
                     times,
                     ty,
                     location,
-                )?
-            }
-            mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), ref operand, cast_ty) => {
+                )?,
+            mir::Rvalue::Cast(
+                mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize),
+                ref operand,
+                cast_ty,
+            ) => {
                 let rhs_ty = self.mir_encoder.get_operand_ty(operand);
                 if rhs_ty.is_array_ref() && cast_ty.is_slice_ref() {
                     trace!("slice: operand={:?}, ty={:?}", operand, cast_ty);
-                    self.encode_assign_slice(
-                        encoded_lhs,
-                        operand,
-                        cast_ty,
-                        location,
-                    )?
+                    self.encode_assign_slice(encoded_lhs, operand, cast_ty, location)?
                 } else {
                     return Err(SpannedEncodingError::unsupported(
                         format!("unsizing a {rhs_ty} into a {cast_ty} is not supported"),
@@ -1597,15 +1660,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     ));
                 }
             }
-            mir::Rvalue::Cast(mir::CastKind::Pointer(_), _, _) |
-            mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
+            mir::Rvalue::Cast(mir::CastKind::Pointer(_), _, _)
+            | mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
                 return Err(SpannedEncodingError::unsupported(
-                    "raw pointers are not supported", span
+                    "raw pointers are not supported",
+                    span,
                 ));
             }
             mir::Rvalue::Cast(cast_kind, _, _) => {
                 return Err(SpannedEncodingError::unsupported(
-                    format!("casts {cast_kind:?} are not supported"), span
+                    format!("casts {cast_kind:?} are not supported"),
+                    span,
                 ));
             }
             mir::Rvalue::AddressOf(_, _) => {
@@ -1615,16 +1680,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
             mir::Rvalue::ThreadLocalRef(_) => {
                 return Err(SpannedEncodingError::unsupported(
-                    "references to thread-local storage are not supported", span
+                    "references to thread-local storage are not supported",
+                    span,
                 ));
             }
             mir::Rvalue::ShallowInitBox(_, op_ty) => {
-                self.encode_assign_box(
-                    op_ty,
-                    encoded_lhs,
-                    ty,
-                    location,
-                )?
+                self.encode_assign_box(op_ty, encoded_lhs, ty, location)?
             }
             mir::Rvalue::CopyForDeref(ref place) => {
                 self.encode_assign_operand(&encoded_lhs, &mir::Operand::Copy(*place), location)?
@@ -1650,13 +1711,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     }
 
     /// Encode the lhs and the rhs of the assignment that create the loan
-    fn encode_loan_places(&mut self, loan_places: &LoanPlaces<'tcx>) -> SpannedEncodingResult<(vir::Expr, Option<vir::Expr>, bool, Vec<vir::Stmt>)> {
+    fn encode_loan_places(
+        &mut self,
+        loan_places: &LoanPlaces<'tcx>,
+    ) -> SpannedEncodingResult<(vir::Expr, Option<vir::Expr>, bool, Vec<vir::Stmt>)> {
         debug!("encode_loan_places '{:?}'", loan_places);
         let location = loan_places.location;
         let span = self.mir_encoder.get_span_of_location(location);
 
-        let (expiring_base, mut stmts, expiring_ty, _) = self.encode_place(loan_places.dest, ArrayAccessKind::Mutable(None, location), location)?;
-        trace!("expiring_base: {:?}", (&expiring_base, &stmts, &expiring_ty));
+        let (expiring_base, mut stmts, expiring_ty, _) = self.encode_place(
+            loan_places.dest,
+            ArrayAccessKind::Mutable(None, location),
+            location,
+        )?;
+        trace!(
+            "expiring_base: {:?}",
+            (&expiring_base, &stmts, &expiring_ty)
+        );
 
         // the original encoding of arrays is with a sort-of magic temporary variable, so
         // `postprocess_place_encoding` will return `i32` here instead of Array$3$i32. so here
@@ -1666,12 +1737,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let (rhs_place_encoding, ..) = self.mir_encoder.encode_place(rhs_place).unwrap();
             if let PlaceEncoding::ArrayAccess { .. } = rhs_place_encoding {
                 // encode expiry of the array borrow
-                let (expired_expr, regained_array, wand_rhs) = self.array_magic_wand_at[&location].clone();
+                let (expired_expr, regained_array, wand_rhs) =
+                    self.array_magic_wand_at[&location].clone();
 
                 // expiring base is something like ref$i32, so we need .val_ref.val_int
-                let deref = self.encoder.encode_value_expr(expiring_base.clone(), expiring_ty).with_span(span)?;
+                let deref = self
+                    .encoder
+                    .encode_value_expr(expiring_base.clone(), expiring_ty)
+                    .with_span(span)?;
                 let target_ty = expiring_ty.peel_refs();
-                let expiring_base_value = self.encoder.encode_value_expr(deref, target_ty).with_span(span)?;
+                let expiring_base_value = self
+                    .encoder
+                    .encode_value_expr(deref, target_ty)
+                    .with_span(span)?;
 
                 // the original magic wand refered to the temporary variable that we created for array
                 // encoding. the expiry here refers to the non-temporary rust variable, so we need
@@ -1682,25 +1760,31 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 // so there's no LHS. instead, we add a label just before the inhale, and refer to
                 // that
                 let new_lhs_label = self.cfg_method.get_fresh_label_name();
-                stmts.push(
-                    vir::Stmt::label(new_lhs_label.clone())
-                );
+                stmts.push(vir::Stmt::label(new_lhs_label.clone()));
 
-                let wand_rhs_patched_lhs = wand_rhs
-                    .map_old_expr_label(|label| if label == "lhs" {
+                let wand_rhs_patched_lhs = wand_rhs.map_old_expr_label(|label| {
+                    if label == "lhs" {
                         trace!("{} -> {}", label, new_lhs_label);
                         new_lhs_label.clone()
                     } else {
                         label
                     }
-                );
+                });
 
-                let expiring_base_pred = self.mir_encoder.encode_place_predicate_permission(expiring_base.clone(), vir::PermAmount::Write).unwrap();
-                stmts.push(vir_stmt!{ exhale [expiring_base_pred] });
+                let expiring_base_pred = self
+                    .mir_encoder
+                    .encode_place_predicate_permission(
+                        expiring_base.clone(),
+                        vir::PermAmount::Write,
+                    )
+                    .unwrap();
+                stmts.push(vir_stmt! { exhale [expiring_base_pred] });
 
-                let arr_pred = vir::Expr::pred_permission(regained_array.clone(), vir::PermAmount::Write).unwrap();
-                stmts.push(vir_stmt!{ inhale [arr_pred] });
-                stmts.push(vir_stmt!{ inhale [wand_rhs_patched_lhs] });
+                let arr_pred =
+                    vir::Expr::pred_permission(regained_array.clone(), vir::PermAmount::Write)
+                        .unwrap();
+                stmts.push(vir_stmt! { inhale [arr_pred] });
+                stmts.push(vir_stmt! { inhale [wand_rhs_patched_lhs] });
 
                 // NOTE: the third tuple elem is called is_mut in
                 // `construct_vir_reborrowing_node_for_assignment`, and is currently only used to
@@ -1712,10 +1796,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
         }
 
-        let mut encode = |rhs_place, stmts: &mut Vec<vir::Stmt>, array_encode_kind| -> SpannedEncodingResult<_> {
-            let (restored, pre_stmts, _, _) = self.encode_place(rhs_place, array_encode_kind, location)?;
+        let mut encode = |rhs_place,
+                          stmts: &mut Vec<vir::Stmt>,
+                          array_encode_kind|
+         -> SpannedEncodingResult<_> {
+            let (restored, pre_stmts, _, _) =
+                self.encode_place(rhs_place, array_encode_kind, location)?;
             stmts.extend(pre_stmts);
-            let ref_field = self.encoder.encode_value_field(expiring_ty).with_span(span)?;
+            let ref_field = self
+                .encoder
+                .encode_value_field(expiring_ty)
+                .with_span(span)?;
             let expiring = expiring_base.clone().field(ref_field.clone());
             Ok((expiring, restored, ref_field))
         };
@@ -1726,32 +1817,43 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     mir::BorrowKind::Mut { .. } => true,
                     _ => return Err(Self::unsupported_borrow_kind(mir_borrow_kind).with_span(span)),
                 };
-                let array_encode_kind = if is_mut { ArrayAccessKind::Mutable(None, location) } else { ArrayAccessKind::Shared };
+                let array_encode_kind = if is_mut {
+                    ArrayAccessKind::Mutable(None, location)
+                } else {
+                    ArrayAccessKind::Shared
+                };
                 let (expiring, restored, _) = encode(rhs_place, &mut stmts, array_encode_kind)?;
                 assert_eq!(expiring.get_type(), restored.get_type());
                 (expiring, Some(restored), is_mut, stmts)
             }
             mir::Rvalue::Use(mir::Operand::Move(rhs_place)) => {
-                let (expiring, restored_base, ref_field) = encode(rhs_place, &mut stmts, ArrayAccessKind::Shared)?;
+                let (expiring, restored_base, ref_field) =
+                    encode(rhs_place, &mut stmts, ArrayAccessKind::Shared)?;
                 let restored = restored_base.field(ref_field);
                 assert_eq!(expiring.get_type(), restored.get_type());
                 (expiring, Some(restored), true, stmts)
             }
             mir::Rvalue::Use(mir::Operand::Copy(rhs_place)) => {
-                let (expiring, restored_base, ref_field) = encode(rhs_place, &mut stmts, ArrayAccessKind::Shared)?;
+                let (expiring, restored_base, ref_field) =
+                    encode(rhs_place, &mut stmts, ArrayAccessKind::Shared)?;
                 let restored = restored_base.field(ref_field);
                 assert_eq!(expiring.get_type(), restored.get_type());
                 (expiring, Some(restored), false, stmts)
             }
 
-            mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), ref operand, ty) => {
+            mir::Rvalue::Cast(
+                mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize),
+                ref operand,
+                ty,
+            ) => {
                 trace!("cast: operand={:?}, ty={:?}", operand, ty);
                 let place = match *operand {
                     mir::Operand::Move(place) => place,
                     mir::Operand::Copy(place) => place,
                     _ => unreachable!("operand: {:?}", operand),
                 };
-                let (restored, r_stmts, ..) = self.encode_place(place, ArrayAccessKind::Shared, location)?;
+                let (restored, r_stmts, ..) =
+                    self.encode_place(place, ArrayAccessKind::Shared, location)?;
                 stmts.extend(r_stmts);
 
                 (expiring_base, Some(restored), false, stmts)
@@ -1760,12 +1862,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             mir::Rvalue::Use(mir::Operand::Constant(ref expr)) => {
                 // TODO: Encoding of string literals is not yet supported, so
                 // do not return an expression in restored here.
-                let restored: Option<vir::Expr> =
-                    if is_str(expr.ty()) {
-                        None
-                    } else {
-                        Some(self.encoder.encode_const_expr(expr.ty(), expr.literal).with_span(span)?)
-                    };
+                let restored: Option<vir::Expr> = if is_str(expr.ty()) {
+                    None
+                } else {
+                    Some(
+                        self.encoder
+                            .encode_const_expr(expr.ty(), expr.literal)
+                            .with_span(span)?,
+                    )
+                };
 
                 (expiring_base, restored, false, stmts)
             }
@@ -1782,13 +1887,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         is_in_package_stmt: bool,
     ) -> Vec<vir::Stmt> {
         let mut stmts = if let Some(var) = self.old_to_ghost_var.get(&rhs) {
-            vec![vir::Stmt::Assign( vir::Assign {
+            vec![vir::Stmt::Assign(vir::Assign {
                 target: var.clone(),
                 source: lhs.clone(),
                 kind: vir::AssignKind::Move,
             })]
         } else {
-            vec![vir::Stmt::TransferPerm( vir::TransferPerm {
+            vec![vir::Stmt::TransferPerm(vir::TransferPerm {
                 left: lhs.clone(),
                 right: rhs.clone(),
                 unchecked: false,
@@ -1796,8 +1901,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         };
 
         if self.check_foldunfold_state && !is_in_package_stmt {
-            let pos = self.register_error(self.mir.source_info(location).span, ErrorCtxt::Unexpected);
-            stmts.push(vir::Stmt::Assert( vir::Assert {
+            let pos =
+                self.register_error(self.mir.source_info(location).span, ErrorCtxt::Unexpected);
+            stmts.push(vir::Stmt::Assert(vir::Assert {
                 expr: vir::Expr::eq_cmp(lhs, rhs),
                 position: pos,
             }));
@@ -1807,17 +1913,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     }
 
     fn encode_obtain(&mut self, expr: vir::Expr, pos: vir::Position) -> Vec<vir::Stmt> {
-        let mut stmts = vec![
-            vir::Stmt::Obtain( vir::Obtain {
-                expr: expr.clone(),
-                position: pos,
-            })
-        ];
+        let mut stmts = vec![vir::Stmt::Obtain(vir::Obtain {
+            expr: expr.clone(),
+            position: pos,
+        })];
 
         if self.check_foldunfold_state {
             let new_pos = self.encoder.error_manager().duplicate_position(pos);
-            self.encoder.error_manager().set_error(new_pos, ErrorCtxt::Unexpected);
-            stmts.push(vir::Stmt::Assert( vir::Assert {
+            self.encoder
+                .error_manager()
+                .set_error(new_pos, ErrorCtxt::Unexpected);
+            stmts.push(vir::Stmt::Assert(vir::Assert {
                 expr,
                 position: new_pos,
             }));
@@ -1828,17 +1934,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
     /// A borrow is mutable if it was a MIR unique borrow, a move of
     /// a borrow, or a argument of a function.
-    fn is_mutable_borrow(&self, loan: facts::Loan)
-        -> EncodingResult<bool>
-    {
+    fn is_mutable_borrow(&self, loan: facts::Loan) -> EncodingResult<bool> {
         if let Some(stmt) = self.polonius_info().get_assignment_for_loan(loan)? {
             Ok(match stmt.kind {
                 mir::StatementKind::Assign(box (_, ref rhs)) => match rhs {
-                    &mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _) |
-                    &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
-                    &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _) |
-                    &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
-                    &mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), _, _ty) => false,
+                    &mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _)
+                    | &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
+                    &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _)
+                    | &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
+                    &mir::Rvalue::Cast(
+                        mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize),
+                        _,
+                        _ty,
+                    ) => false,
                     &mir::Rvalue::Use(mir::Operand::Constant(_)) => false,
                     x => unreachable!("{:?}", x),
                 },
@@ -1879,11 +1987,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         is_in_package_stmt,
                     )?,
                 ReborrowingKind::Call { loan, .. } => {
-                    if let Some(slice_expiry_node) = self.construct_vir_reborrowing_node_for_slice(
-                            loan,
-                            node,
-                            location,
-                        )? {
+                    if let Some(slice_expiry_node) =
+                        self.construct_vir_reborrowing_node_for_slice(loan, node, location)?
+                    {
                         slice_expiry_node
                     } else {
                         self.construct_vir_reborrowing_node_for_call(
@@ -1891,7 +1997,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             loan,
                             node,
                             location,
-                            is_in_package_stmt
+                            is_in_package_stmt,
                         )?
                     }
                 }
@@ -1941,34 +2047,34 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let loan_location = self.polonius_info().get_loan_location(&loan);
         trace!("loan_location: {:?}", loan_location);
 
-        let loan_places = self.polonius_info().get_loan_places(&loan)
+        let loan_places = self
+            .polonius_info()
+            .get_loan_places(&loan)
             .map_err(EncodingError::from)
             .with_span(span)?;
         trace!("loan_places: {:?}", loan_places);
         trace!("node: {:?}", node);
 
-        Ok(if let Some(regained) = self.slice_created_at.get(&loan_location) {
-            let guard = self.construct_location_guard(loan_location);
-            trace!("guard: {:?}", guard);
-            trace!("regained: {:?}", regained);
-            Some(
-                vir::borrows::Node::new(
+        Ok(
+            if let Some(regained) = self.slice_created_at.get(&loan_location) {
+                let guard = self.construct_location_guard(loan_location);
+                trace!("guard: {:?}", guard);
+                trace!("regained: {:?}", regained);
+                Some(vir::borrows::Node::new(
                     guard,
                     node.loan.index().into(),
                     convert_loans_to_borrows(&node.reborrowing_loans),
                     convert_loans_to_borrows(&node.reborrowed_loans),
-                    vec![
-                        vir::Stmt::comment("hi"),
-                    ],
+                    vec![vir::Stmt::comment("hi")],
                     vec![regained.clone()],
                     Vec::new(),
                     Vec::new(),
                     None,
-                )
-            )
-        } else {
-            None
-        })
+                ))
+            } else {
+                None
+            },
+        )
     }
 
     fn construct_vir_reborrowing_node_for_assignment(
@@ -1984,11 +2090,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let node_is_leaf = node.reborrowed_loans.is_empty();
 
         let loan_location = self.polonius_info().get_loan_location(&loan);
-        let loan_places = self.polonius_info().get_loan_places(&loan)
+        let loan_places = self
+            .polonius_info()
+            .get_loan_places(&loan)
             .map_err(EncodingError::from)
-            .with_span(span)?.unwrap();
-        let (expiring, restored, is_mut, mut stmts) = self.encode_loan_places(&loan_places)
-            .with_span(span)?;
+            .with_span(span)?
+            .unwrap();
+        let (expiring, restored, is_mut, mut stmts) =
+            self.encode_loan_places(&loan_places).with_span(span)?;
         let borrowed_places = restored.clone().into_iter().collect();
         trace!("construct_vir_reborrowing_node_for_assignment(loan={:?}, loan_places={:?}, expiring={:?}, restored={:?}, stmts={:?}", loan, loan_places, expiring, restored, stmts);
 
@@ -1996,12 +2105,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         // Move the permissions from the "in loans" ("reborrowing loans") to the current loan
         if node.incoming_zombies && restored.is_some() {
-            let lhs_label = self.get_label_after_location(loan_location)?.unwrap().to_string();
+            let lhs_label = self
+                .get_label_after_location(loan_location)?
+                .unwrap()
+                .to_string();
             for &in_loan in node.reborrowing_loans.iter() {
                 // TODO: Is this the correct span?
                 if self.is_mutable_borrow(in_loan).with_span(span)? {
                     let in_location = self.polonius_info().get_loan_location(&in_loan);
-                    let in_label = self.get_label_after_location(in_location)?.unwrap().to_string();
+                    let in_label = self
+                        .get_label_after_location(in_location)?
+                        .unwrap()
+                        .to_string();
                     used_lhs_label = true;
                     stmts.extend(self.encode_transfer_permissions(
                         expiring.clone().old(in_label),
@@ -2078,9 +2193,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         // Get the borrow information.
         if !self.procedure_contracts.contains_key(&loan_location) {
             return Err(SpannedEncodingError::internal(
-                format!("There is no procedure contract for loan {loan:?}. This could happen if you \
-                         are chaining pure functions, which is not fully supported."),
-                span
+                format!(
+                    "There is no procedure contract for loan {loan:?}. This could happen if you \
+                         are chaining pure functions, which is not fully supported."
+                ),
+                span,
             ));
         }
         let (contract, fake_exprs) = self.procedure_contracts[&loan_location].clone();
@@ -2093,10 +2210,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let borrow_infos = &contract.borrow_infos;
         match borrow_infos.len().cmp(&1) {
             std::cmp::Ordering::Less => (),
-            std::cmp::Ordering::Greater => return Err(SpannedEncodingError::internal(
-                format!("We require at most one magic wand in the postcondition. But we have {:?}", borrow_infos.len()),
-                span,
-            )),
+            std::cmp::Ordering::Greater => {
+                return Err(SpannedEncodingError::internal(
+                    format!(
+                        "We require at most one magic wand in the postcondition. But we have {:?}",
+                        borrow_infos.len()
+                    ),
+                    span,
+                ))
+            }
             std::cmp::Ordering::Equal => {
                 let borrow_info = &borrow_infos[0];
 
@@ -2114,9 +2236,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
                 // Obtain the LHS permission.
                 for (path, _) in &borrow_info.blocking_paths {
-                    let (encoded_place, _, _) = self.encode_generic_place(
-                        contract.def_id, Some(loan_location), *path
-                    ).with_span(span)?;
+                    let (encoded_place, _, _) = self
+                        .encode_generic_place(contract.def_id, Some(loan_location), *path)
+                        .with_span(span)?;
                     let encoded_place = replace_fake_exprs(encoded_place);
 
                     // Move the permissions from the "in loans" ("reborrowing loans") to the current loan
@@ -2151,15 +2273,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     ErrorCtxt::ApplyMagicWandOnExpiry,
                 );
                 // Inhale the magic wand.
-                let magic_wand = vir::Expr::MagicWand( vir::MagicWand {
+                let magic_wand = vir::Expr::MagicWand(vir::MagicWand {
                     left: box lhs.clone(),
                     right: box rhs.clone(),
                     borrow: Some(loan.index().into()),
                     position: pos,
                 });
-                stmts.push(vir::Stmt::Inhale( vir::Inhale {
-                    expr: magic_wand
-                }));
+                stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: magic_wand }));
                 // Emit the apply statement.
                 let statement = vir::Stmt::apply_magic_wand(lhs, rhs, loan.index().into(), pos);
                 debug!("{:?} at {:?}", statement, loan_location);
@@ -2196,9 +2316,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         );
         let mut stmts: Vec<vir::Stmt> = vec![];
         if !loans.is_empty() {
-            let vir_reborrowing_dag =
-                self.construct_vir_reborrowing_dag(&loans, zombie_loans, location, end_location, is_in_package_stmt)?;
-            stmts.push(vir::Stmt::ExpireBorrows( vir::ExpireBorrows {
+            let vir_reborrowing_dag = self.construct_vir_reborrowing_dag(
+                &loans,
+                zombie_loans,
+                location,
+                end_location,
+                is_in_package_stmt,
+            )?;
+            stmts.push(vir::Stmt::ExpireBorrows(vir::ExpireBorrows {
                 dag: vir_reborrowing_dag,
             }));
         }
@@ -2218,15 +2343,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .polonius_info()
             .get_all_loans_dying_between(begin_loc, end_loc);
         // FIXME: is 'end_loc' correct here? What about 'begin_loc'?
-        self.encode_expiration_of_loans(all_dying_loans, &zombie_loans, begin_loc, Some(end_loc), false)
+        self.encode_expiration_of_loans(
+            all_dying_loans,
+            &zombie_loans,
+            begin_loc,
+            Some(end_loc),
+            false,
+        )
     }
 
-    fn encode_expiring_borrows_at(&mut self, location: mir::Location)
-        -> SpannedEncodingResult<Vec<vir::Stmt>>
-    {
+    fn encode_expiring_borrows_at(
+        &mut self,
+        location: mir::Location,
+    ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         debug!("encode_expiring_borrows_at '{:?}'", location);
         let (all_dying_loans, zombie_loans) = self.polonius_info().get_all_loans_dying_at(location);
-        let stmts = self.encode_expiration_of_loans(all_dying_loans, &zombie_loans, location, None, false)?;
+        let stmts =
+            self.encode_expiration_of_loans(all_dying_loans, &zombie_loans, location, None, false)?;
         Ok(self.set_stmts_default_pos(stmts, self.mir_encoder.get_span_of_location(location)))
     }
 
@@ -2235,6 +2368,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         &mut self,
         term: &mir::Terminator<'tcx>,
         location: mir::Location,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(Vec<vir::Stmt>, MirSuccessor)> {
         debug!(
             "Encode terminator '{:?}', span: {:?}",
@@ -2301,29 +2435,27 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 // Use a local variable for the discriminant.
                 // See Silicon issue https://github.com/viperproject/silicon/issues/356
                 let discr_var = match switch_ty.kind() {
-                    ty::TyKind::Bool => {
-                        self.cfg_method.add_fresh_local_var(vir::Type::Bool)
-                    }
+                    ty::TyKind::Bool => self.cfg_method.add_fresh_local_var(vir::Type::Bool),
 
-                    ty::TyKind::Int(_)
-                    | ty::TyKind::Uint(_)
-                    | ty::TyKind::Char => {
+                    ty::TyKind::Int(_) | ty::TyKind::Uint(_) | ty::TyKind::Char => {
                         self.cfg_method.add_fresh_local_var(vir::Type::Int)
                     }
 
-                    ty::TyKind::Float(ty::FloatTy::F32) => {
-                        self.cfg_method.add_fresh_local_var(vir::Type::Float(Float::F32))
-                    }
+                    ty::TyKind::Float(ty::FloatTy::F32) => self
+                        .cfg_method
+                        .add_fresh_local_var(vir::Type::Float(Float::F32)),
 
-                    ty::TyKind::Float(ty::FloatTy::F64) => {
-                        self.cfg_method.add_fresh_local_var(vir::Type::Float(Float::F64))
-                    }
+                    ty::TyKind::Float(ty::FloatTy::F64) => self
+                        .cfg_method
+                        .add_fresh_local_var(vir::Type::Float(Float::F64)),
 
                     ref x => unreachable!("{:?}", x),
                 };
-                let encoded_discr = self.mir_encoder.encode_operand_expr(discr)
+                let encoded_discr = self
+                    .mir_encoder
+                    .encode_operand_expr(discr)
                     .with_span(span)?;
-                stmts.push(vir::Stmt::Assign( vir::Assign {
+                stmts.push(vir::Stmt::Assign(vir::Assign {
                     target: discr_var.clone().into(),
                     source: encoded_discr,
                     kind: vir::AssignKind::Copy,
@@ -2344,12 +2476,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             }
                         }
 
-                        ty::TyKind::Int(_)
-                        | ty::TyKind::Uint(_)
-                        | ty::TyKind::Char => vir::Expr::eq_cmp(
-                            discr_var.clone().into(),
-                            self.encoder.encode_int_cast(value, switch_ty),
-                        ),
+                        ty::TyKind::Int(_) | ty::TyKind::Uint(_) | ty::TyKind::Char => {
+                            vir::Expr::eq_cmp(
+                                discr_var.clone().into(),
+                                self.encoder.encode_int_cast(value, switch_ty),
+                            )
+                        }
 
                         ref x => unreachable!("{:?}", x),
                     };
@@ -2386,13 +2518,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     if guard_is_bool && cfg_targets.len() == 1 {
                         let (target_guard, target) = cfg_targets.pop().unwrap();
                         let target_span = self.mir_encoder.get_span_of_basic_block(target);
-                        let default_target_span = self.mir_encoder.get_span_of_basic_block(default_target);
+                        let default_target_span =
+                            self.mir_encoder.get_span_of_basic_block(default_target);
                         if target_span > default_target_span {
                             let guard_pos = target_guard.pos();
-                            cfg_targets = vec![(
-                                target_guard.negate().set_pos(guard_pos),
-                                default_target,
-                            )];
+                            cfg_targets =
+                                vec![(target_guard.negate().set_pos(guard_pos), default_target)];
                             default_target = target;
                         } else {
                             // Undo the pop
@@ -2417,7 +2548,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
             TerminatorKind::Abort => {
                 let pos = self.register_error(term.source_info.span, ErrorCtxt::AbortTerminator);
-                stmts.push(vir::Stmt::Assert( vir::Assert {
+                stmts.push(vir::Stmt::Assert(vir::Assert {
                     expr: false.into(),
                     position: pos,
                 }));
@@ -2440,11 +2571,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 ref value,
                 ..
             } => {
-                let (encoded_lhs, pre_stmts, _, _) = self.encode_place(lhs, ArrayAccessKind::Mutable(None, location), location)?;
+                let (encoded_lhs, pre_stmts, _, _) =
+                    self.encode_place(lhs, ArrayAccessKind::Mutable(None, location), location)?;
                 stmts.extend(pre_stmts);
-                stmts.extend(
-                    self.encode_assign_operand(&encoded_lhs, value, location)?
-                );
+                stmts.extend(self.encode_assign_operand(&encoded_lhs, value, location)?);
                 (stmts, MirSuccessor::Goto(target))
             }
 
@@ -2452,21 +2582,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 ref args,
                 destination,
                 target,
-                func:
-                    mir::Operand::Constant(box mir::Constant {
-                        literal,
-                        ..
-                    }),
+                func: mir::Operand::Constant(box mir::Constant { literal, .. }),
                 ..
             } => {
                 let ty = literal.ty();
                 let func_const_val = literal.try_to_value(self.encoder.env().tcx());
                 if let ty::TyKind::FnDef(called_def_id, call_substs) = ty.kind() {
                     let called_def_id = *called_def_id;
-                    debug!("Encode function call {:?} with substs {:?}", called_def_id, call_substs);
+                    debug!(
+                        "Encode function call {:?} with substs {:?}",
+                        called_def_id, call_substs
+                    );
 
-                    let full_func_proc_name: &str =
-                        &self.encoder.env().name.get_absolute_item_name(called_def_id);
+                    let full_func_proc_name: &str = &self
+                        .encoder
+                        .env()
+                        .name
+                        .get_absolute_item_name(called_def_id);
 
                     match full_func_proc_name {
                         "std::rt::begin_panic"
@@ -2479,19 +2611,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             // Example of args[0]: 'const "internal error: entered unreachable code"'
                             let panic_message = format!("{:?}", args[0]);
 
-                            let panic_cause = self.mir_encoder.encode_panic_cause(
-                                term.source_info.span
-                            );
+                            let panic_cause =
+                                self.mir_encoder.encode_panic_cause(term.source_info.span);
                             let pos = self.register_error(
-                                    term.source_info.span,
-                                    ErrorCtxt::Panic(panic_cause),
-                                );
+                                term.source_info.span,
+                                ErrorCtxt::Panic(panic_cause),
+                            );
 
                             if self.check_panics {
                                 stmts.push(vir::Stmt::comment(format!(
                                     "Rust panic - {panic_message}"
                                 )));
-                                stmts.push(vir::Stmt::Assert( vir::Assert {
+                                stmts.push(vir::Stmt::Assert(vir::Assert {
                                     expr: false.into(),
                                     position: pos,
                                 }));
@@ -2500,94 +2631,93 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             }
                         }
 
-                        "std::boxed::Box::<T>::new"
-                        | "alloc::boxed::Box::<T>::new" => {
+                        "std::boxed::Box::<T>::new" | "alloc::boxed::Box::<T>::new" => {
                             // This is the initialization of a box
                             // args[0]: value to put in the box
                             assert_eq!(args.len(), 1);
 
-                            let (dst, pre_stmts, dest_ty, _) = self.encode_place(destination, ArrayAccessKind::Shared, location)?;
+                            let (dst, pre_stmts, dest_ty, _) =
+                                self.encode_place(destination, ArrayAccessKind::Shared, location)?;
                             stmts.extend(pre_stmts);
 
                             let boxed_ty = dest_ty.boxed_ty();
-                            let ref_field = self.encoder.encode_dereference_field(boxed_ty)
+                            let ref_field = self
+                                .encoder
+                                .encode_dereference_field(boxed_ty)
                                 .with_span(span)?;
 
                             let box_content = dst.clone().field(ref_field.clone());
 
-                            stmts.extend(
-                                self.prepare_assign_target(
-                                    dst,
-                                    ref_field,
-                                    location,
-                                    vir::AssignKind::Move,
-                                    false
-                                )?
-                            );
+                            stmts.extend(self.prepare_assign_target(
+                                dst,
+                                ref_field,
+                                location,
+                                vir::AssignKind::Move,
+                                false,
+                            )?);
 
                             // Allocate `box_content`
-                            stmts.extend(self.encode_havoc_and_initialization(&box_content).with_span(span)?);
-
-                            // Initialize `box_content`
                             stmts.extend(
-                                self.encode_assign_operand(
-                                    &box_content,
-                                    &args[0],
-                                    location
-                                )?
+                                self.encode_havoc_and_initialization(&box_content)
+                                    .with_span(span)?,
                             );
+
+                            // Initialize `box_content`
+                            stmts.extend(self.encode_assign_operand(
+                                &box_content,
+                                &args[0],
+                                location,
+                            )?);
                         }
 
-                        "std::cmp::PartialEq::eq" |
-                        "core::cmp::PartialEq::eq"
-                            if args.len() == 2 &&
-                                self.encoder.has_structural_eq_impl(
-                                    self.mir_encoder.get_operand_ty(&args[0])
-                                )
-                        => {
+                        "std::cmp::PartialEq::eq" | "core::cmp::PartialEq::eq"
+                            if args.len() == 2
+                                && self.encoder.has_structural_eq_impl(
+                                    self.mir_encoder.get_operand_ty(&args[0]),
+                                ) =>
+                        {
                             debug!("Encoding call of PartialEq::eq");
-                            stmts.extend(
-                                self.encode_cmp_function_call(
-                                    called_def_id,
-                                    location,
-                                    term.source_info.span,
-                                    args,
-                                    destination,
-                                    target,
-                                    vir::BinaryOpKind::EqCmp,
-                                    call_substs,
-                                )?
-                            );
+                            stmts.extend(self.encode_cmp_function_call(
+                                called_def_id,
+                                location,
+                                term.source_info.span,
+                                args,
+                                destination,
+                                target,
+                                vir::BinaryOpKind::EqCmp,
+                                call_substs,
+                                scope_ids,
+                            )?);
                         }
 
-                        "std::cmp::PartialEq::ne" |
-                        "core::cmp::PartialEq::ne"
-                            if args.len() == 2 &&
-                                self.encoder.has_structural_eq_impl(
-                                    self.mir_encoder.get_operand_ty(&args[0])
-                                )
-                        => {
+                        "std::cmp::PartialEq::ne" | "core::cmp::PartialEq::ne"
+                            if args.len() == 2
+                                && self.encoder.has_structural_eq_impl(
+                                    self.mir_encoder.get_operand_ty(&args[0]),
+                                ) =>
+                        {
                             debug!("Encoding call of PartialEq::ne");
-                            stmts.extend(
-                                self.encode_cmp_function_call(
-                                    called_def_id,
-                                    location,
-                                    term.source_info.span,
-                                    args,
-                                    destination,
-                                    target,
-                                    vir::BinaryOpKind::NeCmp,
-                                    call_substs,
-                                )?
-                            );
+                            stmts.extend(self.encode_cmp_function_call(
+                                called_def_id,
+                                location,
+                                term.source_info.span,
+                                args,
+                                destination,
+                                target,
+                                vir::BinaryOpKind::NeCmp,
+                                call_substs,
+                                scope_ids,
+                            )?);
                         }
 
-                        "std::ops::Fn::call"
-                        | "core::ops::Fn::call" => {
+                        "std::ops::Fn::call" | "core::ops::Fn::call" => {
                             let cl_type: ty::Ty = call_substs[0].expect_ty();
                             match cl_type.kind() {
                                 ty::TyKind::Closure(cl_def_id, _) => {
-                                    debug!("Encoding call to closure {:?} with func {:?}", cl_def_id, func_const_val);
+                                    debug!(
+                                        "Encoding call to closure {:?} with func {:?}",
+                                        cl_def_id, func_const_val
+                                    );
                                     stmts.extend(self.encode_impure_function_call(
                                         location,
                                         term.source_info.span,
@@ -2596,6 +2726,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                         target,
                                         *cl_def_id,
                                         call_substs,
+                                        scope_ids,
                                     )?);
                                 }
 
@@ -2610,18 +2741,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
                         "core::slice::<impl [T]>::len" => {
                             debug!("Encoding call of slice::len");
-                            stmts.extend(
-                                self.encode_slice_len_call(
-                                    destination,
-                                    args,
-                                    location,
-                                    span,
-                                )?
-                            );
+                            stmts.extend(self.encode_slice_len_call(
+                                destination,
+                                args,
+                                location,
+                                span,
+                            )?);
                         }
 
-                        "std::iter::Iterator::next" |
-                        "core::iter::Iterator::next" => {
+                        "std::iter::Iterator::next" | "core::iter::Iterator::next" => {
                             return Err(SpannedEncodingError::unsupported(
                                 "iterators are not fully supported yet",
                                 term.source_info.span,
@@ -2629,16 +2757,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         }
 
                         // TODO: use extern_spec
-                        "core::ops::IndexMut::index_mut" |
-                        "std::ops::IndexMut::index_mut" => {
+                        "core::ops::IndexMut::index_mut" | "std::ops::IndexMut::index_mut" => {
                             return Err(SpannedEncodingError::unsupported(
                                 "mutably slicing is not fully supported yet",
                                 term.source_info.span,
                             ));
                         }
 
-                        "core::ops::Index::index" |
-                        "std::ops::Index::index" => {
+                        "core::ops::Index::index" | "std::ops::Index::index" => {
                             debug!("Encoding call of array/slice index call");
                             stmts.extend(
                                 self.encode_sequence_index_call(
@@ -2646,7 +2772,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                     args,
                                     location,
                                     term.source_info.span,
-                                ).with_span(span)?
+                                )
+                                .with_span(span)?,
                             );
                         }
 
@@ -2654,7 +2781,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             // The called method might be a trait method.
                             // We try to resolve it to the concrete implementation
                             // and type substitutions.
-                            let (called_def_id, call_substs) = self.encoder.env().query
+                            let (called_def_id, call_substs) = self
+                                .encoder
+                                .env()
+                                .query
                                 .resolve_method_call(self.proc_def_id, called_def_id, call_substs);
 
                             let is_pure_function = self.encoder.is_pure(called_def_id, Some(call_substs)) &&
@@ -2664,7 +2794,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                 self.proc_def_id != called_def_id;
                             if is_pure_function {
                                 let def_id = called_def_id;
-                                let (function_name, _) = self.encoder
+                                let (function_name, _) = self
+                                    .encoder
                                     .encode_pure_function_use(def_id, self.proc_def_id, call_substs)
                                     .with_default_span(term.source_info.span)?;
                                 debug!("Encoding pure function call '{}'", function_name);
@@ -2674,29 +2805,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                     let _ = self.mir_encoder.encode_operand_expr(operand);
                                 }
 
-                                stmts.extend(
-                                    self.encode_pure_function_call(
-                                        location,
-                                        term.source_info.span,
-                                        args,
-                                        destination,
-                                        target,
-                                        def_id,
-                                        call_substs,
-                                    )?
-                                );
+                                stmts.extend(self.encode_pure_function_call(
+                                    location,
+                                    term.source_info.span,
+                                    args,
+                                    destination,
+                                    target,
+                                    def_id,
+                                    call_substs,
+                                )?);
                             } else {
-                                stmts.extend(
-                                    self.encode_impure_function_call(
-                                        location,
-                                        term.source_info.span,
-                                        args,
-                                        destination,
-                                        target,
-                                        called_def_id,
-                                        call_substs,
-                                    )?
-                                );
+                                stmts.extend(self.encode_impure_function_call(
+                                    location,
+                                    term.source_info.span,
+                                    args,
+                                    destination,
+                                    target,
+                                    called_def_id,
+                                    call_substs,
+                                    scope_ids,
+                                )?);
                             }
                         }
                     }
@@ -2733,12 +2861,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 // Use local variables in the switch/if.
                 // See Silicon issue https://github.com/viperproject/silicon/issues/356
                 let cond_var = self.cfg_method.add_fresh_local_var(vir::Type::Bool);
-                stmts.push(vir::Stmt::Assign( vir::Assign {
+                stmts.push(vir::Stmt::Assign(vir::Assign {
                     target: cond_var.clone().into(),
-                    source: self.mir_encoder.encode_operand_expr(cond)
-                        .with_span(
-                            self.mir_encoder.get_span_of_location(location)
-                        )?,
+                    source: self
+                        .mir_encoder
+                        .encode_operand_expr(cond)
+                        .with_span(self.mir_encoder.get_span_of_location(location))?,
                     kind: vir::AssignKind::Copy,
                 }));
 
@@ -2760,18 +2888,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
                 stmts.push(vir::Stmt::comment(format!("Rust assertion: {assert_msg}")));
                 if self.check_panics {
-                    stmts.push(vir::Stmt::Assert( vir::Assert {
+                    stmts.push(vir::Stmt::Assert(vir::Assert {
                         expr: viper_guard,
-                        position: self.register_error(
-                            term.source_info.span,
-                            error_ctxt,
-                        ),
+                        position: self.register_error(term.source_info.span, error_ctxt),
                     }));
                 } else {
                     stmts.push(vir::Stmt::comment("This assertion will not be checked"));
-                    stmts.push(vir::Stmt::Inhale( vir::Inhale {
-                        expr: viper_guard,
-                    }));
+                    stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: viper_guard }));
                 };
 
                 (stmts, MirSuccessor::Goto(target))
@@ -2793,7 +2916,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         span: Span,
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         assert!(args.len() == 1, "unexpected args to slice::len(): {args:?}");
-        let slice_operand = self.mir_encoder.encode_operand_expr(&args[0])
+        let slice_operand = self
+            .mir_encoder
+            .encode_operand_expr(&args[0])
             .with_span(span)?;
 
         let mut stmts = vec![];
@@ -2803,28 +2928,30 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         stmts.push(vir::Stmt::label(label.clone()));
 
         let slice_ty_ref = self.mir_encoder.get_operand_ty(&args[0]);
-        let slice_ty = if let ty::TyKind::Ref(_, slice_ty, _) = slice_ty_ref.kind() { slice_ty } else { unreachable!() };
-        let slice_types = self.encoder.encode_sequence_types(*slice_ty).with_span(span)?;
+        let slice_ty = if let ty::TyKind::Ref(_, slice_ty, _) = slice_ty_ref.kind() {
+            slice_ty
+        } else {
+            unreachable!()
+        };
+        let slice_types = self
+            .encoder
+            .encode_sequence_types(*slice_ty)
+            .with_span(span)?;
 
         let rhs = slice_types.len(self.encoder, slice_operand);
 
-        let (encoded_lhs, encode_stmts, ty, _) = self.encode_place(
-            destination,
-            ArrayAccessKind::Mutable(None, location),
-            location
-        ).with_span(span)?;
+        let (encoded_lhs, encode_stmts, ty, _) = self
+            .encode_place(
+                destination,
+                ArrayAccessKind::Mutable(None, location),
+                location,
+            )
+            .with_span(span)?;
         stmts.extend(encode_stmts);
 
-        stmts.extend(
-            self.encode_copy_value_assign(
-                encoded_lhs,
-                rhs,
-                ty,
-                location,
-            )?
-        );
+        stmts.extend(self.encode_copy_value_assign(encoded_lhs, rhs, ty, location)?);
 
-        self.encode_transfer_args_permissions(location, args,  &mut stmts, &label, false)?;
+        self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;
 
         // Store a label for permissions got back from the call
         debug!(
@@ -2841,13 +2968,20 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         destination: mir::Place<'tcx>,
         args: &[mir::Operand<'tcx>],
         location: mir::Location,
-        error_span: Span
+        error_span: Span,
     ) -> EncodingResult<Vec<vir::Stmt>> {
-        trace!("encode_sequence_index_call(destination={:?}, args={:?})", destination, args);
+        trace!(
+            "encode_sequence_index_call(destination={:?}, args={:?})",
+            destination,
+            args
+        );
         // args[0] is the base array/slice, args[1] is the index
         // index is not specified exactly, as std::ops::Index::index is a trait method, so all we
         // know is there needs to be an impl Index<Idx> for T
-        assert!(args.len() == 2, "unexpected args to sequence index call: {args:?}");
+        assert!(
+            args.len() == 2,
+            "unexpected args to sequence index call: {args:?}"
+        );
 
         let mut stmts = vec![];
 
@@ -2865,7 +2999,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         if !lhs_ty.is_slice_or_ref() && !lhs_ty.is_array_or_ref() {
             error_unsupported!("Non-slice LHS type '{:?}' not supported yet", lhs_ty);
         }
-        let mutability = if let ty::TyKind::Ref(_, _, mutability) = lhs_ty.kind() { mutability } else { unreachable!() };
+        let mutability = if let ty::TyKind::Ref(_, _, mutability) = lhs_ty.kind() {
+            mutability
+        } else {
+            unreachable!()
+        };
         let perm_amount = match mutability {
             Mutability::Mut => vir::PermAmount::Write,
             Mutability::Not => vir::PermAmount::Read,
@@ -2875,23 +3013,32 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         stmts.push(vir_stmt!{ inhale [vir::Expr::pred_permission(encoded_lhs.clone(), perm_amount).unwrap()] });
 
         let lhs_slice_ty = lhs_ty.peel_refs();
-        let lhs_slice_expr = self.encoder.encode_value_expr(encoded_lhs.clone(), lhs_ty)?;
+        let lhs_slice_expr = self
+            .encoder
+            .encode_value_expr(encoded_lhs.clone(), lhs_ty)?;
 
         let base_seq = self.mir_encoder.encode_operand_place(&args[0])?.unwrap();
         let base_seq_ty = self.mir_encoder.get_operand_ty(&args[0]);
 
         if !base_seq_ty.is_slice_or_ref() && !base_seq_ty.is_array_or_ref() {
-            error_unsupported!("Slicing is only supported for arrays/slices currently, not '{:?}'", base_seq_ty);
+            error_unsupported!(
+                "Slicing is only supported for arrays/slices currently, not '{:?}'",
+                base_seq_ty
+            );
         }
 
         // base_seq is expected to be ref$Array$.. or ref$Slice$.., but lookup_pure wants the
         // contained Array$../Slice$..
         let base_seq_expr = self.encoder.encode_value_expr(base_seq, base_seq_ty)?;
 
-        let enc_sequence_types = self.encoder.encode_sequence_types(base_seq_ty.peel_refs())?;
+        let enc_sequence_types = self
+            .encoder
+            .encode_sequence_types(base_seq_ty.peel_refs())?;
 
-        let j = vir_local!{ j: Int };
-        let elem_snap_ty = self.encoder.encode_snapshot_type(enc_sequence_types.elem_ty_rs)?;
+        let j = vir_local! { j: Int };
+        let elem_snap_ty = self
+            .encoder
+            .encode_snapshot_type(enc_sequence_types.elem_ty_rs)?;
         let rhs_lookup_j = enc_sequence_types.encode_lookup_pure_call(
             self.encoder,
             base_seq_expr.clone(),
@@ -2902,7 +3049,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let encoded_idx = self.mir_encoder.encode_operand_place(&args[1])?.unwrap();
         trace!("idx: {:?}", encoded_idx);
         let idx_ty = self.mir_encoder.get_operand_ty(&args[1]);
-        let idx_ident = self.encoder.env().name.get_absolute_item_name(idx_ty.ty_adt_def().unwrap().did());
+        let idx_ident = self
+            .encoder
+            .env()
+            .name
+            .get_absolute_item_name(idx_ty.ty_adt_def().unwrap().did());
         trace!("ident: {}", idx_ident);
 
         self.slice_created_at.insert(location, encoded_lhs);
@@ -2912,16 +3063,32 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         // TODO: there's fields like _5.f$start.val_int on `encoded_idx`, it just feels hacky to
         // manually re-do and hardcode them here when we probably just encoded the type
         // and the construction of the fields.
-        let usize_ty = self.encoder.env().tcx().mk_ty(ty::TyKind::Uint(ty::UintTy::Usize));
+        let usize_ty = self
+            .encoder
+            .env()
+            .tcx()
+            .mk_ty(ty::TyKind::Uint(ty::UintTy::Usize));
         let start = match &*idx_ident {
-            "std::ops::Range" | "core::ops::Range" |
-            "std::ops::RangeFrom" | "core::ops::RangeFrom" => {
-                let start_expr = self.encoder.encode_struct_field_value(encoded_idx.clone(), "start", usize_ty)?;
+            "std::ops::Range"
+            | "core::ops::Range"
+            | "std::ops::RangeFrom"
+            | "core::ops::RangeFrom" => {
+                let start_expr = self.encoder.encode_struct_field_value(
+                    encoded_idx.clone(),
+                    "start",
+                    usize_ty,
+                )?;
                 if self.check_panics {
                     // Check indexing in bounds
-                    stmts.push(vir::Stmt::Assert( vir::Assert {
-                        expr: vir_expr!{ [start_expr] >= [vir::Expr::from(0usize)] },
-                        position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range start value may be smaller than 0 when slicing".to_string())),
+                    stmts.push(vir::Stmt::Assert(vir::Assert {
+                        expr: vir_expr! { [start_expr] >= [vir::Expr::from(0usize)] },
+                        position: self.register_error(
+                            error_span,
+                            ErrorCtxt::SliceRangeBoundsCheckAssert(
+                                "the range start value may be smaller than 0 when slicing"
+                                    .to_string(),
+                            ),
+                        ),
                     }));
                 }
                 start_expr
@@ -2929,71 +3096,102 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             // RangeInclusive is wierdly differnet to all of the other Range*s in that the struct fields are private
             // and it is created with a new() fn and start/end are accessed with getter fns
             // See https://github.com/rust-lang/rust/issues/67371 for why this is the case...
-            "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => return Err(
-                EncodingError::unsupported("slicing with RangeInclusive (e.g. [x..=y]) currently not supported".to_string())
-            ),
-            "std::ops::RangeTo" | "core::ops::RangeTo" |
-            "std::ops::RangeFull" | "core::ops::RangeFull" |
-            "std::ops::RangeToInclusive" | "core::ops::RangeToInclusive" => vir::Expr::from(0usize),
-            _ => unreachable!("{}", idx_ident)
+            "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => {
+                return Err(EncodingError::unsupported(
+                    "slicing with RangeInclusive (e.g. [x..=y]) currently not supported"
+                        .to_string(),
+                ))
+            }
+            "std::ops::RangeTo"
+            | "core::ops::RangeTo"
+            | "std::ops::RangeFull"
+            | "core::ops::RangeFull"
+            | "std::ops::RangeToInclusive"
+            | "core::ops::RangeToInclusive" => vir::Expr::from(0usize),
+            _ => unreachable!("{}", idx_ident),
         };
         let end = match &*idx_ident {
-            "std::ops::Range" | "core::ops::Range" |
-            "std::ops::RangeTo" | "core::ops::RangeTo" => {
-                let end_expr = self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?;
+            "std::ops::Range" | "core::ops::Range" | "std::ops::RangeTo" | "core::ops::RangeTo" => {
+                let end_expr =
+                    self.encoder
+                        .encode_struct_field_value(encoded_idx, "end", usize_ty)?;
                 if self.check_panics {
                     // Check indexing in bounds
-                    stmts.push(vir::Stmt::Assert( vir::Assert {
-                        expr: vir_expr!{ [end_expr] <= [original_len] },
-                        position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())),
+                    stmts.push(vir::Stmt::Assert(vir::Assert {
+                        expr: vir_expr! { [end_expr] <= [original_len] },
+                        position: self.register_error(
+                            error_span,
+                            ErrorCtxt::SliceRangeBoundsCheckAssert(
+                                "the range end value may be out of bounds when slicing".to_string(),
+                            ),
+                        ),
                     }));
                 }
                 end_expr
             }
-            "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => return Err(
-                EncodingError::unsupported("slicing with RangeInclusive (e.g. [x..=y]) currently not supported".to_string())
-            ),
+            "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => {
+                return Err(EncodingError::unsupported(
+                    "slicing with RangeInclusive (e.g. [x..=y]) currently not supported"
+                        .to_string(),
+                ))
+            }
             "std::ops::RangeToInclusive" | "core::ops::RangeToInclusive" => {
-                let end_expr = self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?;
-                let end_expr = vir_expr!{ [end_expr] + [vir::Expr::from(1usize)] };
+                let end_expr =
+                    self.encoder
+                        .encode_struct_field_value(encoded_idx, "end", usize_ty)?;
+                let end_expr = vir_expr! { [end_expr] + [vir::Expr::from(1usize)] };
                 if self.check_panics {
                     // Check indexing in bounds
-                    stmts.push(vir::Stmt::Assert( vir::Assert {
-                        expr: vir_expr!{ [end_expr] <= [original_len] },
-                        position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())),
+                    stmts.push(vir::Stmt::Assert(vir::Assert {
+                        expr: vir_expr! { [end_expr] <= [original_len] },
+                        position: self.register_error(
+                            error_span,
+                            ErrorCtxt::SliceRangeBoundsCheckAssert(
+                                "the range end value may be out of bounds when slicing".to_string(),
+                            ),
+                        ),
                     }));
                 }
                 end_expr
             }
-            "std::ops::RangeFrom" | "core::ops::RangeFrom" |
-            "std::ops::RangeFull" | "core::ops::RangeFull" => original_len,
-            _ => unreachable!("{}", idx_ident)
+            "std::ops::RangeFrom"
+            | "core::ops::RangeFrom"
+            | "std::ops::RangeFull"
+            | "core::ops::RangeFull" => original_len,
+            _ => unreachable!("{}", idx_ident),
         };
 
         trace!("start: {}, end: {}", start, end);
 
         let slice_types_lhs = self.encoder.encode_sequence_types(lhs_slice_ty)?;
-        let elem_snap_ty = self.encoder.encode_snapshot_type(slice_types_lhs.elem_ty_rs)?;
+        let elem_snap_ty = self
+            .encoder
+            .encode_snapshot_type(slice_types_lhs.elem_ty_rs)?;
 
         // length
-        let length = vir_expr!{ [end] - [start] };
+        let length = vir_expr! { [end] - [start] };
         if self.check_panics {
             // start must be leq than end
             if idx_ident != "std::ops::RangeFull" && idx_ident != "core::ops::RangeFull" {
-                stmts.push(vir::Stmt::Assert( vir::Assert {
-                    expr: vir_expr!{ [start] <= [end] },
-                    position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end may be smaller than the start when slicing".to_string())),
+                stmts.push(vir::Stmt::Assert(vir::Assert {
+                    expr: vir_expr! { [start] <= [end] },
+                    position: self.register_error(
+                        error_span,
+                        ErrorCtxt::SliceRangeBoundsCheckAssert(
+                            "the range end may be smaller than the start when slicing".to_string(),
+                        ),
+                    ),
                 }));
             }
         }
 
         let slice_len_call = slice_types_lhs.len(self.encoder, lhs_slice_expr.clone());
-        stmts.push(vir_stmt!{
+        stmts.push(vir_stmt! {
             inhale [vir_expr!{ [slice_len_call] == [length] }]
         });
 
         // lookup_pure: contents
-        let i = vir_local!{ i: Int };
+        let i = vir_local! { i: Int };
         let i_var: vir::Expr = i.clone().into();
         let j_var: vir::Expr = j.clone().into();
 
@@ -3009,8 +3207,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         // NOTE: the lhs_ and rhs_ here refer to the moment the slice is created, so lhs_lookup is
         // lookup on the slice currently being created, and rhs_lookup is on the array or slice
         // being sliced
-        let lookup_eq = vir_expr!{ [lhs_lookup_i] == [rhs_lookup_j] };
-        let indices = vir_expr!{
+        let lookup_eq = vir_expr! { [lhs_lookup_i] == [rhs_lookup_j] };
+        let indices = vir_expr! {
             [vir_expr!{ [vir::Expr::from(0usize)] <= [i_var] }] &&
             (
                 [vir_expr!{ [i_var] < [slice_len_call] }] &&
@@ -3025,7 +3223,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         };
 
         // forall i: Int, j: Int :: { lhs_lookup(i), rhs_lookup(j) } 0 <= i && i < slice$len && j == i + start && start <= j && j < end ==> lhs_lookup(i) == rhs_lookup(j)
-        stmts.push(vir_stmt!{
+        stmts.push(vir_stmt! {
             inhale [
                 vir::Expr::forall(
                     vec![i, j],
@@ -3035,7 +3233,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             ]
         });
 
-        self.encode_transfer_args_permissions(location, args,  &mut stmts, &label, false)?;
+        self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;
         // Store a label for permissions got back from the call
         debug!(
             "Pure function call location {:?} has label {}",
@@ -3063,40 +3261,44 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         target: Option<BasicBlockIndex>,
         bin_op: vir::BinaryOpKind,
         substs: ty::subst::SubstsRef<'tcx>,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         let arg_ty = self.mir_encoder.get_operand_ty(&args[0]);
 
-        if self.encoder.supports_snapshot_equality(arg_ty).with_span(call_site_span)? {
-            let lhs = self.mir_encoder.encode_operand_expr(&args[0])
+        if self
+            .encoder
+            .supports_snapshot_equality(arg_ty)
+            .with_span(call_site_span)?
+        {
+            let lhs = self
+                .mir_encoder
+                .encode_operand_expr(&args[0])
                 .with_span(call_site_span)?;
-            let rhs = self.mir_encoder.encode_operand_expr(&args[1])
+            let rhs = self
+                .mir_encoder
+                .encode_operand_expr(&args[1])
                 .with_span(call_site_span)?;
 
             let expr = match bin_op {
-                vir::BinaryOpKind::EqCmp => vir::Expr::eq_cmp(
-                    vir::Expr::snap_app(lhs),
-                    vir::Expr::snap_app(rhs),
-                ),
-                vir::BinaryOpKind::NeCmp => vir::Expr::ne_cmp(
-                    vir::Expr::snap_app(lhs),
-                    vir::Expr::snap_app(rhs),
-                ),
-                _ => unreachable!()
+                vir::BinaryOpKind::EqCmp => {
+                    vir::Expr::eq_cmp(vir::Expr::snap_app(lhs), vir::Expr::snap_app(rhs))
+                }
+                vir::BinaryOpKind::NeCmp => {
+                    vir::Expr::ne_cmp(vir::Expr::snap_app(lhs), vir::Expr::snap_app(rhs))
+                }
+                _ => unreachable!(),
             };
 
-            let (target_value, mut stmts) = self.encode_pure_function_call_lhs_value(destination, target, location)
+            let (target_value, mut stmts) = self
+                .encode_pure_function_call_lhs_value(destination, target, location)
                 .with_span(call_site_span)?;
             let inhaled_expr = vir::Expr::eq_cmp(target_value, expr);
 
-            let (call_stmts, label) = self.encode_pure_function_call_site(
-                location,
-                destination,
-                target,
-                inhaled_expr,
-            )?;
+            let (call_stmts, label) =
+                self.encode_pure_function_call_site(location, destination, target, inhaled_expr)?;
             stmts.extend(call_stmts);
 
-            self.encode_transfer_args_permissions(location, args,  &mut stmts, &label, false)?;
+            self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;
 
             Ok(stmts)
         } else {
@@ -3110,6 +3312,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 target,
                 called_def_id,
                 substs,
+                scope_ids,
             )
         }
     }
@@ -3161,13 +3364,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         target: Option<BasicBlockIndex>,
         called_def_id: ProcedureDefId,
         mut substs: ty::subst::SubstsRef<'tcx>,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         let full_func_proc_name = &self
             .encoder
             .env()
             .name
             .get_absolute_item_name(called_def_id);
-        debug!("Encoding non-pure function call '{}' with args {:?} and substs {:?}", full_func_proc_name, mir_args, substs);
+        debug!(
+            "Encoding non-pure function call '{}' with args {:?} and substs {:?}",
+            full_func_proc_name, mir_args, substs
+        );
 
         // Spans for fake exprs that cannot be encoded in viper
         let mut fake_expr_spans: FxHashMap<Local, Span> = FxHashMap::default();
@@ -3179,8 +3386,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         // - the VIR Local that will hold hold the argument before the call
         // - the type of the argument
         // - if not constant, the VIR expression for the argument
-        let mut operands: Vec<(&mir::Operand<'tcx>, Local, ty::Ty<'tcx>, Option<vir::Expr>)> = vec![];
-        let mut encoded_operands = mir_args.iter()
+        let mut operands: Vec<(&mir::Operand<'tcx>, Local, ty::Ty<'tcx>, Option<vir::Expr>)> =
+            vec![];
+        let mut encoded_operands = mir_args
+            .iter()
             .map(|arg| self.mir_encoder.encode_operand_place(arg))
             .collect::<Result<Vec<Option<vir::Expr>>, _>>()
             .with_span(call_site_span)?;
@@ -3192,12 +3401,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let cl_ty = self.mir_encoder.get_operand_ty(&mir_args[0]);
             operands.push((
                 &mir_args[0],
-                mir_args[0].place()
+                mir_args[0]
+                    .place()
                     .and_then(|place| place.as_local())
-                    .map_or_else(
-                        || self.locals.get_fresh(cl_ty),
-                        |local| local.into()
-                    ),
+                    .map_or_else(|| self.locals.get_fresh(cl_ty), |local| local.into()),
                 cl_ty,
                 encoded_operands[0].take(),
             ));
@@ -3224,7 +3431,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
             // TODO: weird fix for closure call substitutions, we need to
             // prepend the identity substs of the containing method ...
-            substs = self.encoder.env().tcx().mk_substs(self.substs.iter().chain(substs));
+            substs = self
+                .encoder
+                .env()
+                .tcx()
+                .mk_substs(self.substs.iter().chain(substs));
         } else {
             for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) {
                 let arg_ty = self.mir_encoder.get_operand_ty(arg);
@@ -3232,10 +3443,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     arg,
                     arg.place()
                         .and_then(|place| place.as_local())
-                        .map_or_else(
-                            || self.locals.get_fresh(arg_ty),
-                            |local| local.into()
-                        ),
+                        .map_or_else(|| self.locals.get_fresh(arg_ty), |local| local.into()),
                     arg_ty,
                     encoded_operand.take(),
                 ));
@@ -3271,10 +3479,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     debug!("arg: {} {}", arg_place, place);
                     if !self.encoder.is_pure(called_def_id, Some(substs)) {
                         type_invs.push(
-                            self.encoder.encode_invariant_func_app(
-                                arg_ty,
-                                vir::Expr::snap_app(place.clone()),
-                            ).with_span(call_site_span)?,
+                            self.encoder
+                                .encode_invariant_func_app(
+                                    arg_ty,
+                                    vir::Expr::snap_app(place.clone()),
+                                )
+                                .with_span(call_site_span)?,
                         );
                     }
                     fake_exprs.insert(arg_place, place);
@@ -3284,28 +3494,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
                     // We have a constant.
                     constant_args.push(arg_place.clone());
-                    let val_field = self.encoder.encode_value_field(arg_ty).with_span(call_site_span)?;
+                    let val_field = self
+                        .encoder
+                        .encode_value_field(arg_ty)
+                        .with_span(call_site_span)?;
 
                     // TODO: String constants are not being encoded currently,
                     //       instead just inhale the permission to the value.
                     if !is_str(arg_ty) {
-                        let arg_val_expr = self.mir_encoder.encode_operand_expr(mir_arg)
+                        let arg_val_expr = self
+                            .mir_encoder
+                            .encode_operand_expr(mir_arg)
                             .with_span(call_site_span)?;
                         debug!("arg_val_expr: {} {}", arg_place, arg_val_expr);
                         fake_exprs.insert(arg_place.clone().field(val_field), arg_val_expr);
                     } else {
-                        fake_expr_spans.insert(
-                          arg,
-                          call_site_span
-                        );
-                        stmts.push(vir::Stmt::Inhale (
-                            vir::Inhale {
-                                expr: vir::Expr::acc_permission(
-                                    arg_place.clone().field(val_field),
-                                    vir::PermAmount::Read
-                                )
-                            }
-                        ));
+                        fake_expr_spans.insert(arg, call_site_span);
+                        stmts.push(vir::Stmt::Inhale(vir::Inhale {
+                            expr: vir::Expr::acc_permission(
+                                arg_place.clone().field(val_field),
+                                vir::PermAmount::Read,
+                            ),
+                        }));
                     }
                     let in_loop = self.loop_encoder.get_loop_depth(location.block) > 0;
                     if in_loop {
@@ -3324,7 +3534,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         let (target_local, encoded_target) = {
             if target.is_some() {
-                let (encoded_target, pre_stmts, ty, _) = self.encode_place(destination, ArrayAccessKind::Shared, location)?;
+                let (encoded_target, pre_stmts, ty, _) =
+                    self.encode_place(destination, ArrayAccessKind::Shared, location)?;
                 stmts.extend(pre_stmts);
 
                 let target_local = if let Some(target_local) = destination.as_local() {
@@ -3341,9 +3552,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 // The return type is Never
                 // This means that the function call never returns
                 // So, we `assume false` after the function call
-                stmts_after.push(vir::Stmt::Inhale( vir::Inhale {
-                    expr: false.into()
-                }));
+                stmts_after.push(vir::Stmt::Inhale(vir::Inhale { expr: false.into() }));
                 // Return a dummy local variable
                 let never_ty = self.encoder.env().tcx().mk_ty(ty::TyKind::Never);
                 (self.locals.get_fresh(never_ty), None)
@@ -3371,7 +3580,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                 }
                             }
                             */
-                            vir::Expr::PredicateAccessPredicate( vir::PredicateAccessPredicate {ref argument, ..} ) => {
+                            vir::Expr::PredicateAccessPredicate(
+                                vir::PredicateAccessPredicate { ref argument, .. },
+                            ) => {
                                 if argument.is_local() && const_arg_vars.contains(argument) {
                                     // Skip predicate permission
                                     true.into()
@@ -3389,13 +3600,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         };
 
         let procedure_contract = {
-            self.encoder.get_procedure_contract_for_call(
-                self.proc_def_id,
-                called_def_id,
-                &arguments,
-                target_local,
-                substs,
-            ).with_span(call_site_span)?
+            self.encoder
+                .get_procedure_contract_for_call(
+                    self.proc_def_id,
+                    called_def_id,
+                    &arguments,
+                    target_local,
+                    substs,
+                )
+                .with_span(call_site_span)?
         };
         assert_one_magic_wand(procedure_contract.borrow_infos.len()).with_span(call_site_span)?;
 
@@ -3405,28 +3618,36 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         // Havoc and inhale variables that store constants
         for constant_arg in &constant_args {
-            stmts.extend(self.encode_havoc_and_initialization(constant_arg).with_span(call_site_span)?);
+            stmts.extend(
+                self.encode_havoc_and_initialization(constant_arg)
+                    .with_span(call_site_span)?,
+            );
         }
 
         // Encode precondition.
-        let (
-            pre_type_spec,
-            pre_mandatory_type_spec,
-            pre_invs_spec,
-            pre_func_spec,
-        ) = self.encode_precondition_expr(&procedure_contract, substs, fake_expr_spans)?;
+        let (pre_type_spec, pre_mandatory_type_spec, pre_invs_spec, pre_func_spec) =
+            self.encode_precondition_expr(&procedure_contract, substs, fake_expr_spans)?;
+
+        let pre_func_spec = if resources::contains_resource_access_predicate(&pre_func_spec)
+            .with_span(call_site_span)?
+        {
+            resources::change_scope_id(pre_func_spec, scope_ids)
+        } else {
+            pre_func_spec
+        };
+
         let pos = self.register_error(call_site_span, ErrorCtxt::ExhaleMethodPrecondition);
-        stmts.push(vir::Stmt::Exhale( vir::Exhale {
+        stmts.push(vir::Stmt::Exhale(vir::Exhale {
             expr: replace_fake_exprs(pre_func_spec),
             position: pos,
         }));
-        stmts.push(vir::Stmt::Assert( vir::Assert {
+        stmts.push(vir::Stmt::Assert(vir::Assert {
             expr: replace_fake_exprs(pre_invs_spec),
             position: pos,
         }));
         let pre_perm_spec = replace_fake_exprs(pre_type_spec);
         assert!(!pos.is_default());
-        stmts.push(vir::Stmt::Exhale( vir::Exhale {
+        stmts.push(vir::Stmt::Exhale(vir::Exhale {
             expr: pre_perm_spec.remove_read_permissions(),
             position: pos,
         }));
@@ -3444,10 +3665,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let from_place = perm.get_place().unwrap().clone();
             let to_place = from_place.clone().old(pre_label.clone());
             let old_perm = perm.replace_place(&from_place, &to_place);
-            stmts.push(vir::Stmt::TransferPerm( vir::TransferPerm {
+            stmts.push(vir::Stmt::TransferPerm(vir::TransferPerm {
                 left: from_place,
                 right: to_place,
-                unchecked: true
+                unchecked: true,
             }));
             pre_mandatory_perms_old.push(old_perm);
         }
@@ -3498,31 +3719,39 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .collect();
 
         let post_perm_spec = replace_fake_exprs(post_type_spec);
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: post_perm_spec.remove_read_permissions(),
         }));
         if let Some(access) = return_type_spec {
-            stmts.push(vir::Stmt::Inhale( vir::Inhale {
+            stmts.push(vir::Stmt::Inhale(vir::Inhale {
                 expr: replace_fake_exprs(access),
             }));
         }
         for (from_place, to_place) in read_transfer {
-            stmts.push(vir::Stmt::TransferPerm( vir::TransferPerm {
+            stmts.push(vir::Stmt::TransferPerm(vir::TransferPerm {
                 left: replace_fake_exprs(from_place),
                 right: replace_fake_exprs(to_place),
                 unchecked: true,
             }));
         }
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: replace_fake_exprs(post_invs_spec),
         }));
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+
+        let post_func_spec = if resources::contains_resource_access_predicate(&post_func_spec)
+            .with_span(call_site_span)?
+        {
+            resources::change_scope_id(post_func_spec, scope_ids)
+        } else {
+            post_func_spec
+        };
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: replace_fake_exprs(post_func_spec),
         }));
 
         // Exhale the permissions that were moved into magic wands.
         assert!(!pos.is_default());
-        stmts.push(vir::Stmt::Exhale( vir::Exhale {
+        stmts.push(vir::Stmt::Exhale(vir::Exhale {
             expr: pre_mandatory_perm_spec,
             position: pos,
         }));
@@ -3549,14 +3778,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         called_def_id: ProcedureDefId,
         call_substs: SubstsRef<'tcx>,
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
-        let (function_name, return_type) = self.encoder.encode_pure_function_use(called_def_id, self.proc_def_id, call_substs)
+        let (function_name, return_type) = self
+            .encoder
+            .encode_pure_function_use(called_def_id, self.proc_def_id, call_substs)
             .with_span(call_site_span)?;
         debug!("Encoding pure function call '{}'", function_name);
         assert!(target.is_some());
 
         let mut arg_exprs = vec![];
         for operand in args.iter() {
-            let arg_expr = self.mir_encoder.encode_operand_expr(operand)
+            let arg_expr = self
+                .mir_encoder
+                .encode_operand_expr(operand)
                 .with_span(call_site_span)?;
             arg_exprs.push(arg_expr);
         }
@@ -3593,7 +3826,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .iter()
             .enumerate()
             .map(|(i, arg)| {
-                self.mir_encoder.encode_operand_expr_type(arg)
+                self.mir_encoder
+                    .encode_operand_expr_type(arg)
                     .map(|ty| vir::LocalVar::new(format!("x{i}"), ty))
             })
             .collect::<Result<_, _>>()
@@ -3601,7 +3835,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         let pos = self.register_error(call_site_span, ErrorCtxt::PureFunctionCall);
 
-        let type_arguments = self.encoder.encode_generic_arguments(called_def_id, call_substs).with_span(call_site_span)?;
+        let type_arguments = self
+            .encoder
+            .encode_generic_arguments(called_def_id, call_substs)
+            .with_span(call_site_span)?;
 
         let func_call = vir::Expr::func_app(
             function_name,
@@ -3609,32 +3846,27 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             arg_exprs,
             formal_args,
             return_type.clone(),
-            pos
+            pos,
         );
 
-        let (target_value, mut stmts) = self.encode_pure_function_call_lhs_value(destination, target, location)
+        let (target_value, mut stmts) = self
+            .encode_pure_function_call_lhs_value(destination, target, location)
             .with_span(call_site_span)?;
 
         let inhaled_expr = if return_type.is_domain() || return_type.is_snapshot() {
-            let (target_place, pre_stmts) = self.encode_pure_function_call_lhs_place(destination, target, location)?;
+            let (target_place, pre_stmts) =
+                self.encode_pure_function_call_lhs_place(destination, target, location)?;
             stmts.extend(pre_stmts);
-            vir::Expr::eq_cmp(
-                vir::Expr::snap_app(target_place),
-                func_call,
-            )
+            vir::Expr::eq_cmp(vir::Expr::snap_app(target_place), func_call)
         } else {
             vir::Expr::eq_cmp(target_value, func_call)
         };
 
-        let (call_stmts, label) = self.encode_pure_function_call_site(
-            location,
-            destination,
-            target,
-            inhaled_expr
-        )?;
+        let (call_stmts, label) =
+            self.encode_pure_function_call_site(location, destination, target, inhaled_expr)?;
         stmts.extend(call_stmts);
 
-        self.encode_transfer_args_permissions(location, args,  &mut stmts, &label, false)?;
+        self.encode_transfer_args_permissions(location, args, &mut stmts, &label, false)?;
         Ok(stmts)
     }
 
@@ -3646,8 +3878,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
         let span = self.mir_encoder.get_span_of_location(location);
         assert!(target.is_some());
-        let (encoded_place, pre_stmts, ty, _) = self.encode_place(destination, ArrayAccessKind::Shared, location)?;
-        let encoded_lhs_value = self.encoder.encode_value_expr(encoded_place, ty).with_span(span)?;
+        let (encoded_place, pre_stmts, ty, _) =
+            self.encode_place(destination, ArrayAccessKind::Shared, location)?;
+        let encoded_lhs_value = self
+            .encoder
+            .encode_value_expr(encoded_place, ty)
+            .with_span(span)?;
         Ok((encoded_lhs_value, pre_stmts))
     }
 
@@ -3658,7 +3894,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         location: mir::Location,
     ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
         assert!(target.is_some());
-        let (encoded, pre_stmts, _, _) = self.encode_place(destination, ArrayAccessKind::Shared, location)?;
+        let (encoded, pre_stmts, _, _) =
+            self.encode_place(destination, ArrayAccessKind::Shared, location)?;
         Ok((encoded, pre_stmts))
     }
 
@@ -3676,7 +3913,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         stmts.push(vir::Stmt::label(label.clone()));
 
         // Havoc the content of the lhs
-        let (target_place, pre_stmts) = self.encode_pure_function_call_lhs_place(destination, target, location)?;
+        let (target_place, pre_stmts) =
+            self.encode_pure_function_call_lhs_place(destination, target, location)?;
         stmts.extend(pre_stmts);
         stmts.extend(self.encode_havoc(&target_place).with_span(span)?);
         let type_predicate = self
@@ -3684,16 +3922,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .encode_place_predicate_permission(target_place.clone(), vir::PermAmount::Write)
             .unwrap();
 
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: type_predicate,
         }));
 
         // Initialize the lhs
-        stmts.push(
-            vir::Stmt::Inhale( vir::Inhale {
-                expr: call_result,
-            })
-        );
+        stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: call_result }));
 
         // Store a label for permissions got back from the call
         debug!(
@@ -3717,17 +3951,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let span = self.mir_encoder.get_span_of_location(location);
         for operand in args.iter() {
             let operand_ty = self.mir_encoder.get_operand_ty(operand);
-            let operand_place = self.mir_encoder.encode_operand_place(operand)
+            let operand_place = self
+                .mir_encoder
+                .encode_operand_place(operand)
                 .with_span(span)?;
             match (operand_place, &operand_ty.kind()) {
-                (
-                    Some(ref place),
-                    ty::TyKind::RawPtr(ty::TypeAndMut {
-                        ty: inner_ty, ..
-                    }),
-                )
+                (Some(ref place), ty::TyKind::RawPtr(ty::TypeAndMut { ty: inner_ty, .. }))
                 | (Some(ref place), ty::TyKind::Ref(_, inner_ty, _)) => {
-                    let ref_field = self.encoder
+                    let ref_field = self
+                        .encoder
                         .encode_dereference_field(*inner_ty)
                         .with_span(span)?;
                     let ref_place = place.clone().field(ref_field);
@@ -3773,9 +4005,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
     /// Encode permissions that are implicitly carried by the given local variable.
     /// `override_span` is used for local vars for fake expressions
-    fn encode_local_variable_permission(&self, local: Local, override_span: Option<Span>)
-        -> SpannedEncodingResult<vir::Expr>
-    {
+    fn encode_local_variable_permission(
+        &self,
+        local: Local,
+        override_span: Option<Span>,
+    ) -> SpannedEncodingResult<vir::Expr> {
         Ok(match self.locals.get_type(local).kind() {
             ty::TyKind::Ref(_, ty, mutability) => {
                 // Use unfolded references.
@@ -3789,13 +4023,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                 "In ProcedureEncoder::encode_local_variable_permission the local \
                                 {local:?} is fake but override_span is None",
                             ),
-                            self.mir.span
+                            self.mir.span,
                         ));
                     }
                     self.mir_encoder.get_local_span(local.into())
                 };
-                let field = self.encoder.encode_dereference_field(*ty)
-                    .with_span(span)?;
+                let field = self.encoder.encode_dereference_field(*ty).with_span(span)?;
                 let place = vir::Expr::from(encoded_local).field(field);
                 let perm_amount = match mutability {
                     Mutability::Mut => vir::PermAmount::Write,
@@ -3825,13 +4058,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         &self,
         contract: &ProcedureContract<'tcx>,
         substs: SubstsRef<'tcx>,
-        override_spans: FxHashMap<Local, Span> // spans for fake locals
-    ) -> SpannedEncodingResult<(
-        vir::Expr,
-        Vec<vir::Expr>,
-        vir::Expr,
-        vir::Expr,
-    )> {
+        override_spans: FxHashMap<Local, Span>, // spans for fake locals
+    ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Expr>, vir::Expr, vir::Expr)> {
         let borrow_infos = &contract.borrow_infos;
         let maybe_blocked_paths = if !borrow_infos.is_empty() {
             assert_eq!(
@@ -3869,12 +4097,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     type_spec.push(access);
                 }
             };
-            let access = self.encode_local_variable_permission(
-                *local,
-                override_spans.get(local).copied()
-            )?;
+            let access =
+                self.encode_local_variable_permission(*local, override_spans.get(local).copied())?;
             match access {
-                vir::Expr::BinOp( vir::BinOp {op_kind: vir::BinaryOpKind::And, left: box access1, right: box access2, ..} ) => {
+                vir::Expr::BinOp(vir::BinOp {
+                    op_kind: vir::BinaryOpKind::And,
+                    left: box access1,
+                    right: box access2,
+                    ..
+                }) => {
                     add(access1);
                     add(access2);
                 }
@@ -3889,24 +4120,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .map(|local| self.encode_prusti_local(*local).into())
             .collect();
 
-        let func_spec: Vec<vir::Expr> = contract.functional_precondition(
-                self.encoder.env(),
-                substs,
-            ).iter()
-            .map(|(assertion, assertion_substs)| self.encoder.encode_assertion(
-                assertion,
-                None,
-                &encoded_args,
-                None,
-                false,
-                self.proc_def_id,
-                assertion_substs,
-            ))
+        let func_spec: Vec<vir::Expr> = contract
+            .functional_precondition(self.encoder.env(), substs)
+            .iter()
+            .map(|(assertion, assertion_substs)| {
+                self.encoder.encode_assertion(
+                    assertion,
+                    None,
+                    &encoded_args,
+                    None,
+                    false,
+                    self.proc_def_id,
+                    assertion_substs,
+                )
+            })
             .collect::<Result<Vec<_>, _>>()?;
 
         // TODO(tymap): do this with the previous step ...
         let precondition_spans = MultiSpan::from_spans(
-            contract.functional_precondition(self.encoder.env(), substs)
+            contract
+                .functional_precondition(self.encoder.env(), substs)
                 .iter()
                 .map(|(ts, _)| self.encoder.env().query.get_def_span(ts))
                 .collect(),
@@ -3919,10 +4152,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let ty = self.locals.get_type(*arg);
             if !ty.is_unsafe_ptr() && !self.encoder.is_pure(contract.def_id, Some(substs)) {
                 invs_spec.push(
-                    self.encoder.encode_invariant_func_app(
-                        ty,
-                        self.encode_prusti_local(*arg).into(),
-                    ).with_span(precondition_spans.clone())?
+                    self.encoder
+                        .encode_invariant_func_app(ty, self.encode_prusti_local(*arg).into())
+                        .with_span(precondition_spans.clone())?,
                 );
             }
         }
@@ -3942,13 +4174,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         Option<PostconditionStrengthening>,
     )> {
         // Encode arguments and return
-        let encoded_args = self.procedure_contract()
+        let encoded_args = self
+            .procedure_contract()
             .args
             .iter()
             .map(|local| self.encode_prusti_local(*local).into())
             .collect::<Vec<_>>();
         let encoded_return = self
-            .encode_prusti_local(self.procedure_contract().returned_value).into();
+            .encode_prusti_local(self.procedure_contract().returned_value)
+            .into();
 
         debug!("procedure_contract: {:?}", self.procedure_contract());
 
@@ -3959,41 +4193,53 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         if let SpecificationItem::Refined(from, to) = &procedure_spec.pres {
             // See comment in `ProcedureContractGeneric::functional_precondition`.
-            let trait_substs = self.encoder.env().query.find_trait_method_substs(
-                self.proc_def_id,
-                self.substs,
-            ).unwrap().1;
+            let trait_substs = self
+                .encoder
+                .env()
+                .query
+                .find_trait_method_substs(self.proc_def_id, self.substs)
+                .unwrap()
+                .1;
 
-            let from_pre = from.iter()
-                .map(|spec| self.encoder.encode_assertion(
-                    spec,
-                    None,
-                    &encoded_args,
-                    None,
-                    false,
-                    self.proc_def_id,
-                    trait_substs,
-                ))
+            let from_pre = from
+                .iter()
+                .map(|spec| {
+                    self.encoder.encode_assertion(
+                        spec,
+                        None,
+                        &encoded_args,
+                        None,
+                        false,
+                        self.proc_def_id,
+                        trait_substs,
+                    )
+                })
                 .collect::<Result<Vec<_>, _>>()?
                 .into_iter()
                 .conjoin();
-            let to_pre = to.iter()
-                .map(|spec| self.encoder.encode_assertion(
-                    spec,
-                    None,
-                    &encoded_args,
-                    None,
-                    false,
-                    self.proc_def_id,
-                    self.substs,
-                ))
+            let to_pre = to
+                .iter()
+                .map(|spec| {
+                    self.encoder.encode_assertion(
+                        spec,
+                        None,
+                        &encoded_args,
+                        None,
+                        false,
+                        self.proc_def_id,
+                        self.substs,
+                    )
+                })
                 .collect::<Result<Vec<_>, _>>()?
                 .into_iter()
                 .conjoin();
 
             // The spans are used for error reporting
-            let spec_functions_span = MultiSpan::from_spans(from.iter().chain(to.iter())
-                .map(|spec_def_id| self.encoder.env().query.get_def_span(spec_def_id)).collect()
+            let spec_functions_span = MultiSpan::from_spans(
+                from.iter()
+                    .chain(to.iter())
+                    .map(|spec_def_id| self.encoder.env().query.get_def_span(spec_def_id))
+                    .collect(),
             );
 
             weakening = Some(RefinementCheckExpr {
@@ -4004,43 +4250,53 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         if let SpecificationItem::Refined(from, to) = &procedure_spec.posts {
             // See comment in `ProcedureContractGeneric::functional_precondition`.
-            let trait_substs = self.encoder.env().query.find_trait_method_substs(
-                self.proc_def_id,
-                self.substs,
-            ).unwrap().1;
+            let trait_substs = self
+                .encoder
+                .env()
+                .query
+                .find_trait_method_substs(self.proc_def_id, self.substs)
+                .unwrap()
+                .1;
 
             let from_post = from
                 .iter()
-                .map(|spec| self.encoder.encode_assertion(
-                    spec,
-                    Some(pre_label),
-                    &encoded_args,
-                    Some(&encoded_return),
-                    false,
-                    self.proc_def_id,
-                    trait_substs,
-                ))
+                .map(|spec| {
+                    self.encoder.encode_assertion(
+                        spec,
+                        Some(pre_label),
+                        &encoded_args,
+                        Some(&encoded_return),
+                        false,
+                        self.proc_def_id,
+                        trait_substs,
+                    )
+                })
                 .collect::<Result<Vec<_>, _>>()?
                 .into_iter()
                 .conjoin();
             let to_post = to
                 .iter()
-                .map(|spec| self.encoder.encode_assertion(
-                    spec,
-                    Some(pre_label),
-                    &encoded_args,
-                    Some(&encoded_return),
-                    false,
-                    self.proc_def_id,
-                    self.substs,
-                ))
+                .map(|spec| {
+                    self.encoder.encode_assertion(
+                        spec,
+                        Some(pre_label),
+                        &encoded_args,
+                        Some(&encoded_return),
+                        false,
+                        self.proc_def_id,
+                        self.substs,
+                    )
+                })
                 .collect::<Result<Vec<_>, _>>()?
                 .into_iter()
                 .conjoin();
 
             // The spans are used for error reporting
-            let spec_functions_span = MultiSpan::from_spans(from.iter().chain(to.iter())
-                .map(|spec_def_id| self.encoder.env().query.get_def_span(spec_def_id)).collect()
+            let spec_functions_span = MultiSpan::from_spans(
+                from.iter()
+                    .chain(to.iter())
+                    .map(|spec_def_id| self.encoder.env().query.get_def_span(spec_def_id))
+                    .collect(),
             );
 
             let strengthening_expr = self.wrap_arguments_into_old(
@@ -4077,51 +4333,47 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<()> {
         self.cfg_method
             .add_stmt(start_cfg_block, vir::Stmt::comment("Preconditions:"));
-        let (type_spec, mandatory_type_spec, invs_spec, func_spec) =
-            self.encode_precondition_expr(
+        let (type_spec, mandatory_type_spec, invs_spec, func_spec) = self
+            .encode_precondition_expr(
                 self.procedure_contract(),
                 self.substs,
-                FxHashMap::default()
+                FxHashMap::default(),
             )?;
         self.cfg_method.add_stmt(
             start_cfg_block,
-            vir::Stmt::Inhale( vir::Inhale {
-                expr: type_spec}),
+            vir::Stmt::Inhale(vir::Inhale { expr: type_spec }),
         );
         self.cfg_method.add_stmt(
             start_cfg_block,
-            vir::Stmt::Inhale( vir::Inhale {
+            vir::Stmt::Inhale(vir::Inhale {
                 expr: mandatory_type_spec.into_iter().conjoin(),
             }),
         );
         self.cfg_method.add_stmt(
             start_cfg_block,
-            vir::Stmt::Inhale( vir::Inhale {
-                expr: invs_spec,
-            }),
+            vir::Stmt::Inhale(vir::Inhale { expr: invs_spec }),
         );
         // Weakening assertion must be put before inhaling the precondition, otherwise the weakening
         // soundness check becomes trivially satisfied.
         if let Some(weakening_spec) = weakening_spec {
-            let pos = self.register_error(weakening_spec.spec_functions_span, ErrorCtxt::AssertMethodPreconditionWeakening);
+            let pos = self.register_error(
+                weakening_spec.spec_functions_span,
+                ErrorCtxt::AssertMethodPreconditionWeakening,
+            );
             self.cfg_method.add_stmt(
                 start_cfg_block,
-                vir::Stmt::Assert( vir::Assert {
+                vir::Stmt::Assert(vir::Assert {
                     expr: weakening_spec.refinement_check_expr,
-                    position: pos
+                    position: pos,
                 }),
             );
         }
         self.cfg_method.add_stmt(
             start_cfg_block,
-            vir::Stmt::Inhale( vir::Inhale {
-                expr: func_spec
-            }),
-        );
-        self.cfg_method.add_stmt(
-            start_cfg_block,
-            vir::Stmt::label(PRECONDITION_LABEL),
+            vir::Stmt::Inhale(vir::Inhale { expr: func_spec }),
         );
+        self.cfg_method
+            .add_stmt(start_cfg_block, vir::Stmt::label(PRECONDITION_LABEL));
         Ok(())
     }
 
@@ -4169,9 +4421,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     Mutability::Not => vir::PermAmount::Read,
                     Mutability::Mut => vir::PermAmount::Write,
                 };
-                let (place_expr, place_ty, _) = self.encode_generic_place(
-                    contract.def_id, location, place
-                ).with_span(span)?;
+                let (place_expr, place_ty, _) = self
+                    .encode_generic_place(contract.def_id, location, place)
+                    .with_span(span)?;
                 let vir_access =
                     vir::Expr::pred_permission(place_expr.clone().old(label), perm_amount).unwrap();
                 if !self.encoder.is_pure(contract.def_id, Some(substs)) {
@@ -4194,7 +4446,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 .iter()
                 .map(|(place, mutability)| encode_place_perm(*place, *mutability, pre_label))
                 .collect::<SpannedEncodingResult<_>>()?;
-            if let Some(typed::Pledge { reference, lhs: body_lhs, rhs: body_rhs}) = pledges.first() {
+            if let Some(typed::Pledge {
+                reference,
+                lhs: body_lhs,
+                rhs: body_rhs,
+            }) = pledges.first()
+            {
                 debug!(
                     "pledge reference={:?} lhs={:?} rhs={:?}",
                     reference, body_lhs, body_rhs
@@ -4238,9 +4495,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     &encoded_args,
                 )?;
                 let ty = self.locals.get_type(contract.returned_value);
-                let return_span = self.mir_encoder.get_local_span(
-                    contract.returned_value.into()
-                );
+                let return_span = self
+                    .mir_encoder
+                    .get_local_span(contract.returned_value.into());
                 let (encoded_deref, ..) = self
                     .mir_encoder
                     .encode_deref(encoded_return, ty)
@@ -4256,12 +4513,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 lhs.push(assertion_lhs);
                 rhs.push(assertion_rhs);
             }
-            let lhs = lhs
-                .into_iter()
-                .conjoin();
-            let rhs = rhs
-                .into_iter()
-                .conjoin();
+            let lhs = lhs.into_iter().conjoin();
+            let rhs = rhs.into_iter().conjoin();
             Ok(Some((lhs, rhs)))
         } else {
             Ok(None)
@@ -4294,7 +4547,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             } else {
                 // If the argument is not a reference, we wrap entire path into old.
                 assertion = assertion.fold_expr(|e| {
-                    if let vir::Expr::FuncApp(vir::FuncApp { function_name, arguments, .. }) = &e {
+                    if let vir::Expr::FuncApp(vir::FuncApp {
+                        function_name,
+                        arguments,
+                        ..
+                    }) = &e
+                    {
                         // If `assertion` is e.g. a `foo(snap(_1))` with an `_1: T` and `fn foo(x: &T)` we cannot
                         // wrap `foo(snap(old[pre](_1)))`, but should instead wrap as `foo(old[pre](snap(_1)))`
                         // TODO: this could all be fixed by making all arguments into fields (e.g. `_1.local`).
@@ -4357,9 +4615,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 place, mutability
             );
             // TODO: Use a better span
-            let (place_expr, place_ty, _) = self.encode_generic_place(
-                contract.def_id, location, *place
-            ).with_span(self.mir.span)?;
+            let (place_expr, place_ty, _) = self
+                .encode_generic_place(contract.def_id, location, *place)
+                .with_span(self.mir.span)?;
             let old_place_expr = place_expr.clone().old(pre_label);
             let mut add_type_spec = |perm_amount| {
                 let permissions =
@@ -4393,9 +4651,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .iter()
             .map(|local| self.encode_prusti_local(*local).into())
             .collect();
-        trace!("encode_postcondition_expr: encoded_args {:?} ({:?}) as {:?}", contract.args,
-               contract.args.iter().map(|a| self.locals.get_type(*a)).collect::<Vec<_>>(),
-               encoded_args);
+        trace!(
+            "encode_postcondition_expr: encoded_args {:?} ({:?}) as {:?}",
+            contract.args,
+            contract
+                .args
+                .iter()
+                .map(|a| self.locals.get_type(*a))
+                .collect::<Vec<_>>(),
+            encoded_args
+        );
 
         let encoded_return: vir::Expr = self.encode_prusti_local(contract.returned_value).into();
 
@@ -4405,13 +4670,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             self.mir.span
         };
         let mut magic_wands = Vec::new();
-        if let Some((mut lhs, mut rhs)) = self.encode_postcondition_magic_wand(
-            location,
-            contract,
-            pre_label,
-            post_label,
-            substs,
-        ).with_span(span)? {
+        if let Some((mut lhs, mut rhs)) = self
+            .encode_postcondition_magic_wand(location, contract, pre_label, post_label, substs)
+            .with_span(span)?
+        {
             if let Some((location, fake_exprs)) = magic_wand_store_info {
                 let replace_fake_exprs = |mut expr: vir::Expr| -> vir::Expr {
                     for (fake_arg, arg_expr) in fake_exprs.iter() {
@@ -4421,25 +4683,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 };
                 lhs = replace_fake_exprs(lhs);
                 rhs = replace_fake_exprs(rhs);
-                lhs = self.encoder.patch_snapshots(lhs)
-                    .with_span(self.mir.span)?;
-                rhs = self.encoder.patch_snapshots(rhs)
-                    .with_span(self.mir.span)?;
+                lhs = self.encoder.patch_snapshots(lhs).with_span(self.mir.span)?;
+                rhs = self.encoder.patch_snapshots(rhs).with_span(self.mir.span)?;
                 debug!("Insert ({:?} {:?}) at {:?}", lhs, rhs, location);
                 self.magic_wand_at_location
                     .insert(location, (post_label.to_string(), lhs.clone(), rhs.clone()));
             }
-            magic_wands.push(vir::Expr::magic_wand(lhs, rhs, loan.map(|l| l.index().into())));
+            magic_wands.push(vir::Expr::magic_wand(
+                lhs,
+                rhs,
+                loan.map(|l| l.index().into()),
+            ));
         }
 
         // Encode permissions for return type
         // TODO: Clean-up: remove unnecessary Option.
-        let return_perm = Some(
-            self.encode_local_variable_permission(
-                contract.returned_value,
-                None
-            )?
-        );
+        let return_perm =
+            Some(self.encode_local_variable_permission(contract.returned_value, None)?);
 
         // Encode functional specification
         let mut func_spec = vec![];
@@ -4458,12 +4718,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let assertion_span = self.encoder.env().query.get_def_span(typed_assertion);
             func_spec_spans.push(assertion_span);
             let assertion_pos = self.mir_encoder.register_span(assertion_span);
-            assertion = self.wrap_arguments_into_old(
-                assertion,
-                pre_label,
-                contract,
-                &encoded_args,
-            )?;
+            assertion =
+                self.wrap_arguments_into_old(assertion, pre_label, contract, &encoded_args)?;
             func_spec.push(assertion.set_default_pos(assertion_pos));
         }
         let postcondition_span = MultiSpan::from_spans(func_spec_spans);
@@ -4472,14 +4728,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         // Encode invariant for return value
         if !self.encoder.is_pure(contract.def_id, Some(substs)) {
             invs_spec.push(
-                self.encoder.encode_invariant_func_app(
-                    self.locals.get_type(contract.returned_value),
-                    encoded_return,
-                ).with_span(postcondition_span)?
+                self.encoder
+                    .encode_invariant_func_app(
+                        self.locals.get_type(contract.returned_value),
+                        encoded_return,
+                    )
+                    .with_span(postcondition_span)?,
             );
         }
 
-        let full_func_spec = func_spec.into_iter().conjoin()
+        let full_func_spec = func_spec
+            .into_iter()
+            .conjoin()
             .set_default_pos(func_spec_pos);
 
         Ok((
@@ -4513,9 +4773,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         }
         impl<'a> vir::ExprFolder for OldReplacer<'a> {
             #[allow(clippy::map_entry)]
-            fn fold_labelled_old(&mut self, vir::LabelledOld {label, base, position}: vir::LabelledOld) -> vir::Expr {
+            fn fold_labelled_old(
+                &mut self,
+                vir::LabelledOld {
+                    label,
+                    base,
+                    position,
+                }: vir::LabelledOld,
+            ) -> vir::Expr {
                 let base = self.fold_boxed(base);
-                let expr = vir::Expr::LabelledOld( vir::LabelledOld {
+                let expr = vir::Expr::LabelledOld(vir::LabelledOld {
                     label: label.clone(),
                     base,
                     position,
@@ -4567,14 +4834,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let span = self.mir.source_info(location).span;
 
         // Package magic wand(s)
-        if let Some((lhs, rhs)) = self.encode_postcondition_magic_wand(
-            None,
-            self.procedure_contract(),
-            pre_label,
-            post_label,
-            self.substs,
-        ).with_span(span)? {
-            let pos = self.register_error(self.mir.span, ErrorCtxt::PackageMagicWandForPostcondition);
+        if let Some((lhs, rhs)) = self
+            .encode_postcondition_magic_wand(
+                None,
+                self.procedure_contract(),
+                pre_label,
+                post_label,
+                self.substs,
+            )
+            .with_span(span)?
+        {
+            let pos =
+                self.register_error(self.mir.span, ErrorCtxt::PackageMagicWandForPostcondition);
 
             let blocker = mir::RETURN_PLACE;
             // TODO: Check if it really is always start and not the mid point.
@@ -4582,28 +4853,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 .polonius_info()
                 .get_point(location, facts::PointType::Start);
 
-            let opt_region = self.polonius_info()
-                .place_regions
-                .for_local(blocker);
+            let opt_region = self.polonius_info().place_regions.for_local(blocker);
             let mut package_stmts = if let Some(region) = opt_region {
-                    let (all_loans, zombie_loans) = self
-                        .polonius_info()
-                        .get_all_loans_kept_alive_by(start_point, region);
-                    self.encode_expiration_of_loans(all_loans, &zombie_loans, location, None, true)?
-                } else {
-                    // This happens when encoding the following function
-                    // ```
-                    // struct MyStruct<'tcx>(TyCtxt<'tcx>);
-                    // fn foo(tcx: TyCtxt) -> MyStruct {
-                    //     MyStruct(tcx)
-                    // }
-                    // ```
-                    return Err(SpannedEncodingError::unsupported(
-                        "the encoding of pledges does not supporte this \
+                let (all_loans, zombie_loans) = self
+                    .polonius_info()
+                    .get_all_loans_kept_alive_by(start_point, region);
+                self.encode_expiration_of_loans(all_loans, &zombie_loans, location, None, true)?
+            } else {
+                // This happens when encoding the following function
+                // ```
+                // struct MyStruct<'tcx>(TyCtxt<'tcx>);
+                // fn foo(tcx: TyCtxt) -> MyStruct {
+                //     MyStruct(tcx)
+                // }
+                // ```
+                return Err(SpannedEncodingError::unsupported(
+                    "the encoding of pledges does not supporte this \
                         kind of reborrowing",
-                        self.mir_encoder.get_span_of_location(location),
-                    ));
-                };
+                    self.mir_encoder.get_span_of_location(location),
+                ));
+            };
 
             // We need to make sure that the lhs of the magic wand is
             // fully folded before the label.
@@ -4631,10 +4900,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 let arg_span = self.mir_encoder.get_local_span(arg_index);
                 if is_reference(arg_ty) {
                     let encoded_arg = self.mir_encoder.encode_local(arg_index)?;
-                    let (deref_place, ..) =
-                        self.mir_encoder
-                            .encode_deref(encoded_arg.into(), arg_ty)
-                            .with_span(arg_span)?;
+                    let (deref_place, ..) = self
+                        .mir_encoder
+                        .encode_deref(encoded_arg.into(), arg_ty)
+                        .with_span(arg_span)?;
                     let old_deref_place = deref_place.clone().old(pre_label);
                     package_stmts.extend(self.encode_transfer_permissions(
                         deref_place,
@@ -4672,11 +4941,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 "We can have at most one magic wand in the postcondition."
             );
             for (path, _) in borrow_infos[0].blocking_paths.clone().iter() {
-                let (encoded_place, _, _) = self.encode_generic_place(
-                    self.procedure_contract().def_id, None, *path
-                ).with_span(span)?;
+                let (encoded_place, _, _) = self
+                    .encode_generic_place(self.procedure_contract().def_id, None, *path)
+                    .with_span(span)?;
                 let old_place = encoded_place.clone().old(post_label.clone());
-                stmts.extend(self.encode_transfer_permissions(old_place, encoded_place, location, true));
+                stmts.extend(self.encode_transfer_permissions(
+                    old_place,
+                    encoded_place,
+                    location,
+                    true,
+                ));
             }
         }
 
@@ -4692,29 +4966,27 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         // This clone is only due to borrow checker restrictions
         let contract = self.procedure_contract().clone();
 
-        self.cfg_method.add_stmt(return_cfg_block, vir::Stmt::comment("Exhale postcondition"));
+        self.cfg_method
+            .add_stmt(return_cfg_block, vir::Stmt::comment("Exhale postcondition"));
 
         let postcondition_label = self.cfg_method.get_fresh_label_name();
-        self.cfg_method.add_stmt(return_cfg_block, vir::Stmt::label(postcondition_label.clone()));
+        self.cfg_method.add_stmt(
+            return_cfg_block,
+            vir::Stmt::label(postcondition_label.clone()),
+        );
 
-        let (
-            type_spec,
-            return_type_spec,
-            invs_spec,
-            func_spec,
-            magic_wands,
-            _,
-        ) = self.encode_postcondition_expr(
-            None,
-            &contract,
-            PRECONDITION_LABEL,
-            &postcondition_label,
-            None,
-            false,
-            None,
-            true,
-            self.substs,
-        )?;
+        let (type_spec, return_type_spec, invs_spec, func_spec, magic_wands, _) = self
+            .encode_postcondition_expr(
+                None,
+                &contract,
+                PRECONDITION_LABEL,
+                &postcondition_label,
+                None,
+                false,
+                None,
+                true,
+                self.substs,
+            )?;
 
         let type_inv_pos = self.register_error(
             self.mir.span,
@@ -4775,10 +5047,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         vir::PermAmount::Write,
                     )
                     .unwrap();
-                for stmt in self
-                    .encode_obtain(deref_pred, type_inv_pos)
-                    .drain(..)
-                {
+                for stmt in self.encode_obtain(deref_pred, type_inv_pos).drain(..) {
                     self.cfg_method.add_stmt(return_cfg_block, stmt);
                 }
 
@@ -4806,25 +5075,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
                 self.cfg_method.add_stmt(
                     return_cfg_block,
-                    vir::Stmt::Assign( vir::Assign {
+                    vir::Stmt::Assign(vir::Assign {
                         target: var,
                         source: encoded_deref,
-                        kind: vir::AssignKind::Move
+                        kind: vir::AssignKind::Move,
                     }),
                 );
             }
         }
 
         // Fold the result.
-        self.cfg_method.add_stmt(
-            return_cfg_block,
-            vir::Stmt::comment("Fold the result"),
-        );
+        self.cfg_method
+            .add_stmt(return_cfg_block, vir::Stmt::comment("Fold the result"));
         let ty = self.locals.get_type(contract.returned_value);
         let encoded_return: vir::Expr = self.encode_prusti_local(contract.returned_value).into();
-        let return_span = self.mir_encoder.get_local_span(contract.returned_value.into());
+        let return_span = self
+            .mir_encoder
+            .get_local_span(contract.returned_value.into());
         let encoded_return_expr = if is_reference(ty) {
-            let (encoded_deref, ..) = self.mir_encoder
+            let (encoded_deref, ..) = self
+                .mir_encoder
                 .encode_deref(encoded_return, ty)
                 .with_span(return_span)?;
             encoded_deref
@@ -4835,7 +5105,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .mir_encoder
             .encode_place_predicate_permission(encoded_return_expr, vir::PermAmount::Write)
             .unwrap();
-        let obtain_return_stmt = vir::Stmt::Obtain( vir::Obtain {
+        let obtain_return_stmt = vir::Stmt::Obtain(vir::Obtain {
             expr: return_pred,
             position: type_inv_pos,
         });
@@ -4848,12 +5118,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             vir::Stmt::comment("Assert possible strengthening"),
         );
         if let Some(strengthening_spec) = strengthening_spec {
-            let patched_strengthening_spec =
-                self.replace_old_places_with_ghost_vars(None, strengthening_spec.refinement_check_expr);
-            let pos = self.register_error(strengthening_spec.spec_functions_span, ErrorCtxt::AssertMethodPostconditionStrengthening);
+            let patched_strengthening_spec = self
+                .replace_old_places_with_ghost_vars(None, strengthening_spec.refinement_check_expr);
+            let pos = self.register_error(
+                strengthening_spec.spec_functions_span,
+                ErrorCtxt::AssertMethodPostconditionStrengthening,
+            );
             self.cfg_method.add_stmt(
                 return_cfg_block,
-                vir::Stmt::Assert( vir::Assert {
+                vir::Stmt::Assert(vir::Assert {
                     expr: patched_strengthening_spec,
                     position: pos,
                 }),
@@ -4869,7 +5142,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let patched_func_spec = self.replace_old_places_with_ghost_vars(None, func_spec);
         self.cfg_method.add_stmt(
             return_cfg_block,
-            vir::Stmt::Assert( vir::Assert {
+            vir::Stmt::Assert(vir::Assert {
                 expr: patched_func_spec,
                 position: func_pos,
             }),
@@ -4883,7 +5156,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let patched_invs_spec = self.replace_old_places_with_ghost_vars(None, invs_spec);
         self.cfg_method.add_stmt(
             return_cfg_block,
-            vir::Stmt::Assert( vir::Assert {
+            vir::Stmt::Assert(vir::Assert {
                 expr: patched_invs_spec,
                 position: type_inv_pos,
             }),
@@ -4899,7 +5172,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         debug_assert!(!perm_pos.is_default());
         self.cfg_method.add_stmt(
             return_cfg_block,
-            vir::Stmt::Exhale( vir::Exhale {
+            vir::Stmt::Exhale(vir::Exhale {
                 expr: patched_type_spec,
                 position: perm_pos,
             }),
@@ -4912,7 +5185,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         if let Some(access) = return_type_spec {
             self.cfg_method.add_stmt(
                 return_cfg_block,
-                vir::Stmt::Exhale( vir::Exhale {
+                vir::Stmt::Exhale(vir::Exhale {
                     expr: access,
                     position: perm_pos,
                 }),
@@ -4926,7 +5199,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         for magic_wand in magic_wands {
             self.cfg_method.add_stmt(
                 return_cfg_block,
-                vir::Stmt::Exhale( vir::Exhale {
+                vir::Stmt::Exhale(vir::Exhale {
                     expr: magic_wand,
                     position: perm_pos,
                 }),
@@ -4972,7 +5245,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         place: &vir::Expr,
     ) -> vir::Expr {
         let tmp_var = self.get_pure_var_for_preserving_value(loop_head, place);
-        vir::Expr::BinOp ( vir::BinOp {
+        vir::Expr::BinOp(vir::BinOp {
             op_kind: vir::BinaryOpKind::EqCmp,
             left: box tmp_var.into(),
             right: box place.clone(),
@@ -4995,7 +5268,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         let snap_array = vir::Expr::snap_app(array_base);
         let old_snap_array = vir::Expr::old(snap_array.clone(), old_label);
-        vir_expr!{ [snap_array] == [old_snap_array] }
+        vir_expr! { [snap_array] == [old_snap_array] }
     }
 
     /// Arguments:
@@ -5037,17 +5310,21 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let enclosing_permission_forest = if loops.len() > 1 {
             let next_to_last = loops.len() - 2;
             let enclosing_loop_head = loops[next_to_last];
-            Some(self.loop_encoder.compute_loop_invariant(
-                enclosing_loop_head,
-                self.cached_loop_invariant_block[&enclosing_loop_head],
-            ).map_err(|err| match err {
-                LoopAnalysisError::UnsupportedPlaceContext(place_ctxt, loc) => {
-                    SpannedEncodingError::internal(
-                        format!("loop uses the unexpected PlaceContext '{place_ctxt:?}'"),
-                        self.mir_encoder.get_span_of_location(loc),
+            Some(
+                self.loop_encoder
+                    .compute_loop_invariant(
+                        enclosing_loop_head,
+                        self.cached_loop_invariant_block[&enclosing_loop_head],
                     )
-                }
-            })?)
+                    .map_err(|err| match err {
+                        LoopAnalysisError::UnsupportedPlaceContext(place_ctxt, loc) => {
+                            SpannedEncodingError::internal(
+                                format!("loop uses the unexpected PlaceContext '{place_ctxt:?}'"),
+                                self.mir_encoder.get_span_of_location(loc),
+                            )
+                        }
+                    })?,
+            )
         } else {
             None
         };
@@ -5073,16 +5350,21 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     ExprOrArrayBase::ArrayBase(b) | ExprOrArrayBase::SliceBase(b) => (b, true),
                 };
 
-                debug!("kind={:?} mir_place={:?} encoded_place={:?} ty={:?}", kind, mir_place, encoded_place, ty);
+                debug!(
+                    "kind={:?} mir_place={:?} encoded_place={:?} ty={:?}",
+                    kind, mir_place, encoded_place, ty
+                );
                 match kind {
                     // Gives read permission to this node. It must not be a leaf node.
                     PermissionKind::ReadNode => {
                         if is_array_access {
                             // if it's already there, it's at least read -> nothing to do here
-                            array_pred_perms.entry(encoded_place)
+                            array_pred_perms
+                                .entry(encoded_place)
                                 .or_insert(vir::PermAmount::Read);
                         } else {
-                            let perm = vir::Expr::acc_permission(encoded_place, vir::PermAmount::Read);
+                            let perm =
+                                vir::Expr::acc_permission(encoded_place, vir::PermAmount::Read);
                             permissions.push(perm);
                         }
                     }
@@ -5092,7 +5374,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         if is_array_access {
                             array_pred_perms.insert(encoded_place, vir::PermAmount::Write);
                         } else {
-                            let perm = vir::Expr::acc_permission(encoded_place, vir::PermAmount::Write);
+                            let perm =
+                                vir::Expr::acc_permission(encoded_place, vir::PermAmount::Write);
                             permissions.push(perm);
                         }
                     }
@@ -5110,7 +5393,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             .loop_encoder
                             .is_definitely_initialised(mir_place, loop_head);
                         debug!("    perm_amount={} def_init={}", perm_amount, def_init);
-                        if let Some(base) = utils::try_pop_deref(self.encoder.env().tcx(), mir_place)
+                        if let Some(base) =
+                            utils::try_pop_deref(self.encoder.env().tcx(), mir_place)
                         {
                             // will panic if attempting to encode unsupported type
                             let ref_ty = self.mir_encoder.encode_place(base).unwrap().1;
@@ -5151,8 +5435,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                         &field_place,
                                     ));
                                 }
-                                if def_init
-                                    && !(mutbl == &Mutability::Not && drop_read_references)
+                                if def_init && !(mutbl == &Mutability::Not && drop_read_references)
                                 {
                                     permissions.push(
                                         vir::Expr::pred_permission(field_place, perm_amount)
@@ -5162,12 +5445,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             }
                             _ => {
                                 if is_array_access {
-                                    array_pred_perms.entry(encoded_place)
-                                        .and_modify(|e| if perm_amount == vir::PermAmount::Write { *e = vir::PermAmount::Write; })
+                                    array_pred_perms
+                                        .entry(encoded_place)
+                                        .and_modify(|e| {
+                                            if perm_amount == vir::PermAmount::Write {
+                                                *e = vir::PermAmount::Write;
+                                            }
+                                        })
                                         .or_insert(perm_amount);
                                 } else {
                                     permissions.push(
-                                        vir::Expr::pred_permission(encoded_place, perm_amount).unwrap(),
+                                        vir::Expr::pred_permission(encoded_place, perm_amount)
+                                            .unwrap(),
                                     );
                                 }
 
@@ -5178,23 +5467,30 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                         // that we will lose information about the children of that
                                         // place after the loop and we need to preserve it via local
                                         // variables.
-                                        let encoded_child = self.mir_encoder.encode_place(child_place)?.0;
+                                        let encoded_child =
+                                            self.mir_encoder.encode_place(child_place)?.0;
                                         match encoded_child.into_array_base() {
                                             ExprOrArrayBase::Expr(e) => {
-                                                equalities.push(self.construct_value_preserving_equality(
-                                                    loop_head,
-                                                    &e,
-                                                ));
+                                                equalities.push(
+                                                    self.construct_value_preserving_equality(
+                                                        loop_head, &e,
+                                                    ),
+                                                );
                                             }
                                             ExprOrArrayBase::ArrayBase(b) => {
-                                                let eq = self.construct_value_preserving_array_equality(loop_head, b);
+                                                let eq = self
+                                                    .construct_value_preserving_array_equality(
+                                                        loop_head, b,
+                                                    );
                                                 // arrays can be mentioned multiple times, so we
                                                 // need to check here
                                                 if !equalities.contains(&eq) {
                                                     equalities.push(eq);
                                                 }
                                             }
-                                            ExprOrArrayBase::SliceBase(_) => unimplemented!("slices in loops not yet implemented"),
+                                            ExprOrArrayBase::SliceBase(_) => unimplemented!(
+                                                "slices in loops not yet implemented"
+                                            ),
                                         }
                                     }
                                 }
@@ -5217,21 +5513,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         trace!("array_pred_perms: {:?}", array_pred_perms);
         for (place, perm) in array_pred_perms.into_iter() {
             permissions.push(
-                vir::Expr::pred_permission(place, perm)
-                    .expect("invalid place in array_pred_perms")
+                vir::Expr::pred_permission(place, perm).expect("invalid place in array_pred_perms"),
             );
         }
 
         // encode type invariants
         let mut invs_spec = Vec::new();
         for permission in &permissions {
-            if let vir::Expr::PredicateAccessPredicate( vir::PredicateAccessPredicate {predicate_type, argument, ..}) = permission {
+            if let vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate {
+                predicate_type,
+                argument,
+                ..
+            }) = permission
+            {
                 let ty = self.encoder.decode_type_predicate_type(predicate_type)?;
                 if !self.encoder.is_pure(self.proc_def_id, Some(self.substs)) {
-                    let inv_func_app = self.encoder.encode_invariant_func_app(
-                        ty,
-                        (**argument).clone(),
-                    )?;
+                    let inv_func_app = self
+                        .encoder
+                        .encode_invariant_func_app(ty, (**argument).clone())?;
                     invs_spec.push(inv_func_app);
                 }
             }
@@ -5281,6 +5580,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         &self,
         loop_head: BasicBlockIndex,
         _loop_inv_block: BasicBlockIndex,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(Vec<vir::Expr>, MultiSpan)> {
         let spec_blocks = self.get_loop_spec_blocks(loop_head);
         trace!(
@@ -5297,17 +5597,31 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             for stmt in &self.mir.basic_blocks[bbi].statements {
                 if let mir::StatementKind::Assign(box (
                     _,
-                    mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
-                )) = stmt.kind {
+                    mir::Rvalue::Aggregate(
+                        box mir::AggregateKind::Closure(cl_def_id, cl_substs),
+                        _,
+                    ),
+                )) = stmt.kind
+                {
                     if let Some(spec) = self.encoder.get_loop_specs(cl_def_id.to_def_id()) {
-                        encoded_specs.push(self.encoder.encode_invariant(
+                        let invariant_expr = self.encoder.encode_invariant(
                             self.mir,
                             bbi,
                             self.proc_def_id,
                             cl_substs,
-                        )?);
+                        )?;
+                        if resources::contains_resource_access_predicate(&invariant_expr)
+                            .with_span(self.mir.span)?
+                        {
+                            encoded_specs
+                                .push(resources::change_scope_id(invariant_expr, scope_ids));
+                        } else {
+                            encoded_specs.push(invariant_expr);
+                        }
                         let invariant = match spec {
-                            prusti_interface::specs::typed::LoopSpecification::Invariant(inv) => inv,
+                            prusti_interface::specs::typed::LoopSpecification::Invariant(inv) => {
+                                inv
+                            }
                             _ => continue,
                         };
                         encoded_spec_spans.push(self.encoder.env().tcx().def_span(invariant));
@@ -5325,6 +5639,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         loop_head: BasicBlockIndex,
         loop_inv_block: BasicBlockIndex,
         after_loop_iteration: bool,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         trace!(
             "[enter] encode_loop_invariant_exhale_stmts loop_head={:?} \
@@ -5337,10 +5652,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 .insert(loop_head, FxHashMap::default());
         }
         let (func_spec, func_spec_span) =
-            self.encode_loop_invariant_specs(loop_head, loop_inv_block)?;
-        let (permissions, equalities, invs_spec) =
-            self.encode_loop_invariant_permissions(loop_head, loop_inv_block, true)
-                .with_span(func_spec_span.clone())?;
+            self.encode_loop_invariant_specs(loop_head, loop_inv_block, scope_ids)?;
+        let (permissions, equalities, invs_spec) = self
+            .encode_loop_invariant_permissions(loop_head, loop_inv_block, true)
+            .with_span(func_spec_span.clone())?;
 
         // TODO: use different positions, and generate different error messages, for the exhale
         // before the loop and after the loop body
@@ -5373,7 +5688,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 stmts.push(vir::Stmt::label(label));
             }
             for (place, field) in &self.pure_var_for_preserving_value_map[&loop_head] {
-                stmts.push(vir::Stmt::Assign( vir::Assign {
+                stmts.push(vir::Stmt::Assign(vir::Assign {
                     target: field.into(),
                     source: place.clone(),
                     kind: vir::AssignKind::Ghost,
@@ -5382,28 +5697,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         }
         assert!(!assert_pos.is_default());
         let obtain_predicates = permissions.iter().map(|p| {
-            vir::Stmt::Obtain( vir::Obtain {
+            vir::Stmt::Obtain(vir::Obtain {
                 expr: p.clone(),
                 position: assert_pos,
             }) // TODO: Use a better position.
         });
         stmts.extend(obtain_predicates);
 
-        stmts.push(vir::Stmt::Exhale( vir::Exhale {
+        stmts.push(vir::Stmt::Exhale(vir::Exhale {
             expr: func_spec.into_iter().conjoin(),
             position: assert_pos,
         }));
-        stmts.push(vir::Stmt::Assert( vir::Assert {
+        stmts.push(vir::Stmt::Assert(vir::Assert {
             expr: invs_spec.into_iter().conjoin(),
             position: exhale_pos,
         }));
         let equalities_expr = equalities.into_iter().conjoin();
-        stmts.push(vir::Stmt::Assert( vir::Assert {
+        stmts.push(vir::Stmt::Assert(vir::Assert {
             expr: equalities_expr,
             position: exhale_pos,
         }));
         let permission_expr = permissions.into_iter().conjoin();
-        stmts.push(vir::Stmt::Exhale( vir::Exhale {
+        stmts.push(vir::Stmt::Exhale(vir::Exhale {
             expr: permission_expr,
             position: exhale_pos,
         }));
@@ -5430,13 +5745,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let mut stmts = vec![vir::Stmt::comment(format!(
             "Inhale the loop permissions invariant of block {loop_head:?}"
         ))];
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: permission_expr,
         }));
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: equality_expr,
         }));
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: invs_spec.into_iter().conjoin(),
         }));
         Ok(stmts)
@@ -5447,6 +5762,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         loop_head: BasicBlockIndex,
         loop_inv_block: BasicBlockIndex,
         after_loop: bool,
+        scope_ids: &[isize],
     ) -> SpannedEncodingResult<(Vec<vir::Stmt>, MultiSpan)> {
         trace!(
             "[enter] encode_loop_invariant_inhale_fnspec_stmts loop_head={:?} after_loop={}",
@@ -5454,12 +5770,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             after_loop
         );
         let (func_spec, func_spec_span) =
-            self.encode_loop_invariant_specs(loop_head, loop_inv_block)?;
+            self.encode_loop_invariant_specs(loop_head, loop_inv_block, scope_ids)?;
 
         let mut stmts = vec![vir::Stmt::comment(format!(
             "Inhale the loop fnspec invariant of block {loop_head:?}"
         ))];
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: func_spec.into_iter().conjoin(),
         }));
         Ok((stmts, func_spec_span))
@@ -5469,7 +5785,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let var_name = self.locals.get_name(local);
         let typ = self
             .encoder
-            .encode_type(self.locals.get_type(local)).unwrap(); // will panic if attempting to encode unsupported type
+            .encode_type(self.locals.get_type(local))
+            .unwrap(); // will panic if attempting to encode unsupported type
         vir::LocalVar::new(var_name, typ)
     }
 
@@ -5500,9 +5817,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> EncodingResult<(vir::Expr, ty::Ty<'tcx>, Option<usize>)> {
         let mir_encoder = if let Some(location) = location {
             let block = &self.mir.basic_blocks[location.block];
-            assert_eq!(block.statements.len(), location.statement_index, "expected terminator location");
+            assert_eq!(
+                block.statements.len(),
+                location.statement_index,
+                "expected terminator location"
+            );
             match &block.terminator().kind {
-                mir::TerminatorKind::Call{ args, destination, .. } => {
+                mir::TerminatorKind::Call {
+                    args, destination, ..
+                } => {
                     let tcx = self.encoder.env().tcx();
                     let arg_tys = args.iter().map(|arg| arg.ty(self.mir, tcx)).collect();
                     let return_ty = destination.ty(self.mir, tcx).ty;
@@ -5528,7 +5851,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
             Place::SubstitutedPlace {
                 substituted_root,
-                place
+                place,
             } => {
                 let (place_encoding, ty, variant) = mir_encoder.encode_place(place)?;
                 let expr = place_encoding.try_into_expr()?;
@@ -5538,7 +5861,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 }
                 use vir::ExprFolder;
                 impl ExprFolder for RootReplacer {
-                    fn fold_local(&mut self, vir::Local {position, ..}: vir::Local) -> vir::Expr {
+                    fn fold_local(&mut self, vir::Local { position, .. }: vir::Local) -> vir::Expr {
                         vir::Expr::local_with_pos(self.new_root.clone(), position)
                     }
                 }
@@ -5623,15 +5946,20 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         //   inhale lookup_pure(array, index) == encoded_rhs
         //   // now we have all the contents as before, just one item updated
 
-        let (encoded_array, mut stmts) = self.postprocess_place_encoding(
-            base,
-            ArrayAccessKind::Shared,  // shouldn't be nested, so doesn't matter[tm]
-        ).with_span(span)?;
+        let (encoded_array, mut stmts) = self
+            .postprocess_place_encoding(
+                base,
+                ArrayAccessKind::Shared, // shouldn't be nested, so doesn't matter[tm]
+            )
+            .with_span(span)?;
 
         let label = self.cfg_method.get_fresh_label_name();
         stmts.push(vir::Stmt::label(&label));
 
-        let sequence_types = self.encoder.encode_sequence_types(array_ty).with_span(span)?;
+        let sequence_types = self
+            .encoder
+            .encode_sequence_types(array_ty)
+            .with_span(span)?;
         let sequence_len = sequence_types.len(self.encoder, encoded_array.clone());
 
         let array_acc_expr = vir::Expr::predicate_access_predicate(
@@ -5641,54 +5969,78 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         );
 
         // exhale and re-inhale to havoc
-        stmts.push(vir_stmt!{ exhale [array_acc_expr] });
-        stmts.push(vir_stmt!{ inhale [array_acc_expr] });
+        stmts.push(vir_stmt! { exhale [array_acc_expr] });
+        stmts.push(vir_stmt! { inhale [array_acc_expr] });
 
-        let old = |e| { vir::Expr::labelled_old(&label, e) };
+        let old = |e| vir::Expr::labelled_old(&label, e);
 
         // For sequences with fixed len (e.g. arrays) this will be Some
         if sequence_types.sequence_len.is_none() {
             // inhale that len unchanged
-            let len_eq = vir_expr!{ [ sequence_len ] == [ old(sequence_len.clone()) ] };
-            stmts.push(vir_stmt!{ inhale [len_eq] });
+            let len_eq = vir_expr! { [ sequence_len ] == [ old(sequence_len.clone()) ] };
+            stmts.push(vir_stmt! { inhale [len_eq] });
         }
 
-        let idx_val_int = self.encoder.patch_snapshots(vir::Expr::snap_app(index)).with_span(span)?;
+        let idx_val_int = self
+            .encoder
+            .patch_snapshots(vir::Expr::snap_app(index))
+            .with_span(span)?;
 
         // inhale infos about array contents back
-        let i_var: vir::Expr = vir_local!{ i: Int }.into();
-        let zero_le_i = vir_expr!{ [vir::Expr::from(0usize)] <= [ i_var ] };
-        let i_lt_len = vir_expr!{ [ i_var ] < [ sequence_len ] };
-        let i_ne_idx = vir_expr!{ [ i_var ] != [ old(idx_val_int.clone()) ] };
-        let idx_conditions = vir_expr!{ [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
-        let lookup_ret_ty = self.encoder.encode_snapshot_type(sequence_types.elem_ty_rs).with_span(span)?;
-        let lookup_array_i = sequence_types.encode_lookup_pure_call(self.encoder, encoded_array.clone(), i_var.clone(), lookup_ret_ty.clone());
+        let i_var: vir::Expr = vir_local! { i: Int }.into();
+        let zero_le_i = vir_expr! { [vir::Expr::from(0usize)] <= [ i_var ] };
+        let i_lt_len = vir_expr! { [ i_var ] < [ sequence_len ] };
+        let i_ne_idx = vir_expr! { [ i_var ] != [ old(idx_val_int.clone()) ] };
+        let idx_conditions = vir_expr! { [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
+        let lookup_ret_ty = self
+            .encoder
+            .encode_snapshot_type(sequence_types.elem_ty_rs)
+            .with_span(span)?;
+        let lookup_array_i = sequence_types.encode_lookup_pure_call(
+            self.encoder,
+            encoded_array.clone(),
+            i_var.clone(),
+            lookup_ret_ty.clone(),
+        );
         // FIXME: using `old` here is a work-around for https://github.com/viperproject/prusti-dev/issues/877
         // FIXME: which is due to an issue in Silicon, see https://github.com/viperproject/silicon/issues/603
-        let lookup_array_i_old = sequence_types.encode_lookup_pure_call(self.encoder, old(encoded_array.clone()), i_var, lookup_ret_ty.clone());
-        let lookup_same_as_old = vir_expr!{ [lookup_array_i] == [old(lookup_array_i)] };
-        let forall_body = vir_expr!{ [idx_conditions] ==> [lookup_same_as_old] };
-        let all_others_unchanged = vir_expr!{ forall i: Int :: { [lookup_array_i_old] } :: [ forall_body ] };
+        let lookup_array_i_old = sequence_types.encode_lookup_pure_call(
+            self.encoder,
+            old(encoded_array.clone()),
+            i_var,
+            lookup_ret_ty.clone(),
+        );
+        let lookup_same_as_old = vir_expr! { [lookup_array_i] == [old(lookup_array_i)] };
+        let forall_body = vir_expr! { [idx_conditions] ==> [lookup_same_as_old] };
+        let all_others_unchanged =
+            vir_expr! { forall i: Int :: { [lookup_array_i_old] } :: [ forall_body ] };
 
-        stmts.push(vir_stmt!{ inhale [ all_others_unchanged ]});
+        stmts.push(vir_stmt! { inhale [ all_others_unchanged ]});
 
-        let tmp = vir::Expr::from(self.cfg_method.add_fresh_local_var(sequence_types.elem_pred_type.clone()));
+        let tmp = vir::Expr::from(
+            self.cfg_method
+                .add_fresh_local_var(sequence_types.elem_pred_type.clone()),
+        );
         stmts.extend(
-            self.encode_assign(
-                tmp.clone(),
-                rhs,
-                sequence_types.elem_ty_rs,
-                location,
-            ).with_span(span)?
+            self.encode_assign(tmp.clone(), rhs, sequence_types.elem_ty_rs, location)
+                .with_span(span)?,
         );
 
-        let tmp_val_field = self.encoder.encode_value_expr(tmp, sequence_types.elem_ty_rs).with_span(span)?;
+        let tmp_val_field = self
+            .encoder
+            .encode_value_expr(tmp, sequence_types.elem_ty_rs)
+            .with_span(span)?;
 
-        let indexed_lookup_pure_call = sequence_types
-            .encode_lookup_pure_call(self.encoder, encoded_array, old(idx_val_int), lookup_ret_ty);
-        let indexed_updated = vir_expr!{ [ indexed_lookup_pure_call ] == [ vir::Expr::snap_app(tmp_val_field) ] };
+        let indexed_lookup_pure_call = sequence_types.encode_lookup_pure_call(
+            self.encoder,
+            encoded_array,
+            old(idx_val_int),
+            lookup_ret_ty,
+        );
+        let indexed_updated =
+            vir_expr! { [ indexed_lookup_pure_call ] == [ vir::Expr::snap_app(tmp_val_field) ] };
 
-        stmts.push(vir_stmt!{ inhale [ indexed_updated ] });
+        stmts.push(vir_stmt! { inhale [ indexed_updated ] });
 
         Ok(stmts)
     }
@@ -5703,12 +6055,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         trace!(
             "[enter] encode_assign_operand(lhs={}, operand={:?}, location={:?})",
-            lhs, operand, location
+            lhs,
+            operand,
+            location
         );
         let span = self.mir_encoder.get_span_of_location(location);
         let stmts = match operand {
             mir::Operand::Move(place) => {
-                let (src, mut stmts, ty, _) = self.encode_place(*place, ArrayAccessKind::Shared, location)?;
+                let (src, mut stmts, ty, _) =
+                    self.encode_place(*place, ArrayAccessKind::Shared, location)?;
                 let encode_stmts = match ty.kind() {
                     ty::TyKind::RawPtr(..) | ty::TyKind::Ref(..) => {
                         // Reborrow.
@@ -5718,26 +6073,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             field.clone(),
                             location,
                             vir::AssignKind::Move,
-                            false
+                            false,
                         )?;
-                        alloc_stmts.push(vir::Stmt::Assign( vir::Assign {
+                        alloc_stmts.push(vir::Stmt::Assign(vir::Assign {
                             target: lhs.clone().field(field.clone()),
                             source: src.field(field),
                             kind: vir::AssignKind::Move,
                         }));
                         alloc_stmts
                     }
-                    _ if config::enable_purification_optimization() &&
-                         prusti_common::vir::optimizations::purification::is_purifiable_type(lhs.get_type()) => {
+                    _ if config::enable_purification_optimization()
+                        && prusti_common::vir::optimizations::purification::is_purifiable_type(
+                            lhs.get_type(),
+                        ) =>
+                    {
                         self.encode_copy2(src, lhs.clone(), ty, location)?
                     }
                     _ => {
                         // Just move.
-                        let move_assign =
-                            vir::Stmt::Assign( vir::Assign {
-                                target: lhs.clone(),
-                                source: src,
-                                kind: vir::AssignKind::Move
+                        let move_assign = vir::Stmt::Assign(vir::Assign {
+                            target: lhs.clone(),
+                            source: src,
+                            kind: vir::AssignKind::Move,
                         });
                         vec![move_assign]
                     }
@@ -5755,7 +6112,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
 
             mir::Operand::Copy(place) => {
-                let (src, mut stmts, ty, _) = self.encode_place(*place, ArrayAccessKind::Shared, location)?;
+                let (src, mut stmts, ty, _) =
+                    self.encode_place(*place, ArrayAccessKind::Shared, location)?;
                 let encode_stmts = match ty.kind() {
                     ty::TyKind::RawPtr(..) => {
                         return Err(SpannedEncodingError::unsupported(
@@ -5771,9 +6129,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             ref_field.clone(),
                             location,
                             vir::AssignKind::SharedBorrow(loan.index().into()),
-                            false
+                            false,
                         )?;
-                        stmts.push(vir::Stmt::Assign( vir::Assign {
+                        stmts.push(vir::Stmt::Assign(vir::Assign {
                             target: lhs.clone().field(ref_field.clone()),
                             source: src.field(ref_field),
                             kind: vir::AssignKind::SharedBorrow(loan.index().into()),
@@ -5805,17 +6163,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             field.clone(),
                             location,
                             vir::AssignKind::Copy,
-                            true
+                            true,
                         )?;
                         // TODO Encoding of string literals is not yet supported,
                         // so do not encode an assignment if the RHS is a string
                         if !is_str(ty) {
                             // Initialize the constant
-                            let const_val = self.encoder
+                            let const_val = self
+                                .encoder
                                 .encode_const_expr(ty, expr.literal)
                                 .with_span(span)?;
                             // Initialize value of lhs
-                            stmts.push(vir::Stmt::Assign( vir::Assign {
+                            stmts.push(vir::Stmt::Assign(vir::Assign {
                                 target: lhs.clone().field(field),
                                 source: const_val,
                                 kind: vir::AssignKind::Copy,
@@ -5854,13 +6213,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             right
         );
         let span = self.mir_encoder.get_span_of_location(location);
-        let encoded_left = self.mir_encoder.encode_operand_expr(left)
+        let encoded_left = self.mir_encoder.encode_operand_expr(left).with_span(span)?;
+        let encoded_right = self
+            .mir_encoder
+            .encode_operand_expr(right)
             .with_span(span)?;
-        let encoded_right = self.mir_encoder.encode_operand_expr(right)
+        let encoded_value = self
+            .mir_encoder
+            .encode_bin_op_expr(op, encoded_left, encoded_right, ty)
             .with_span(span)?;
-        let encoded_value =
-            self.mir_encoder.encode_bin_op_expr(op, encoded_left, encoded_right, ty)
-                .with_span(span)?;
         self.encode_copy_value_assign(encoded_lhs, encoded_value, ty, location)
     }
 
@@ -5873,12 +6234,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         let span = self.mir_encoder.get_span_of_location(location);
         let field = self.encoder.encode_value_field(ty).with_span(span)?;
-        self.encode_copy_value_assign2(
-            encoded_lhs,
-            encoded_rhs,
-            field,
-            location
-        )
+        self.encode_copy_value_assign2(encoded_lhs, encoded_rhs, field, location)
     }
 
     /// Assignment with a(n overflow-)checked binary operation on the RHS.
@@ -5904,20 +6260,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         } else {
             unreachable!()
         };
-        let encoded_left = self.mir_encoder.encode_operand_expr(left)
+        let encoded_left = self.mir_encoder.encode_operand_expr(left).with_span(span)?;
+        let encoded_right = self
+            .mir_encoder
+            .encode_operand_expr(right)
             .with_span(span)?;
-        let encoded_right = self.mir_encoder.encode_operand_expr(right)
+        let encoded_value = self
+            .mir_encoder
+            .encode_bin_op_expr(op, encoded_left.clone(), encoded_right.clone(), operand_ty)
+            .with_span(span)?;
+        let encoded_check = self
+            .mir_encoder
+            .encode_bin_op_check(op, encoded_left, encoded_right, operand_ty)
             .with_span(span)?;
-        let encoded_value = self.mir_encoder.encode_bin_op_expr(
-            op,
-            encoded_left.clone(),
-            encoded_right.clone(),
-            operand_ty,
-        ).with_span(span)?;
-        let encoded_check =
-            self.mir_encoder
-                .encode_bin_op_check(op, encoded_left, encoded_right, operand_ty)
-                .with_span(span)?;
         let field_types = if let ty::TyKind::Tuple(ref x) = ty.kind() {
             x
         } else {
@@ -5927,19 +6282,25 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             .encoder
             .encode_raw_ref_field("tuple_0".to_string(), field_types[0])
             .with_span(span)?;
-        let value_field_value = self.encoder.encode_value_field(field_types[0]).with_span(span)?;
+        let value_field_value = self
+            .encoder
+            .encode_value_field(field_types[0])
+            .with_span(span)?;
         let check_field = self
             .encoder
             .encode_raw_ref_field("tuple_1".to_string(), field_types[1])
             .with_span(span)?;
-        let check_field_value = self.encoder.encode_value_field(field_types[1]).with_span(span)?;
+        let check_field_value = self
+            .encoder
+            .encode_value_field(field_types[1])
+            .with_span(span)?;
         let mut stmts = if !self
             .init_info
             .is_vir_place_accessible(&encoded_lhs, location)
         {
             let mut alloc_stmts = self.encode_havoc(&encoded_lhs).with_span(span)?;
             let mut inhale_acc = |place| {
-                alloc_stmts.push(vir::Stmt::Inhale( vir::Inhale {
+                alloc_stmts.push(vir::Stmt::Inhale(vir::Inhale {
                     expr: vir::Expr::acc_permission(place, vir::PermAmount::Write),
                 }));
             };
@@ -5962,7 +6323,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             Vec::with_capacity(2)
         };
         // Initialize lhs.field
-        stmts.push(vir::Stmt::Assign( vir::Assign {
+        stmts.push(vir::Stmt::Assign(vir::Assign {
             target: encoded_lhs
                 .clone()
                 .field(value_field)
@@ -5970,7 +6331,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             source: encoded_value,
             kind: vir::AssignKind::Copy,
         }));
-        stmts.push(vir::Stmt::Assign( vir::Assign {
+        stmts.push(vir::Stmt::Assign(vir::Assign {
             target: encoded_lhs.field(check_field).field(check_field_value),
             source: encoded_check,
             kind: vir::AssignKind::Copy,
@@ -5994,10 +6355,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             op,
             operand
         );
-        let encoded_val = self.mir_encoder.encode_operand_expr(operand)
-            .with_span(
-                self.mir_encoder.get_span_of_location(location)
-            )?;
+        let encoded_val = self
+            .mir_encoder
+            .encode_operand_expr(operand)
+            .with_span(self.mir_encoder.get_span_of_location(location))?;
         let encoded_value = self.mir_encoder.encode_unary_op_expr(op, encoded_val);
         // Initialize `lhs.field`
         self.encode_copy_value_assign(encoded_lhs, encoded_value, ty, location)
@@ -6019,10 +6380,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let param_env = tcx.param_env(self.proc_def_id);
         let layout = match tcx.layout_of(param_env.and(op_ty)) {
             Ok(layout_of) => layout_of.layout,
-            Err(_) => return Err(SpannedEncodingError::internal(
-                format!("could not fetch layout of type `{op_ty}` while translating `{op:?}`"),
-                self.mir.source_info(location).span,
-            )),
+            Err(_) => {
+                return Err(SpannedEncodingError::internal(
+                    format!("could not fetch layout of type `{op_ty}` while translating `{op:?}`"),
+                    self.mir.source_info(location).span,
+                ))
+            }
         };
         let bytes = match op {
             mir::NullOp::SizeOf => layout.size().bytes(),
@@ -6030,12 +6393,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             mir::NullOp::AlignOf => layout.align().abi.bytes(),
         };
         let bytes_vir = vir::Expr::from(bytes);
-        self.encode_copy_value_assign(
-            encoded_lhs,
-            bytes_vir,
-            ty,
-            location,
-        )
+        self.encode_copy_value_assign(encoded_lhs, bytes_vir, ty, location)
     }
 
     fn encode_assign_box(
@@ -6047,10 +6405,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         assert_eq!(op_ty, ty.boxed_ty());
         let span = self.mir_encoder.get_span_of_location(location);
-        let ref_field = self.encoder.encode_dereference_field(op_ty)
-            .with_span(
-                self.mir_encoder.get_span_of_location(location)
-            )?;
+        let ref_field = self
+            .encoder
+            .encode_dereference_field(op_ty)
+            .with_span(self.mir_encoder.get_span_of_location(location))?;
         let box_content = encoded_lhs.clone().field(ref_field.clone());
 
         let mut stmts = self.prepare_assign_target(
@@ -6058,14 +6416,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             ref_field,
             location,
             vir::AssignKind::Move,
-            false
+            false,
         )?;
 
         // Allocate `box_content`
         // TODO: This is also encoding initialization, which should be avoided because both
         //   `Rvalue::NullaryOp(NullOp::Box)` and `Rvalue::ShallowInitBox` don't initialize the
         //   content of the box.
-        stmts.extend(self.encode_havoc_and_initialization(&box_content).with_span(span)?);
+        stmts.extend(
+            self.encode_havoc_and_initialization(&box_content)
+                .with_span(span)?,
+        );
 
         // Leave `box_content` uninitialized
         Ok(stmts)
@@ -6086,7 +6447,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             location
         );
         let span = self.mir_encoder.get_span_of_location(location);
-        let (encoded_src, mut stmts, src_ty, _) = self.encode_place(src, ArrayAccessKind::Shared, location)?;
+        let (encoded_src, mut stmts, src_ty, _) =
+            self.encode_place(src, ArrayAccessKind::Shared, location)?;
         let encode_stmts = match src_ty.kind() {
             ty::TyKind::Adt(adt_def, _) if !adt_def.is_box() => {
                 let num_variants = adt_def.variants().len();
@@ -6103,16 +6465,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             self.proc_def_id,
                         );
                     }
-                    let encoded_rhs = self.encoder.encode_discriminant_func_app(
-                        encoded_src,
-                        *adt_def,
-                    )?;
-                    self.encode_copy_value_assign(
-                        encoded_lhs,
-                        encoded_rhs,
-                        ty,
-                        location
-                    )?
+                    let encoded_rhs = self
+                        .encoder
+                        .encode_discriminant_func_app(encoded_src, *adt_def)?;
+                    self.encode_copy_value_assign(encoded_lhs, encoded_rhs, ty, location)?
                 } else {
                     vec![]
                 }
@@ -6121,12 +6477,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             ty::TyKind::Int(_) | ty::TyKind::Uint(_) | ty::TyKind::Float(_) => {
                 let value_field = self.encoder.encode_value_field(src_ty).with_span(span)?;
                 let discr_value = encoded_src.field(value_field);
-                self.encode_copy_value_assign(
-                    encoded_lhs,
-                    discr_value,
-                    ty,
-                    location
-                )?
+                self.encode_copy_value_assign(encoded_lhs, discr_value, ty, location)?
             }
 
             ref x => {
@@ -6157,26 +6508,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let span = self.mir_encoder.get_span_of_location(location);
         let loan = self.polonius_info().get_loan_at_location(location);
         let (vir_assign_kind, array_encode_kind) = match mir_borrow_kind {
-            mir::BorrowKind::Shared =>
-                (vir::AssignKind::SharedBorrow(loan.index().into()), ArrayAccessKind::Shared),
-            mir::BorrowKind::Mut { .. } =>
-                (vir::AssignKind::MutableBorrow(loan.index().into()),
-                 ArrayAccessKind::Mutable(Some(loan.index().into()), location)),
+            mir::BorrowKind::Shared => (
+                vir::AssignKind::SharedBorrow(loan.index().into()),
+                ArrayAccessKind::Shared,
+            ),
+            mir::BorrowKind::Mut { .. } => (
+                vir::AssignKind::MutableBorrow(loan.index().into()),
+                ArrayAccessKind::Mutable(Some(loan.index().into()), location),
+            ),
             _ => return Err(Self::unsupported_borrow_kind(mir_borrow_kind).with_span(span)),
         };
-        let (encoded_value, mut stmts, _, _) = self.encode_place(place, array_encode_kind, location)?;
+        let (encoded_value, mut stmts, _, _) =
+            self.encode_place(place, array_encode_kind, location)?;
         // Initialize ref_var.ref_field
         let field = self.encoder.encode_value_field(ty).with_span(span)?;
-        stmts.extend(
-            self.prepare_assign_target(
-                encoded_lhs.clone(),
-                field.clone(),
-                location,
-                vir_assign_kind,
-                false
-            )?
-        );
-        stmts.push(vir::Stmt::Assign( vir::Assign {
+        stmts.extend(self.prepare_assign_target(
+            encoded_lhs.clone(),
+            field.clone(),
+            location,
+            vir_assign_kind,
+            false,
+        )?);
+        stmts.push(vir::Stmt::Assign(vir::Assign {
             target: encoded_lhs.field(field),
             source: encoded_value,
             kind: vir_assign_kind,
@@ -6218,7 +6571,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         ty: ty::Ty<'tcx>,
         location: mir::Location,
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
-        trace!("encode_assign_slice(lhs={:?}, operand={:?}, ty={:?})", encoded_lhs, operand, ty);
+        trace!(
+            "encode_assign_slice(lhs={:?}, operand={:?}, ty={:?})",
+            encoded_lhs,
+            operand,
+            ty
+        );
         debug_assert!(ty.is_slice_ref());
         let span = self.mir_encoder.get_span_of_location(location);
         let mut stmts = Vec::new();
@@ -6231,24 +6589,33 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         } else {
             unreachable!("encode_assign_slice on a non-ref?!")
         };
-        let slice_types = self.encoder.encode_sequence_types(*slice_ty).with_span(span)?;
+        let slice_types = self
+            .encoder
+            .encode_sequence_types(*slice_ty)
+            .with_span(span)?;
 
         stmts.extend(self.encode_havoc(&encoded_lhs).with_span(span)?);
         let val_ref_field = self.encoder.encode_value_field(ty).with_span(span)?;
         let slice_expr = encoded_lhs.field(val_ref_field);
-        stmts.push(vir_stmt!{ inhale [vir::Expr::FieldAccessPredicate( vir::FieldAccessPredicate {
-            base: box slice_expr.clone(),
-            permission: vir::PermAmount::Write,
-            position: vir::Position::default(),
-        })]});
+        stmts.push(
+            vir_stmt! { inhale [vir::Expr::FieldAccessPredicate( vir::FieldAccessPredicate {
+                base: box slice_expr.clone(),
+                permission: vir::PermAmount::Write,
+                position: vir::Position::default(),
+            })]},
+        );
 
-        let slice_perm = vir::Expr::PredicateAccessPredicate( vir::PredicateAccessPredicate {
+        let slice_perm = vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate {
             predicate_type: slice_types.sequence_pred_type.clone(),
             argument: box slice_expr.clone(),
-            permission: if is_mut { vir::PermAmount::Write } else { vir::PermAmount::Read },
+            permission: if is_mut {
+                vir::PermAmount::Write
+            } else {
+                vir::PermAmount::Read
+            },
             position: vir::Position::default(),
         });
-        stmts.push(vir_stmt!{ inhale [slice_perm] });
+        stmts.push(vir_stmt! { inhale [slice_perm] });
 
         let (rhs_place, rhs_ty) = if let mir::Operand::Move(place) = operand {
             let (rhs_place, rhs_ty, ..) = self.mir_encoder.encode_place(*place).with_span(span)?;
@@ -6265,7 +6632,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         let val_ref_field = self.encoder.encode_value_field(rhs_ty).with_span(span)?;
         let rhs_expr = rhs_place.field(val_ref_field);
-        let sequence_types = self.encoder.encode_sequence_types(*rhs_array_ty).with_span(span)?;
+        let sequence_types = self
+            .encoder
+            .encode_sequence_types(*rhs_array_ty)
+            .with_span(span)?;
 
         let slice_len_call = slice_types.len(self.encoder, slice_expr.clone());
 
@@ -6273,7 +6643,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             expr: vir_expr!{ [slice_len_call] == [sequence_types.len(self.encoder, rhs_expr.clone())] }
         }));
 
-        let elem_snap_ty = self.encoder.encode_snapshot_type(sequence_types.elem_ty_rs).with_span(span)?;
+        let elem_snap_ty = self
+            .encoder
+            .encode_snapshot_type(sequence_types.elem_ty_rs)
+            .with_span(span)?;
 
         let i: vir::Expr = vir_local! { i: Int }.into();
 
@@ -6284,20 +6657,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             elem_snap_ty.clone(),
         );
 
-        let slice_lookup_call = slice_types.encode_lookup_pure_call(
-            self.encoder,
-            slice_expr,
-            i.clone(),
-            elem_snap_ty,
-        );
+        let slice_lookup_call =
+            slice_types.encode_lookup_pure_call(self.encoder, slice_expr, i.clone(), elem_snap_ty);
 
         let indices = vir_expr! { ([vir::Expr::from(0usize)] <= [i]) && ([i] < [sequence_types.len(self.encoder, rhs_expr)]) };
 
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: vir_expr! {
-                forall i: Int ::
-                { [array_lookup_call] } { [slice_lookup_call] } ::
-                ([indices] ==> ([array_lookup_call] == [slice_lookup_call])) }
+            forall i: Int ::
+            { [array_lookup_call] } { [slice_lookup_call] } ::
+            ([indices] ==> ([array_lookup_call] == [slice_lookup_call])) },
         }));
 
         // Store a label for permissions got back from the call
@@ -6323,18 +6692,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             dst_ty,
         );
         let span = self.mir_encoder.get_span_of_location(location);
-        let (encoded_place, mut stmts, place_ty, ..) = self.encode_place(
-            place,
-            ArrayAccessKind::Mutable(None, location),
-            location
-        )?;
+        let (encoded_place, mut stmts, place_ty, ..) =
+            self.encode_place(place, ArrayAccessKind::Mutable(None, location), location)?;
         match place_ty.kind() {
-            ty::TyKind::Array(..) |
-            ty::TyKind::Slice(..) => {
-                let slice_types = self.encoder.encode_sequence_types(place_ty)
-                        .with_span(span)?;
+            ty::TyKind::Array(..) | ty::TyKind::Slice(..) => {
+                let slice_types = self
+                    .encoder
+                    .encode_sequence_types(place_ty)
+                    .with_span(span)?;
 
-                stmts.push(vir::Stmt::Assert( vir::Assert {
+                stmts.push(vir::Stmt::Assert(vir::Assert {
                     expr: vir::Expr::predicate_access_predicate(
                         slice_types.sequence_pred_type.clone(),
                         encoded_place.clone(),
@@ -6345,19 +6712,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
                 let rhs = slice_types.len(self.encoder, encoded_place);
 
-                stmts.extend(
-                    self.encode_copy_value_assign(
-                        encoded_lhs,
-                        rhs,
-                        dst_ty,
-                        location,
-                    )?
-                );
-            },
-            other => return Err(
-                EncodingError::unsupported(format!("length operation on unsupported type '{other:?}'"))
-                    .with_span(span)
-            ),
+                stmts.extend(self.encode_copy_value_assign(encoded_lhs, rhs, dst_ty, location)?);
+            }
+            other => {
+                return Err(EncodingError::unsupported(format!(
+                    "length operation on unsupported type '{other:?}'"
+                ))
+                .with_span(span))
+            }
         }
 
         Ok(stmts)
@@ -6374,11 +6736,21 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let span = self.mir_encoder.get_span_of_location(location);
         let sequence_types = self.encoder.encode_sequence_types(ty).with_span(span)?;
 
-        let encoded_operand = self.mir_encoder.encode_operand_expr(operand)
+        let encoded_operand = self
+            .mir_encoder
+            .encode_operand_expr(operand)
             .with_span(span)?;
-        let len: usize = self.encoder.const_eval_intlike(mir::ConstantKind::Ty(times)).with_span(span)?
-            .to_u64().unwrap().try_into().unwrap();
-        let lookup_ret_ty = self.encoder.encode_snapshot_type(sequence_types.elem_ty_rs)
+        let len: usize = self
+            .encoder
+            .const_eval_intlike(mir::ConstantKind::Ty(times))
+            .with_span(span)?
+            .to_u64()
+            .unwrap()
+            .try_into()
+            .unwrap();
+        let lookup_ret_ty = self
+            .encoder
+            .encode_snapshot_type(sequence_types.elem_ty_rs)
             .with_span(span)?;
 
         let inhaled_operand = if lookup_ret_ty.is_domain() || lookup_ret_ty.is_snapshot() {
@@ -6387,20 +6759,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             encoded_operand
         };
 
-        let mut stmts = self.encode_havoc_and_initialization(&encoded_lhs).with_span(span)?;
+        let mut stmts = self
+            .encode_havoc_and_initialization(&encoded_lhs)
+            .with_span(span)?;
         let idx: vir::Expr = vir_local! { i: Int }.into();
-        let indices = vir_expr! { ([vir::Expr::from(0usize)] <= [idx]) && ([idx] < [vir::Expr::from(len)]) };
-        let lookup_pure_call = sequence_types.encode_lookup_pure_call(
-            self.encoder,
-            encoded_lhs,
-            idx,
-            lookup_ret_ty,
-        );
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
+        let indices =
+            vir_expr! { ([vir::Expr::from(0usize)] <= [idx]) && ([idx] < [vir::Expr::from(len)]) };
+        let lookup_pure_call =
+            sequence_types.encode_lookup_pure_call(self.encoder, encoded_lhs, idx, lookup_ret_ty);
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
             expr: vir_expr! {
-                forall i: Int ::
-                { [lookup_pure_call] } ::
-                ([indices] ==> ([lookup_pure_call] == [inhaled_operand])) }
+            forall i: Int ::
+            { [lookup_pure_call] } ::
+            ([indices] ==> ([lookup_pure_call] == [inhaled_operand])) },
         }));
 
         Ok(stmts)
@@ -6423,8 +6794,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let havoc_ref_method_name = self
             .encoder
             .encode_builtin_method_use(BuiltinMethodKind::HavocRef)?;
-        if let vir::Expr::Local( vir::Local {variable: ref dst_local_var, ..} ) = dst {
-            Ok(vec![vir::Stmt::MethodCall( vir::MethodCall {
+        if let vir::Expr::Local(vir::Local {
+            variable: ref dst_local_var,
+            ..
+        }) = dst
+        {
+            Ok(vec![vir::Stmt::MethodCall(vir::MethodCall {
                 method_name: havoc_ref_method_name,
                 arguments: vec![],
                 targets: vec![dst_local_var.clone()],
@@ -6432,12 +6807,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         } else {
             let tmp_var = self.get_auxiliary_local_var("havoc", dst.get_type().clone());
             Ok(vec![
-                vir::Stmt::MethodCall( vir::MethodCall {
+                vir::Stmt::MethodCall(vir::MethodCall {
                     method_name: havoc_ref_method_name,
                     arguments: vec![],
                     targets: vec![tmp_var.clone()],
                 }),
-                vir::Stmt::Assign( vir::Assign {
+                vir::Stmt::Assign(vir::Assign {
                     target: dst.clone(),
                     source: tmp_var.into(),
                     kind: vir::AssignKind::Move,
@@ -6447,17 +6822,21 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     }
 
     /// Havoc and assume permission on fields
-    fn encode_havoc_and_initialization(&mut self, dst: &vir::Expr) -> EncodingResult<Vec<vir::Stmt>> {
+    fn encode_havoc_and_initialization(
+        &mut self,
+        dst: &vir::Expr,
+    ) -> EncodingResult<Vec<vir::Stmt>> {
         debug!("Encode havoc and allocation {:?}", dst);
 
         let mut stmts = vec![];
         // Havoc `dst`
         stmts.extend(self.encode_havoc(dst)?);
         // Initialize `dst`
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
-            expr: self.mir_encoder
-                    .encode_place_predicate_permission(dst.clone(), vir::PermAmount::Write)
-                    .unwrap(),
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
+            expr: self
+                .mir_encoder
+                .encode_place_predicate_permission(dst.clone(), vir::PermAmount::Write)
+                .unwrap(),
         }));
         Ok(stmts)
     }
@@ -6471,7 +6850,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         field: vir::Field,
         location: mir::Location,
         vir_assign_kind: vir::AssignKind,
-        can_copy_reference: bool // reference copies are allowed if the field is a constant
+        can_copy_reference: bool, // reference copies are allowed if the field is a constant
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         trace!(
             "[enter] prepare_assign_target(dst={}, field={}, location={:?})",
@@ -6484,9 +6863,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             let mut alloc_stmts = self.encode_havoc(&dst).with_span(span)?;
             let dst_field = dst.clone().field(field.clone());
             let acc = vir::Expr::acc_permission(dst_field.clone(), vir::PermAmount::Write);
-            alloc_stmts.push(vir::Stmt::Inhale( vir::Inhale {
-                expr: acc,
-            }));
+            alloc_stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: acc }));
             match vir_assign_kind {
                 vir::AssignKind::Copy => {
                     if field.typ.is_typed_ref_or_type_var() {
@@ -6494,11 +6871,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             let pred_acc = vir::Expr::predicate_access_predicate(
                                 field.typ,
                                 dst_field,
-                                vir::PermAmount::Read
+                                vir::PermAmount::Read,
                             );
-                            alloc_stmts.push(vir::Stmt::Inhale(
-                                vir::Inhale { expr: pred_acc }
-                            ));
+                            alloc_stmts.push(vir::Stmt::Inhale(vir::Inhale { expr: pred_acc }));
                         } else {
                             // TODO: Inhale the predicate rooted at dst_field
                             return Err(SpannedEncodingError::unsupported(
@@ -6534,9 +6909,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             field.clone(),
             location,
             vir::AssignKind::Copy,
-            false
+            false,
         )?;
-        stmts.push(vir::Stmt::Assign( vir::Assign {
+        stmts.push(vir::Stmt::Assign(vir::Assign {
             target: lhs.field(field),
             source: rhs,
             kind: vir::AssignKind::Copy,
@@ -6555,12 +6930,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         let span = self.mir_encoder.get_span_of_location(location);
         let field = self.encoder.encode_value_field(ty).with_span(span)?;
-        self.encode_copy_value_assign2(
-            dst,
-            src.field(field.clone()),
-            field,
-            location
-        )
+        self.encode_copy_value_assign2(dst, src.field(field.clone()), field, location)
     }
 
     /// Copy a value by inhaling snapshot equality.
@@ -6570,11 +6940,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         dst: vir::Expr,
     ) -> EncodingResult<Vec<vir::Stmt>> {
         let mut stmts = self.encode_havoc_and_initialization(&dst)?;
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
-            expr: vir::Expr::eq_cmp(
-                vir::Expr::snap_app(src),
-                vir::Expr::snap_app(dst),
-            ),
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
+            expr: vir::Expr::eq_cmp(vir::Expr::snap_app(src), vir::Expr::snap_app(dst)),
         }));
         Ok(stmts)
     }
@@ -6592,9 +6959,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             | ty::TyKind::Int(_)
             | ty::TyKind::Uint(_)
             | ty::TyKind::Float(_)
-            | ty::TyKind::Char => {
-                self.encode_copy_primitive_value(src, dst, self_ty, location)?
-            }
+            | ty::TyKind::Char => self.encode_copy_primitive_value(src, dst, self_ty, location)?,
 
             ty::TyKind::Adt(_, _)
             | ty::TyKind::Closure(_, _)
@@ -6606,8 +6971,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
             _ => {
                 return Err(SpannedEncodingError::unsupported(
-                    format!("copy operation for an unsupported type {:?}", self_ty.kind()),
-                    span
+                    format!(
+                        "copy operation for an unsupported type {:?}",
+                        self_ty.kind()
+                    ),
+                    span,
                 ));
             }
         };
@@ -6660,7 +7028,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 if adt_def.is_union() {
                     return Err(SpannedEncodingError::unsupported(
                         "unions are not supported",
-                        span
+                        span,
                     ));
                 }
                 let num_variants = adt_def.variants().len();
@@ -6671,10 +7039,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     // Handle *signed* discriminats
                     let discr_type = adt_def.repr().discr_type();
                     let discr_value: vir::Expr = if discr_type.is_signed() {
-                        let bit_size =
-                            Integer::from_attr(&tcx, discr_type)
-                                .size()
-                                .bits();
+                        let bit_size = Integer::from_attr(&tcx, discr_type).size().bits();
                         let shift = 128 - bit_size;
                         let unsigned_discr =
                             adt_def.discriminant_for_variant(tcx, variant_index).val;
@@ -6691,20 +7056,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     let discriminant = self
                         .encoder
                         .encode_discriminant_func_app(dst.clone(), adt_def)?;
-                    stmts.push(vir::Stmt::Inhale( vir::Inhale {
+                    stmts.push(vir::Stmt::Inhale(vir::Inhale {
                         expr: vir::Expr::eq_cmp(discriminant, discr_value),
                     }));
 
                     let variant_name = variant_def.ident(tcx).to_string();
                     let new_dst_base = dst_base.variant(&variant_name);
-                    let variant_field = if let vir::Expr::Variant( vir::Variant {variant_index: ref field, ..}) = new_dst_base {
+                    let variant_field = if let vir::Expr::Variant(vir::Variant {
+                        variant_index: ref field,
+                        ..
+                    }) = new_dst_base
+                    {
                         field.clone()
                     } else {
                         unreachable!()
                     };
 
                     if !variant_def.fields.is_empty() {
-                        stmts.push(vir::Stmt::Downcast( vir::Downcast {
+                        stmts.push(vir::Stmt::Downcast(vir::Downcast {
                             base: dst.clone(),
                             field: variant_field,
                         }));
@@ -6716,7 +7085,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     let operand = &operands[field_index];
                     let field_name = field.ident(tcx).to_string();
                     let field_ty = field.ty(tcx, subst);
-                    let encoded_field = self.encoder
+                    let encoded_field = self
+                        .encoder
                         .encode_struct_field(&field_name, field_ty)
                         .with_span(span)?;
                     stmts.extend(self.encode_assign_operand(
@@ -6729,12 +7099,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
             mir::AggregateKind::Closure(def_id, substs) => {
                 // TODO: might need to assert history invariants?
-                assert!(!self.encoder.is_spec_closure(def_id.to_def_id()), "spec closure: {def_id:?}");
+                assert!(
+                    !self.encoder.is_spec_closure(def_id.to_def_id()),
+                    "spec closure: {def_id:?}"
+                );
                 let cl_substs = substs.as_closure();
                 for (field_index, field_ty) in cl_substs.upvar_tys().enumerate() {
                     let operand = &operands[field_index];
                     let field_name = format!("closure_{field_index}");
-                    let encoded_field = self.encoder
+                    let encoded_field = self
+                        .encoder
                         .encode_raw_ref_field(field_name, field_ty)
                         .with_span(span)?;
                     stmts.extend(self.encode_assign_operand(
@@ -6747,14 +7121,22 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
             mir::AggregateKind::Array(..) => {
                 let sequence_types = self.encoder.encode_sequence_types(ty).with_span(span)?;
-                let lookup_ret_ty = self.encoder.encode_snapshot_type(sequence_types.elem_ty_rs)
+                let lookup_ret_ty = self
+                    .encoder
+                    .encode_snapshot_type(sequence_types.elem_ty_rs)
                     .with_span(span)?;
 
                 for (idx, operand) in operands.iter().enumerate() {
-                    let lookup_pure_call = sequence_types
-                        .encode_lookup_pure_call(self.encoder, dst.clone(), idx.into(), lookup_ret_ty.clone());
+                    let lookup_pure_call = sequence_types.encode_lookup_pure_call(
+                        self.encoder,
+                        dst.clone(),
+                        idx.into(),
+                        lookup_ret_ty.clone(),
+                    );
 
-                    let encoded_operand = self.mir_encoder.encode_operand_expr(operand)
+                    let encoded_operand = self
+                        .mir_encoder
+                        .encode_operand_expr(operand)
                         .with_span(span)?;
 
                     stmts.push(
@@ -6768,7 +7150,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             mir::AggregateKind::Generator(..) => {
                 return Err(SpannedEncodingError::unsupported(
                     "construction of generators is not supported",
-                    span
+                    span,
                 ));
             }
         }
@@ -6786,7 +7168,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         Ok(())
     }
 
-    fn get_label_after_location(&mut self, location: mir::Location) -> SpannedEncodingResult<Option<&String>> {
+    fn get_label_after_location(
+        &mut self,
+        location: mir::Location,
+    ) -> SpannedEncodingResult<Option<&String>> {
         let opt_label = self.label_after_location.get(&location);
         if opt_label.is_none() {
             if config::allow_unreachable_unsupported_code() {
@@ -6824,9 +7209,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         location: mir::Location,
     ) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Stmt>, ty::Ty<'tcx>, Option<usize>)> {
         let span = self.mir_encoder.get_span_of_location(location);
-        let (encoded_place, ty, variant_idx) = self.mir_encoder.encode_place(place).with_span(span)?;
+        let (encoded_place, ty, variant_idx) =
+            self.mir_encoder.encode_place(place).with_span(span)?;
         trace!("encode_place(ty={:?})", ty);
-        let (encoded_expr, encoding_stmts) = self.postprocess_place_encoding(encoded_place, encode_kind).with_span(span)?;
+        let (encoded_expr, encoding_stmts) = self
+            .postprocess_place_encoding(encoded_place, encode_kind)
+            .with_span(span)?;
 
         Ok((encoded_expr, encoding_stmts, ty, variant_idx))
     }
@@ -6839,13 +7227,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> EncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
         let sequence_types = self.encoder.encode_sequence_types(sequence_ty)?;
 
-        let lookup_res: vir::Expr = self.cfg_method.add_fresh_local_var(sequence_types.elem_pred_type.clone()).into();
-        let lookup_res_val_field = self.encoder.encode_value_expr(lookup_res.clone(), sequence_types.elem_ty_rs)?;
-        let snap_lookup_res_val_field = self.encoder.patch_snapshots(vir::Expr::snap_app(lookup_res_val_field))?;
+        let lookup_res: vir::Expr = self
+            .cfg_method
+            .add_fresh_local_var(sequence_types.elem_pred_type.clone())
+            .into();
+        let lookup_res_val_field = self
+            .encoder
+            .encode_value_expr(lookup_res.clone(), sequence_types.elem_ty_rs)?;
+        let snap_lookup_res_val_field = self
+            .encoder
+            .patch_snapshots(vir::Expr::snap_app(lookup_res_val_field))?;
 
-        let lookup_ret_ty = self.encoder.encode_snapshot_type(sequence_types.elem_ty_rs)?;
+        let lookup_ret_ty = self
+            .encoder
+            .encode_snapshot_type(sequence_types.elem_ty_rs)?;
 
-        let (encoded_base_expr, mut stmts) = self.postprocess_place_encoding(base, ArrayAccessKind::Shared)?;
+        let (encoded_base_expr, mut stmts) =
+            self.postprocess_place_encoding(base, ArrayAccessKind::Shared)?;
         stmts.extend(self.encode_havoc_and_initialization(&lookup_res)?);
 
         let idx_val_int = self.encoder.patch_snapshots(vir::Expr::snap_app(index))?;
@@ -6857,13 +7255,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             lookup_ret_ty,
         );
 
-        stmts.push(vir::Stmt::Assert( vir::Assert {
-            expr: vir::Expr::predicate_access_predicate(sequence_types.sequence_pred_type, encoded_base_expr, vir::PermAmount::Read),
+        stmts.push(vir::Stmt::Assert(vir::Assert {
+            expr: vir::Expr::predicate_access_predicate(
+                sequence_types.sequence_pred_type,
+                encoded_base_expr,
+                vir::PermAmount::Read,
+            ),
             position: vir::Position::default(),
         }));
 
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
-            expr: vir_expr!{ [ lookup_pure_call ] == [ snap_lookup_res_val_field ] }
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
+            expr: vir_expr! { [ lookup_pure_call ] == [ snap_lookup_res_val_field ] },
         }));
         Ok((lookup_res, stmts))
     }
@@ -6878,11 +7280,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
     ) -> EncodingResult<(vir::Expr, Vec<vir::Stmt>)> {
         let sequence_types = self.encoder.encode_sequence_types(sequence_ty)?;
 
-        let res: vir::Expr = self.cfg_method.add_fresh_local_var(sequence_types.elem_pred_type.clone()).into();
-        let res_val_field = self.encoder.encode_value_expr(res.clone(), sequence_types.elem_ty_rs)?;
-        let snap_res_val_field = self.encoder.patch_snapshots(vir::Expr::snap_app(res_val_field.clone()))?;
+        let res: vir::Expr = self
+            .cfg_method
+            .add_fresh_local_var(sequence_types.elem_pred_type.clone())
+            .into();
+        let res_val_field = self
+            .encoder
+            .encode_value_expr(res.clone(), sequence_types.elem_ty_rs)?;
+        let snap_res_val_field = self
+            .encoder
+            .patch_snapshots(vir::Expr::snap_app(res_val_field.clone()))?;
 
-        let (encoded_base_expr, mut stmts) = self.postprocess_place_encoding(base, ArrayAccessKind::Mutable(None, location))?;
+        let (encoded_base_expr, mut stmts) =
+            self.postprocess_place_encoding(base, ArrayAccessKind::Mutable(None, location))?;
 
         let idx_val_int = self.encoder.patch_snapshots(vir::Expr::snap_app(index))?;
 
@@ -6900,26 +7310,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         }));
 
         // exhale Array$4$i32(self)
-        let array_access_pred = vir::Expr::pred_permission(
-            encoded_base_expr.clone(),
-            vir::PermAmount::Write,
-        ).unwrap();
+        let array_access_pred =
+            vir::Expr::pred_permission(encoded_base_expr.clone(), vir::PermAmount::Write).unwrap();
 
-        stmts.push(vir_stmt!{ exhale [array_access_pred] });
+        stmts.push(vir_stmt! { exhale [array_access_pred] });
 
-        let old = |e| { vir::Expr::labelled_old(&before_label, e) };
-        let old_lhs = |e| { vir::Expr::labelled_old("lhs", e) };
+        let old = |e| vir::Expr::labelled_old(&before_label, e);
+        let old_lhs = |e| vir::Expr::labelled_old("lhs", e);
 
         // value of res
-        let lookup_ret_ty = self.encoder.encode_snapshot_type(sequence_types.elem_ty_rs)?;
+        let lookup_ret_ty = self
+            .encoder
+            .encode_snapshot_type(sequence_types.elem_ty_rs)?;
         let lookup_pure_call = sequence_types.encode_lookup_pure_call(
             self.encoder,
             encoded_base_expr.clone(),
             idx_val_int.clone(),
             lookup_ret_ty.clone(),
         );
-        stmts.push(vir::Stmt::Inhale( vir::Inhale {
-            expr: vir_expr!{ [ old(lookup_pure_call) ] == [ snap_res_val_field ] }
+        stmts.push(vir::Stmt::Inhale(vir::Inhale {
+            expr: vir_expr! { [ old(lookup_pure_call) ] == [ snap_res_val_field ] },
         }));
 
         // inhale magic wand
@@ -6936,21 +7346,22 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         // NEEDSWORK: the vir! macro can't do everything we want here..
         // TODO: de-duplicate with encode_array_direct_assign
-        let i_var: vir::Expr = vir_local!{ i: Int }.into();
+        let i_var: vir::Expr = vir_local! { i: Int }.into();
 
-        let zero_le_i = vir_expr!{ [ vir::Expr::from(0) ] <= [ i_var ] };
-        let i_lt_len = vir_expr!{ [ i_var ] < [ sequence_types.len(self.encoder, encoded_base_expr.clone()) ] };
-        let i_ne_idx = vir_expr!{ [ i_var ] != [ old(idx_val_int.clone()) ] };
-        let idx_conditions = vir_expr!{ [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
+        let zero_le_i = vir_expr! { [ vir::Expr::from(0) ] <= [ i_var ] };
+        let i_lt_len = vir_expr! { [ i_var ] < [ sequence_types.len(self.encoder, encoded_base_expr.clone()) ] };
+        let i_ne_idx = vir_expr! { [ i_var ] != [ old(idx_val_int.clone()) ] };
+        let idx_conditions = vir_expr! { [zero_le_i] && ([i_lt_len] && [i_ne_idx]) };
         let lookup_array_i = sequence_types.encode_lookup_pure_call(
             self.encoder,
             encoded_base_expr.clone(),
             i_var,
             lookup_ret_ty.clone(),
         );
-        let lookup_same_as_old = vir_expr!{ [lookup_array_i] == [old(lookup_array_i.clone())] };
-        let forall_body = vir_expr!{ [idx_conditions] ==> [lookup_same_as_old] };
-        let all_others_unchanged = vir_expr!{ forall i: Int :: { [lookup_array_i] } :: [ forall_body ] };
+        let lookup_same_as_old = vir_expr! { [lookup_array_i] == [old(lookup_array_i.clone())] };
+        let forall_body = vir_expr! { [idx_conditions] ==> [lookup_same_as_old] };
+        let all_others_unchanged =
+            vir_expr! { forall i: Int :: { [lookup_array_i] } :: [ forall_body ] };
         let indexed_lookup_pure = sequence_types.encode_lookup_pure_call(
             self.encoder,
             encoded_base_expr.clone(),
@@ -6958,14 +7369,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             lookup_ret_ty,
         );
         // TODO: old inside snapshot or the other way around?
-        let snap_old_res_val_field = self.encoder.patch_snapshots(vir::Expr::snap_app(res_val_field.clone()))?;
-        let indexed_updated = vir_expr!{ [ indexed_lookup_pure ] == [ old_lhs(snap_old_res_val_field) ] };
+        let snap_old_res_val_field = self
+            .encoder
+            .patch_snapshots(vir::Expr::snap_app(res_val_field.clone()))?;
+        let indexed_updated =
+            vir_expr! { [ indexed_lookup_pure ] == [ old_lhs(snap_old_res_val_field) ] };
 
-        let magic_wand_rhs = vir_expr!{ [all_others_unchanged] && [indexed_updated] };
-        self.array_magic_wand_at.insert(
-            location,
-            (res_val_field, encoded_base_expr, magic_wand_rhs)
-        );
+        let magic_wand_rhs = vir_expr! { [all_others_unchanged] && [indexed_updated] };
+        self.array_magic_wand_at
+            .insert(location, (res_val_field, encoded_base_expr, magic_wand_rhs));
 
         Ok((res, stmts))
     }
@@ -6982,8 +7394,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 let (expr, stmts) = self.postprocess_place_encoding(base, array_encode_kind)?;
                 (expr.field(field), stmts)
             }
-            PlaceEncoding::SliceAccess { base, index, rust_slice_ty: rust_ty, .. } |
-            PlaceEncoding::ArrayAccess { base, index, rust_array_ty: rust_ty, .. } => {
+            PlaceEncoding::SliceAccess {
+                base,
+                index,
+                rust_slice_ty: rust_ty,
+                ..
+            }
+            | PlaceEncoding::ArrayAccess {
+                base,
+                index,
+                rust_array_ty: rust_ty,
+                ..
+            } => {
                 if let ArrayAccessKind::Mutable(loan, location) = array_encode_kind {
                     self.encode_sequence_lookup_mut(*base, index, rust_ty, loan, location)?
                 } else {
@@ -6992,17 +7414,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
             PlaceEncoding::Variant { box base, field } => {
                 let (expr, stmts) = self.postprocess_place_encoding(base, array_encode_kind)?;
-                (vir::Expr::Variant( vir::Variant {
-                    base: box expr,
-                    variant_index: field,
-                    position: vir::Position::default(),
-                }),
-                stmts)
+                (
+                    vir::Expr::Variant(vir::Variant {
+                        base: box expr,
+                        variant_index: field,
+                        position: vir::Position::default(),
+                    }),
+                    stmts,
+                )
             }
         })
     }
 
-    pub fn register_error<T: Into<MultiSpan>>(&self, span: T, error_ctxt: ErrorCtxt) -> vir::Position {
+    pub fn register_error<T: Into<MultiSpan>>(
+        &self,
+        span: T,
+        error_ctxt: ErrorCtxt,
+    ) -> vir::Position {
         self.mir_encoder.register_error(span, error_ctxt)
     }
 }
@@ -7022,17 +7450,19 @@ fn convert_loans_to_borrows(loans: &[facts::Loan]) -> Vec<Borrow> {
 /// len: Length of borrow_infos
 fn assert_one_magic_wand(len: usize) -> EncodingResult<()> {
     if len > 1 {
-        Err(EncodingError::internal(
-            format!("We can have at most one magic wand in the postcondition. But we have {len:?}")
-        ))
-    } else { Ok(()) }
+        Err(EncodingError::internal(format!(
+            "We can have at most one magic wand in the postcondition. But we have {len:?}"
+        )))
+    } else {
+        Ok(())
+    }
 }
 
 // Checks if a type is a reference to a string, or a reference to a reference to a string, etc.
 fn is_str(ty: ty::Ty<'_>) -> bool {
     match ty.kind() {
         ty::TyKind::Ref(_, inner, _) => inner.is_str() || is_str(*inner),
-        _ => false
+        _ => false,
     }
 }