diff --git a/docs/src/getting-started/verification-results/src/main.rs b/docs/src/getting-started/verification-results/src/main.rs
index 72653cf4dc8f..7a03b34f0f9e 100644
--- a/docs/src/getting-started/verification-results/src/main.rs
+++ b/docs/src/getting-started/verification-results/src/main.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
-#[kani::unwind(4)]
 // ANCHOR: success_example
 fn success_example() {
     let mut sum = 0;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index 7f19e5814ce0..b210b2c9333e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -8,27 +8,23 @@ use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::mir::Local;
+use stable_mir::mir::{Local, VarDebugInfoContents};
+use stable_mir::ty::{FnDef, RigidTy, TyKind};
 use stable_mir::CrateDef;
-use tracing::debug;
-
-use stable_mir::ty::{RigidTy, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
     /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
     /// for which it needs to be enforced.
     ///
-    /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance
-    ///    of it. Panics if there are more or less than one instance.
-    /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function,
-    ///    turns it into a CBMC contract and attaches it to the symbol for the previously resolved
-    ///    instance.
+    /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one
+    ///    instance of it. Panics if there are more or less than one instance.
+    /// 2. The additional arguments for the inner checks are locations that may be modified.
+    ///    Add them to the list of CBMC's assigns.
     /// 3. Returns the mangled name of the symbol it attached the contract to.
-    /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract`
-    ///    which has `static mut REENTRY : bool` declared inside.
-    /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is
-    ///    comprised of the file path that `checked_with` is located in, the name of the
+    /// 4. Returns the full path to the static marked with `#[kanitool::recursion_tracker]` which
+    ///    is passed to the `--nondet-static-exclude` argument.
+    ///    This flag expects the file path that `checked_with` is located in, the name of the
     ///    `checked_with` function and the name of the constant (`REENTRY`).
     pub fn handle_check_contract(
         &mut self,
@@ -36,86 +32,101 @@ impl<'tcx> GotocCtx<'tcx> {
         items: &[MonoItem],
     ) -> AssignsContract {
         let tcx = self.tcx;
-        let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract);
+        let modify = items
+            .iter()
+            .find_map(|item| {
+                // Find the instance under contract
+                let MonoItem::Fn(instance) = *item else { return None };
+                if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract {
+                    self.find_modifies(instance)
+                } else {
+                    None
+                }
+            })
+            .unwrap();
+        self.attach_modifies_contract(modify);
+        let recursion_tracker = self.find_recursion_tracker(items);
+        AssignsContract { recursion_tracker, contracted_function_name: modify.mangled_name() }
+    }
 
-        let recursion_wrapper_id =
-            function_under_contract_attrs.checked_with_id().unwrap().unwrap();
-        let expected_name = format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id));
-        let mut recursion_tracker = items.iter().filter_map(|i| match i {
-            MonoItem::Static(recursion_tracker)
-                if (*recursion_tracker).name().contains(expected_name.as_str()) =>
+    /// The name and location for the recursion tracker should match the exact information added
+    /// to the symbol table, otherwise our contract instrumentation will silently failed.
+    /// This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly
+    /// handle this tracker. CBMC silently fails if there is no match in the symbol table
+    /// that correspond to the argument of this flag.
+    /// More details at https://github.com/model-checking/kani/pull/3045.
+    ///
+    /// We must use the pretty name of the tracker instead of the mangled name.
+    /// This restriction comes from `--nondet-static-exclude` in CBMC.
+    /// Mode details at https://github.com/diffblue/cbmc/issues/8225.
+    fn find_recursion_tracker(&mut self, items: &[MonoItem]) -> Option<String> {
+        // Return item tagged with `#[kanitool::recursion_tracker]`
+        let mut recursion_trackers = items.iter().filter_map(|item| {
+            let MonoItem::Static(static_item) = item else { return None };
+            if !static_item
+                .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()])
+                .is_empty()
             {
-                Some(*recursion_tracker)
+                let span = static_item.span();
+                let loc = self.codegen_span_stable(span);
+                Some(format!(
+                    "{}:{}",
+                    loc.filename().expect("recursion location wrapper should have a file name"),
+                    static_item.name(),
+                ))
+            } else {
+                None
             }
-            _ => None,
         });
 
-        let recursion_tracker_def = recursion_tracker
-            .next()
-            .expect("There should be at least one recursion tracker (REENTRY) in scope");
+        let recursion_tracker = recursion_trackers.next();
         assert!(
-            recursion_tracker.next().is_none(),
-            "Only one recursion tracker (REENTRY) may be in scope"
+            recursion_trackers.next().is_none(),
+            "Expected up to one recursion tracker (`REENTRY`) in scope"
         );
+        recursion_tracker
+    }
 
-        let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id);
-        let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper);
-        // The name and location for the recursion tracker should match the exact information added
-        // to the symbol table, otherwise our contract instrumentation will silently failed.
-        // This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly
-        // handle this tracker. CBMC silently fails if there is no match in the symbol table
-        // that correspond to the argument of this flag.
-        // More details at https://github.com/model-checking/kani/pull/3045.
-        let full_recursion_tracker_name = format!(
-            "{}:{}",
-            location_of_recursion_wrapper
-                .filename()
-                .expect("recursion location wrapper should have a file name"),
-            // We must use the pretty name of the tracker instead of the mangled name.
-            // This restrictions comes from `--nondet-static-exclude` in CBMC.
-            // Mode details at https://github.com/diffblue/cbmc/issues/8225.
-            recursion_tracker_def.name(),
-        );
-
-        let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap();
-        let mut instance_under_contract = items.iter().filter_map(|i| match i {
-            MonoItem::Fn(instance @ Instance { def, .. })
-                if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) =>
-            {
-                Some(*instance)
-            }
-            _ => None,
-        });
-        let instance_of_check = instance_under_contract.next().unwrap();
-        assert!(
-            instance_under_contract.next().is_none(),
-            "Only one instance of a checked function may be in scope"
-        );
-        let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn);
-        let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| {
-            debug!(?instance_of_check, "had no assigns contract specified");
-            vec![]
-        });
-        self.attach_modifies_contract(instance_of_check, assigns_contract);
-        let wrapper_name = instance_of_check.mangled_name();
-
-        AssignsContract {
-            recursion_tracker: full_recursion_tracker_name,
-            contracted_function_name: wrapper_name,
-        }
+    /// Find the modifies recursively since we may have a recursion wrapper.
+    /// I.e.: [recursion_wrapper ->]? check -> modifies.
+    fn find_modifies(&mut self, instance: Instance) -> Option<Instance> {
+        let contract_attrs =
+            KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?;
+        let mut find_closure = |inside: Instance, name: &str| {
+            let body = self.transformer.body(self.tcx, inside);
+            body.var_debug_info.iter().find_map(|var_info| {
+                if var_info.name.as_str() == name {
+                    let ty = match &var_info.value {
+                        VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
+                        VarDebugInfoContents::Const(const_op) => const_op.ty(),
+                    };
+                    if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() {
+                        return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap());
+                    }
+                }
+                None
+            })
+        };
+        let check_instance = if contract_attrs.has_recursion {
+            let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?;
+            find_closure(recursion_check, contract_attrs.checked_with.as_str())?
+        } else {
+            find_closure(instance, contract_attrs.checked_with.as_str())?
+        };
+        find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
     }
 
     /// Convert the Kani level contract into a CBMC level contract by creating a
     /// CBMC lambda.
     fn codegen_modifies_contract(
         &mut self,
-        modified_places: Vec<Local>,
+        goto_annotated_fn_name: &str,
+        modifies: Instance,
         loc: Location,
     ) -> FunctionContract {
-        let goto_annotated_fn_name = self.current_fn().name();
         let goto_annotated_fn_typ = self
             .symbol_table
-            .lookup(&goto_annotated_fn_name)
+            .lookup(goto_annotated_fn_name)
             .unwrap_or_else(|| panic!("Function '{goto_annotated_fn_name}' is not declared"))
             .typ
             .clone();
@@ -141,13 +152,24 @@ impl<'tcx> GotocCtx<'tcx> {
             })
             .unwrap_or_default();
 
-        let assigns = modified_places
+        // The last argument is a tuple with addresses that can be modified.
+        let modifies_local = Local::from(modifies.fn_abi().unwrap().args.len());
+        let modifies_ty = self.local_ty_stable(modifies_local);
+        let modifies_args =
+            self.codegen_place_stable(&modifies_local.into(), loc).unwrap().goto_expr;
+        let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else {
+            unreachable!("found {:?}", modifies_ty.kind())
+        };
+        let assigns: Vec<_> = modifies_tys
             .into_iter()
-            .map(|local| {
-                if self.is_fat_pointer_stable(self.local_ty_stable(local)) {
-                    let unref = match self.local_ty_stable(local).kind() {
-                        TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => ty,
-                        kind => unreachable!("{:?} is not a reference", kind),
+            .enumerate()
+            .map(|(idx, ty)| {
+                assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
+                let ptr = modifies_args.clone().member(idx.to_string(), &self.symbol_table);
+                if self.is_fat_pointer_stable(ty) {
+                    let unref = match ty.kind() {
+                        TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty,
+                        kind => unreachable!("Expected a raw pointer, but found {:?}", kind),
                     };
                     let size = match unref.kind() {
                         TyKind::RigidTy(RigidTy::Slice(elt_type)) => {
@@ -176,30 +198,17 @@ impl<'tcx> GotocCtx<'tcx> {
                             ),
                         )
                         .call(vec![
-                            self.codegen_place_stable(&local.into(), loc)
-                                .unwrap()
-                                .goto_expr
+                            ptr.clone()
                                 .member("data", &self.symbol_table)
                                 .cast_to(Type::empty().to_pointer()),
-                            self.codegen_place_stable(&local.into(), loc)
-                                .unwrap()
-                                .goto_expr
-                                .member("len", &self.symbol_table)
-                                .mul(Expr::size_constant(
-                                    size.try_into().unwrap(),
-                                    &self.symbol_table,
-                                )),
+                            ptr.member("len", &self.symbol_table).mul(Expr::size_constant(
+                                size.try_into().unwrap(),
+                                &self.symbol_table,
+                            )),
                         ]),
                     )
                 } else {
-                    Lambda::as_contract_for(
-                        &goto_annotated_fn_typ,
-                        None,
-                        self.codegen_place_stable(&local.into(), loc)
-                            .unwrap()
-                            .goto_expr
-                            .dereference(),
-                    )
+                    Lambda::as_contract_for(&goto_annotated_fn_typ, None, ptr.dereference())
                 }
             })
             .chain(shadow_memory_assign)
@@ -212,17 +221,19 @@ impl<'tcx> GotocCtx<'tcx> {
     /// `instance` must have previously been declared.
     ///
     /// This merges with any previously attached contracts.
-    pub fn attach_modifies_contract(&mut self, instance: Instance, modified_places: Vec<Local>) {
+    pub fn attach_modifies_contract(&mut self, instance: Instance) {
         // This should be safe, since the contract is pretty much evaluated as
         // though it was the first (or last) assertion in the function.
         assert!(self.current_fn.is_none());
-        let body = instance.body().unwrap();
+        let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
-        let goto_contract =
-            self.codegen_modifies_contract(modified_places, self.codegen_span_stable(body.span));
-        let name = self.current_fn().name();
-
-        self.symbol_table.attach_contract(name, goto_contract);
-        self.reset_current_fn()
+        let mangled_name = instance.mangled_name();
+        let goto_contract = self.codegen_modifies_contract(
+            &mangled_name,
+            instance,
+            self.codegen_span_stable(instance.def.span()),
+        );
+        self.symbol_table.attach_contract(&mangled_name, goto_contract);
+        self.reset_current_fn();
     }
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 1703335dda51..9baa3c59f4c2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1140,7 +1140,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Mapping enums to CBMC types is rather complicated. There are a few cases to consider:
     /// 1. When there is only 0 or 1 variant, this is straightforward as the code shows
-    /// 2. When there are more variants, rust might decides to apply the typical encoding which
+    /// 2. When there are more variants, rust might decide to apply the typical encoding which
     ///    regard enums as tagged union, or an optimized form, called niche encoding.
     ///
     /// The direct encoding is straightforward. Enums are just mapped to C as a struct of union of structs.
@@ -1242,6 +1242,23 @@ impl<'tcx> GotocCtx<'tcx> {
                                     )
                                 }),
                             ));
+                            // Check if any padding is needed for alignment. This is needed for
+                            // https://github.com/model-checking/kani/issues/2857 for example.
+                            // The logic for determining the maximum variant size is taken from:
+                            // https://github.com/rust-lang/rust/blob/e60ebb2f2c1facba87e7971798f3cbdfd309cd23/compiler/rustc_session/src/code_stats.rs#L166
+                            let max_variant_size = variants
+                                .iter()
+                                .map(|l: &LayoutS<FieldIdx, VariantIdx>| l.size)
+                                .max()
+                                .unwrap();
+                            let max_variant_size = std::cmp::max(max_variant_size, discr_offset);
+                            if let Some(padding) = gcx.codegen_alignment_padding(
+                                max_variant_size,
+                                &layout,
+                                fields.len(),
+                            ) {
+                                fields.push(padding);
+                            }
                             fields
                         })
                     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 986cd00e32a5..0a92e07f4ab4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -264,7 +264,7 @@ impl CodegenBackend for GotocCodegenBackend {
                         for harness in &unit.harnesses {
                             let model_path = units.harness_model_path(*harness).unwrap();
                             let contract_metadata =
-                                contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap();
+                                contract_metadata_for_harness(tcx, harness.def.def_id());
                             let (gcx, items, contract_info) = self.codegen_items(
                                 tcx,
                                 &[MonoItem::Fn(*harness)],
@@ -448,12 +448,9 @@ impl CodegenBackend for GotocCodegenBackend {
     }
 }
 
-fn contract_metadata_for_harness(
-    tcx: TyCtxt,
-    def_id: DefId,
-) -> Result<Option<InternalDefId>, ErrorGuaranteed> {
+fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<InternalDefId> {
     let attrs = KaniAttributes::for_def_id(tcx, def_id);
-    Ok(attrs.interpret_the_for_contract_attribute().transpose()?.map(|(_, id, _)| id))
+    attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
 }
 
 fn check_target(session: &Session) {
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 8c729bbdec9f..f75c0607e1bc 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -6,24 +6,16 @@ use std::collections::BTreeMap;
 
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use rustc_ast::{
-    attr,
-    token::Token,
-    token::TokenKind,
-    tokenstream::{TokenStream, TokenTree},
-    AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind,
+    attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind,
     NestedMetaItem,
 };
 use rustc_errors::ErrorGuaranteed;
-use rustc_hir::{
-    def::DefKind,
-    def_id::{DefId, LocalDefId},
-};
+use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
 use rustc_smir::rustc_internal;
 use rustc_span::{Span, Symbol};
 use stable_mir::mir::mono::Instance as InstanceStable;
-use stable_mir::mir::Local;
 use stable_mir::{CrateDef, DefId as StableDefId};
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
@@ -56,24 +48,27 @@ enum KaniAttributeKind {
     /// name of the function which was generated as the sound stub from the
     /// contract of this function.
     ReplacedWith,
+    /// Attribute on a function with a contract that identifies the code
+    /// implementing the recursive check for the harness.
+    RecursionCheck,
     /// Attribute on a function that was auto-generated from expanding a
     /// function contract.
     IsContractGenerated,
-    /// Identifies a set of pointer arguments that should be added to the write
-    /// set when checking a function contract. Placed on the inner check function.
-    ///
-    /// Emitted by the expansion of a `modifies` function contract clause.
-    Modifies,
-    /// A function used as the inner code of a contract check.
+    /// A function with contract expanded to include the write set as arguments.
     ///
     /// Contains the original body of the contracted function. The signature is
     /// expanded with additional pointer arguments that are not used in the function
     /// but referenced by the `modifies` annotation.
-    InnerCheck,
+    ModifiesWrapper,
     /// Attribute used to mark contracts for functions with recursion.
     /// We use this attribute to properly instantiate `kani::any_modifies` in
     /// cases when recursion is present given our contracts instrumentation.
     Recursion,
+    /// Attribute used to mark the static variable used for tracking recursion check.
+    RecursionTracker,
+    /// Generic marker that can be used to mark functions so this list doesn't have to keep growing.
+    /// This takes a key which is the marker.
+    FnMarker,
     /// Used to mark functions where generating automatic pointer checks should be disabled. This is
     /// used later to automatically attach pragma statements to locations.
     DisableChecks,
@@ -91,11 +86,13 @@ impl KaniAttributeKind {
             | KaniAttributeKind::StubVerified
             | KaniAttributeKind::Unwind => true,
             KaniAttributeKind::Unstable
+            | KaniAttributeKind::FnMarker
             | KaniAttributeKind::Recursion
+            | KaniAttributeKind::RecursionTracker
             | KaniAttributeKind::ReplacedWith
+            | KaniAttributeKind::RecursionCheck
             | KaniAttributeKind::CheckedWith
-            | KaniAttributeKind::Modifies
-            | KaniAttributeKind::InnerCheck
+            | KaniAttributeKind::ModifiesWrapper
             | KaniAttributeKind::IsContractGenerated
             | KaniAttributeKind::DisableChecks => false,
         }
@@ -125,6 +122,21 @@ pub struct KaniAttributes<'tcx> {
     map: BTreeMap<KaniAttributeKind, Vec<&'tcx Attribute>>,
 }
 
+#[derive(Clone, Debug)]
+/// Bundle contract attributes for a function annotated with contracts.
+pub struct ContractAttributes {
+    /// Whether the contract was marked with #[recursion] attribute.
+    pub has_recursion: bool,
+    /// The name of the contract recursion check.
+    pub recursion_check: Symbol,
+    /// The name of the contract check.
+    pub checked_with: Symbol,
+    /// The name of the contract replacement.
+    pub replaced_with: Symbol,
+    /// The name of the inner check used to modify clauses.
+    pub modifies_wrapper: Symbol,
+}
+
 impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         f.debug_struct("KaniAttributes")
@@ -182,22 +194,28 @@ impl<'tcx> KaniAttributes<'tcx> {
     /// returned `Symbol` and `DefId` are respectively the name and id of
     /// `TARGET`. The `Span` is that of the contents of the attribute and used
     /// for error reporting.
-    fn interpret_stub_verified_attribute(
-        &self,
-    ) -> Vec<Result<(Symbol, DefId, Span), ErrorGuaranteed>> {
+    ///
+    /// Any error is emitted and the attribute is filtered out.
+    pub fn interpret_stub_verified_attribute(&self) -> Vec<(Symbol, DefId, Span)> {
         self.map
             .get(&KaniAttributeKind::StubVerified)
             .map_or([].as_slice(), Vec::as_slice)
             .iter()
-            .map(|attr| {
-                let name = expect_key_string_value(self.tcx.sess, attr)?;
-                let ok = self.resolve_sibling(name.as_str()).map_err(|e| {
-                    self.tcx.dcx().span_err(
-                        attr.span,
-                        format!("Failed to resolve replacement function {}: {e}", name.as_str()),
-                    )
-                })?;
-                Ok((name, ok, attr.span))
+            .filter_map(|attr| {
+                let name = expect_key_string_value(self.tcx.sess, attr).ok()?;
+                let def = self
+                    .resolve_from_mod(name.as_str())
+                    .map_err(|e| {
+                        self.tcx.dcx().span_err(
+                            attr.span,
+                            format!(
+                                "Failed to resolve replacement function {}: {e}",
+                                name.as_str()
+                            ),
+                        )
+                    })
+                    .ok()?;
+                Some((name, def, attr.span))
             })
             .collect()
     }
@@ -209,13 +227,14 @@ impl<'tcx> KaniAttributes<'tcx> {
     /// Parse and extract the `proof_for_contract(TARGET)` attribute. The
     /// returned symbol and DefId are respectively the name and id of `TARGET`,
     /// the span in the span for the attribute (contents).
-    pub(crate) fn interpret_the_for_contract_attribute(
-        &self,
-    ) -> Option<Result<(Symbol, DefId, Span), ErrorGuaranteed>> {
-        self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| {
-            let name = expect_key_string_value(self.tcx.sess, target)?;
-            self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err(
-                |resolve_err| {
+    ///
+    /// In the case of an error, this function will emit the error and return `None`.
+    pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> {
+        self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| {
+            let name = expect_key_string_value(self.tcx.sess, target).ok()?;
+            self.resolve_from_mod(name.as_str())
+                .map(|ok| (name, ok, target.span))
+                .map_err(|resolve_err| {
                     self.tcx.dcx().span_err(
                         target.span,
                         format!(
@@ -223,81 +242,62 @@ impl<'tcx> KaniAttributes<'tcx> {
                             name.as_str()
                         ),
                     )
-                },
-            )
+                })
+                .ok()
         })
     }
 
-    /// Extract the name of the sibling function this function's contract is
-    /// checked with (if any).
-    ///
-    /// `None` indicates this function does not use a contract, `Some(Err(_))`
-    /// indicates a contract does exist but an error occurred during resolution.
-    pub fn checked_with(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
-        self.expect_maybe_one(KaniAttributeKind::CheckedWith)
-            .map(|target| expect_key_string_value(self.tcx.sess, target))
-    }
-
     pub fn proof_for_contract(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
         self.expect_maybe_one(KaniAttributeKind::ProofForContract)
             .map(|target| expect_key_string_value(self.tcx.sess, target))
     }
 
-    pub fn inner_check(&self) -> Option<Result<DefId, ErrorGuaranteed>> {
-        self.eval_sibling_attribute(KaniAttributeKind::InnerCheck)
+    /// Extract the name of the local that represents this function's contract is
+    /// checked with (if any).
+    ///
+    /// `None` indicates this function does not use a contract, or an error was found.
+    /// Note that the error will already be emitted, so we don't return an error.
+    pub fn contract_attributes(&self) -> Option<ContractAttributes> {
+        let has_recursion = self.has_recursion();
+        let recursion_check = self.attribute_value(KaniAttributeKind::RecursionCheck);
+        let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith);
+        let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith);
+        let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper);
+
+        let total = recursion_check
+            .iter()
+            .chain(&checked_with)
+            .chain(&replace_with)
+            .chain(&modifies_wrapper)
+            .count();
+        if total != 0 && total != 4 {
+            self.tcx.sess.dcx().err(format!(
+                "Failed to parse contract instrumentation tags in function `{}`.\
+                Expected `4` attributes, but was only able to process `{total}`",
+                self.tcx.def_path_str(self.item)
+            ));
+        }
+        Some(ContractAttributes {
+            has_recursion,
+            recursion_check: recursion_check?,
+            checked_with: checked_with?,
+            replaced_with: replace_with?,
+            modifies_wrapper: modifies_wrapper?,
+        })
     }
 
-    pub fn replaced_with(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
-        self.expect_maybe_one(KaniAttributeKind::ReplacedWith)
-            .map(|target| expect_key_string_value(self.tcx.sess, target))
+    /// Return a function marker if any.
+    pub fn fn_marker(&self) -> Option<Symbol> {
+        self.attribute_value(KaniAttributeKind::FnMarker)
     }
 
-    /// Retrieves the global, static recursion tracker variable.
-    pub fn checked_with_id(&self) -> Option<Result<DefId, ErrorGuaranteed>> {
-        self.eval_sibling_attribute(KaniAttributeKind::CheckedWith)
+    /// Check if function is annotated with any contract attribute.
+    pub fn has_contract(&self) -> bool {
+        self.map.contains_key(&KaniAttributeKind::CheckedWith)
     }
 
-    /// Find the `mod` that `self.item` is defined in, then search in the items defined in this
-    /// `mod` for an item that is named after the `name` in the `#[kanitool::<kind> = "<name>"]`
-    /// annotation on `self.item`.
-    ///
-    /// This is similar to [`resolve_fn`] but more efficient since it only looks inside one `mod`.
-    fn eval_sibling_attribute(
-        &self,
-        kind: KaniAttributeKind,
-    ) -> Option<Result<DefId, ErrorGuaranteed>> {
-        use rustc_hir::{Item, ItemKind, Mod, Node};
-        self.expect_maybe_one(kind).map(|target| {
-            let name = expect_key_string_value(self.tcx.sess, target)?;
-            let hir_map = self.tcx.hir();
-            let hir_id = self.tcx.local_def_id_to_hir_id(self.item.expect_local());
-            let find_in_mod = |md: &Mod<'_>| {
-                md.item_ids
-                    .iter()
-                    .find(|it| hir_map.item(**it).ident.name == name)
-                    .unwrap()
-                    .hir_id()
-            };
-
-            let result = match self.tcx.parent_hir_node(hir_id) {
-                Node::Item(Item { kind, .. }) => match kind {
-                    ItemKind::Mod(m) => find_in_mod(m),
-                    ItemKind::Impl(imp) => {
-                        imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id()
-                    }
-                    other => panic!("Odd parent item kind {other:?}"),
-                },
-                Node::Crate(m) => find_in_mod(m),
-                other => panic!("Odd parent node type {other:?}"),
-            }
-            .expect_owner()
-            .def_id
-            .to_def_id();
-            Ok(result)
-        })
-    }
-
-    fn resolve_sibling(&self, path_str: &str) -> Result<DefId, ResolveError<'tcx>> {
+    /// Resolve a path starting from this item's module context.
+    fn resolve_from_mod(&self, path_str: &str) -> Result<DefId, ResolveError<'tcx>> {
         resolve_fn(
             self.tcx,
             self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(),
@@ -371,20 +371,20 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::StubVerified => {
                     expect_single(self.tcx, kind, &attrs);
                 }
-                KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => {
-                    self.expect_maybe_one(kind)
-                        .map(|attr| expect_key_string_value(&self.tcx.sess, attr));
+                KaniAttributeKind::FnMarker
+                | KaniAttributeKind::CheckedWith
+                | KaniAttributeKind::ModifiesWrapper
+                | KaniAttributeKind::RecursionCheck
+                | KaniAttributeKind::ReplacedWith => {
+                    self.attribute_value(kind);
                 }
                 KaniAttributeKind::IsContractGenerated => {
                     // Ignored here because this is only used by the proc macros
                     // to communicate with one another. So by the time it gets
                     // here we don't care if it's valid or not.
                 }
-                KaniAttributeKind::Modifies => {
-                    self.modifies_contract();
-                }
-                KaniAttributeKind::InnerCheck => {
-                    self.inner_check();
+                KaniAttributeKind::RecursionTracker => {
+                    // Nothing to do here. This is used by contract instrumentation.
                 }
                 KaniAttributeKind::DisableChecks => {
                     // Ignored here, because it should be an internal attribute. Actual validation
@@ -394,6 +394,17 @@ impl<'tcx> KaniAttributes<'tcx> {
         }
     }
 
+    /// Get the value of an attribute if one exists.
+    ///
+    /// This expects up to one attribute with format `#[kanitool::<name>("<value>")]`.
+    ///
+    /// Any format or expectation error is emitted already, and does not need to be handled
+    /// upstream.
+    fn attribute_value(&self, kind: KaniAttributeKind) -> Option<Symbol> {
+        self.expect_maybe_one(kind)
+            .and_then(|target| expect_key_string_value(self.tcx.sess, target).ok())
+    }
+
     /// Check that any unstable API has been enabled. Otherwise, emit an error.
     ///
     /// TODO: Improve error message by printing the span of the harness instead of the definition.
@@ -499,8 +510,9 @@ impl<'tcx> KaniAttributes<'tcx> {
                 }
                 KaniAttributeKind::CheckedWith
                 | KaniAttributeKind::IsContractGenerated
-                | KaniAttributeKind::Modifies
-                | KaniAttributeKind::InnerCheck
+                | KaniAttributeKind::ModifiesWrapper
+                | KaniAttributeKind::RecursionCheck
+                | KaniAttributeKind::RecursionTracker
                 | KaniAttributeKind::ReplacedWith => {
                     self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
                 }
@@ -508,6 +520,9 @@ impl<'tcx> KaniAttributes<'tcx> {
                     // Internal attribute which shouldn't exist here.
                     unreachable!()
                 }
+                KaniAttributeKind::FnMarker => {
+                    /* no-op */
+                }
             };
             harness
         })
@@ -515,15 +530,14 @@ impl<'tcx> KaniAttributes<'tcx> {
 
     fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) {
         let dcx = self.tcx.dcx();
-        let (name, id, span) = match self.interpret_the_for_contract_attribute() {
-            None => unreachable!(
-                "impossible, was asked to handle `proof_for_contract` but didn't find such an attribute."
-            ),
-            Some(Err(_)) => return, // This error was already emitted
-            Some(Ok(values)) => values,
+        let (name, id, span) = match self.interpret_for_contract_attribute() {
+            None => return, // This error was already emitted
+            Some(values) => values,
         };
-        let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with()
-        else {
+        assert!(matches!(
+                &harness.kind, HarnessKind::ProofForContract { target_fn }
+                if *target_fn == name.to_string()));
+        if KaniAttributes::for_item(self.tcx, id).contract_attributes().is_none() {
             dcx.struct_span_err(
                 span,
                 format!(
@@ -533,24 +547,14 @@ impl<'tcx> KaniAttributes<'tcx> {
             )
             .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
             .emit();
-            return;
-        };
-        harness.stubs.push(self.stub_for_relative_item(name, replacement_name));
+        }
     }
 
     fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
         let dcx = self.tcx.dcx();
-        for contract in self.interpret_stub_verified_attribute() {
-            let Ok((name, def_id, span)) = contract else {
-                // This error has already been emitted so we can ignore it now.
-                // Later the session will fail anyway so we can just
-                // optimistically forge on and try to find more errors.
-                continue;
-            };
-            let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with()
-            {
-                None => {
-                    dcx.struct_span_err(
+        for (name, def_id, span) in self.interpret_stub_verified_attribute() {
+            if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() {
+                dcx.struct_span_err(
                         span,
                         format!(
                             "Failed to generate verified stub: Function `{}` has no contract.",
@@ -564,13 +568,10 @@ impl<'tcx> KaniAttributes<'tcx> {
                                 KaniAttributeKind::Stub.as_ref(),
                             ),
                         )
-                        .emit();
-                    continue;
-                }
-                Some(Ok(replacement_name)) => replacement_name,
-                Some(Err(_)) => continue,
-            };
-            harness.stubs.push(self.stub_for_relative_item(name, replacement_name))
+                    .emit();
+                return;
+            }
+            harness.verified_stubs.push(name.to_string())
         }
     }
 
@@ -595,92 +596,6 @@ impl<'tcx> KaniAttributes<'tcx> {
             }
         }
     }
-
-    fn stub_for_relative_item(&self, anchor: Symbol, replacement: Symbol) -> Stub {
-        let local_id = self.item.expect_local();
-        let current_module = self.tcx.parent_module_from_def_id(local_id);
-        let replace_str = replacement.as_str();
-        let original_str = anchor.as_str();
-        let replacement = original_str
-            .rsplit_once("::")
-            .map_or_else(|| replace_str.to_string(), |t| t.0.to_string() + "::" + replace_str);
-        resolve::resolve_fn(self.tcx, current_module.to_local_def_id(), &replacement).unwrap();
-        Stub { original: original_str.to_string(), replacement }
-    }
-
-    /// Parse and interpret the `kanitool::modifies(var1, var2, ...)` annotation into the vector
-    /// `[var1, var2, ...]`.
-    pub fn modifies_contract(&self) -> Option<Vec<Local>> {
-        let local_def_id = self.item.expect_local();
-        self.map.get(&KaniAttributeKind::Modifies).map(|attr| {
-            attr.iter()
-                .flat_map(|clause| match &clause.get_normal_item().args {
-                    AttrArgs::Delimited(lvals) => {
-                        parse_modify_values(self.tcx, local_def_id, &lvals.tokens)
-                    }
-                    _ => unreachable!(),
-                })
-                .collect()
-        })
-    }
-}
-
-/// Pattern macro for the comma token used in attributes.
-macro_rules! comma_tok {
-    () => {
-        TokenTree::Token(Token { kind: TokenKind::Comma, .. }, _)
-    };
-}
-
-/// Parse the token stream inside an attribute (like `kanitool::modifies`) as a comma separated
-/// sequence of function parameter names on `local_def_id` (must refer to a function). Then
-/// translates the names into [`Local`]s.
-fn parse_modify_values<'a>(
-    tcx: TyCtxt<'a>,
-    local_def_id: LocalDefId,
-    t: &'a TokenStream,
-) -> impl Iterator<Item = Local> + 'a {
-    let mir = tcx.optimized_mir(local_def_id);
-    let mut iter = t.trees();
-    std::iter::from_fn(move || {
-        let tree = iter.next()?;
-        let wrong_token_err =
-            || tcx.sess.dcx().span_err(tree.span(), "Unexpected token. Expected identifier.");
-        let result = match tree {
-            TokenTree::Token(token, _) => {
-                if let TokenKind::Ident(id, _) = &token.kind {
-                    let hir = tcx.hir();
-                    let bid = hir.body_owned_by(local_def_id).id();
-                    Some(
-                        hir.body_param_names(bid)
-                            .zip(mir.args_iter())
-                            .find(|(name, _decl)| name.name == *id)
-                            .unwrap()
-                            .1
-                            .as_usize(),
-                    )
-                } else {
-                    wrong_token_err();
-                    None
-                }
-            }
-            _ => {
-                wrong_token_err();
-                None
-            }
-        };
-        match iter.next() {
-            None | Some(comma_tok!()) => (),
-            Some(not_comma) => {
-                tcx.sess.dcx().span_err(
-                    not_comma.span(),
-                    "Unexpected token, expected end of attribute or comma",
-                );
-                iter.by_ref().skip_while(|t| !matches!(t, comma_tok!())).count();
-            }
-        }
-        result
-    })
 }
 
 /// An efficient check for the existence for a particular [`KaniAttributeKind`].
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index b4ea06c8d5db..d16e4d2b93d1 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -11,23 +11,24 @@ use crate::args::ReachabilityType;
 use crate::kani_middle::attributes::is_proof_harness;
 use crate::kani_middle::metadata::gen_proof_metadata;
 use crate::kani_middle::reachability::filter_crate_items;
+use crate::kani_middle::resolve::expect_resolve_fn;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
 use crate::kani_queries::QueryDb;
-use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata};
-use rustc_hir::def_id::{DefId, DefPathHash};
+use kani_metadata::{ArtifactType, AssignsContract, HarnessKind, HarnessMetadata, KaniMetadata};
+use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::ty::{FnDef, RigidTy, TyKind};
+use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind};
 use stable_mir::CrateDef;
-use std::collections::{BTreeMap, HashMap, HashSet};
+use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;
 use std::io::BufWriter;
 use std::path::{Path, PathBuf};
 use tracing::debug;
 
-/// A stable (across compilation sessions) identifier for the harness function.
+/// An identifier for the harness function.
 type Harness = Instance;
 
 /// A set of stubs.
@@ -124,20 +125,21 @@ fn stub_def(tcx: TyCtxt, def_id: DefId) -> FnDef {
     }
 }
 
-/// Group the harnesses by their stubs.
+/// Group the harnesses by their stubs and contract usage.
 fn group_by_stubs(
     tcx: TyCtxt,
     all_harnesses: &HashMap<Harness, HarnessMetadata>,
 ) -> Vec<CodegenUnit> {
-    let mut per_stubs: HashMap<BTreeMap<DefPathHash, DefPathHash>, CodegenUnit> =
-        HashMap::default();
+    let mut per_stubs: HashMap<_, CodegenUnit> = HashMap::default();
     for (harness, metadata) in all_harnesses {
         let stub_ids = harness_stub_map(tcx, *harness, metadata);
+        let contracts = extract_contracts(tcx, *harness, metadata);
         let stub_map = stub_ids
             .iter()
             .map(|(k, v)| (tcx.def_path_hash(*k), tcx.def_path_hash(*v)))
             .collect::<BTreeMap<_, _>>();
-        if let Some(unit) = per_stubs.get_mut(&stub_map) {
+        let key = (contracts, stub_map);
+        if let Some(unit) = per_stubs.get_mut(&key) {
             unit.harnesses.push(*harness);
         } else {
             let stubs = stub_ids
@@ -145,12 +147,43 @@ fn group_by_stubs(
                 .map(|(from, to)| (stub_def(tcx, *from), stub_def(tcx, *to)))
                 .collect::<HashMap<_, _>>();
             let stubs = apply_transitivity(tcx, *harness, stubs);
-            per_stubs.insert(stub_map, CodegenUnit { stubs, harnesses: vec![*harness] });
+            per_stubs.insert(key, CodegenUnit { stubs, harnesses: vec![*harness] });
         }
     }
     per_stubs.into_values().collect()
 }
 
+#[derive(Copy, Clone, Debug, Ord, PartialOrd, PartialEq, Eq, Hash)]
+enum ContractUsage {
+    Stub(usize),
+    Check(usize),
+}
+
+/// Extract the contract related usages.
+///
+/// Note that any error interpreting the result is emitted, but we delay aborting, so we emit as
+/// many errors as possible.
+fn extract_contracts(
+    tcx: TyCtxt,
+    harness: Harness,
+    metadata: &HarnessMetadata,
+) -> BTreeSet<ContractUsage> {
+    let def = harness.def;
+    let mut result = BTreeSet::new();
+    if let HarnessKind::ProofForContract { target_fn } = &metadata.attributes.kind {
+        if let Ok(check_def) = expect_resolve_fn(tcx, def, target_fn, "proof_for_contract") {
+            result.insert(ContractUsage::Check(check_def.def_id().to_index()));
+        }
+    }
+
+    for stub in &metadata.attributes.verified_stubs {
+        let Ok(stub_def) = expect_resolve_fn(tcx, def, stub, "stub_verified") else { continue };
+        result.insert(ContractUsage::Stub(stub_def.def_id().to_index()));
+    }
+
+    result
+}
+
 /// Extract the filename for the metadata file.
 fn metadata_output_path(tcx: TyCtxt) -> PathBuf {
     let filepath = tcx.output_filenames(()).path(OutputType::Object);
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 816f25343fe3..ca4e8e749b75 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -9,14 +9,18 @@
 //!
 //! Note that glob use statements can form loops. The paths can also walk through the loop.
 
+use rustc_smir::rustc_internal;
 use std::collections::HashSet;
 use std::fmt;
 use std::iter::Peekable;
 
+use rustc_errors::ErrorGuaranteed;
 use rustc_hir::def::{DefKind, Res};
 use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE};
 use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
+use stable_mir::ty::{FnDef, RigidTy, TyKind};
+use stable_mir::CrateDef;
 use tracing::debug;
 
 /// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`.
@@ -47,6 +51,33 @@ pub fn resolve_fn<'tcx>(
     }
 }
 
+/// Resolve the name of a function from the context of the definition provided.
+///
+/// Ideally this should pass a more precise span, but we don't keep them around.
+pub fn expect_resolve_fn<T: CrateDef>(
+    tcx: TyCtxt,
+    res_cx: T,
+    name: &str,
+    reason: &str,
+) -> Result<FnDef, ErrorGuaranteed> {
+    let internal_def_id = rustc_internal::internal(tcx, res_cx.def_id());
+    let current_module = tcx.parent_module_from_def_id(internal_def_id.as_local().unwrap());
+    let maybe_resolved = resolve_fn(tcx, current_module.to_local_def_id(), name);
+    let resolved = maybe_resolved.map_err(|err| {
+        tcx.dcx().span_err(
+            rustc_internal::internal(tcx, res_cx.span()),
+            format!("Failed to resolve `{name}` for `{reason}`: {err}"),
+        )
+    })?;
+    let ty_internal = tcx.type_of(resolved).instantiate_identity();
+    let ty = rustc_internal::stable(ty_internal);
+    if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = ty.kind() {
+        Ok(def)
+    } else {
+        unreachable!("Expected function for `{name}`, but found: {ty}")
+    }
+}
+
 /// Attempts to resolve a simple path (in the form of a string) to a `DefId`.
 /// The current module is provided as an argument in order to resolve relative
 /// paths.
diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index d3f2afc15d31..3d110c4e9656 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -54,6 +54,10 @@ impl MutableBody {
         &self.locals
     }
 
+    pub fn arg_count(&self) -> usize {
+        self.arg_count
+    }
+
     /// Create a mutable body from the original MIR body.
     pub fn from(body: Body) -> Self {
         MutableBody {
@@ -147,6 +151,19 @@ impl MutableBody {
         result
     }
 
+    /// Add a new assignment to an existing place.
+    pub fn assign_to(
+        &mut self,
+        place: Place,
+        rvalue: Rvalue,
+        source: &mut SourceInstruction,
+        position: InsertPosition,
+    ) {
+        let span = source.span(&self.blocks);
+        let stmt = Statement { kind: StatementKind::Assign(place, rvalue), span };
+        self.insert_stmt(stmt, source, position);
+    }
+
     /// Add a new assert to the basic block indicated by the given index.
     ///
     /// The new assertion will have the same span as the source instruction, and the basic block
@@ -402,12 +419,21 @@ impl MutableBody {
     /// by the compiler. This function allow us to delete the dummy body before
     /// creating a new one.
     ///
-    /// Note: We do not prune the local variables today for simplicity.
-    pub fn clear_body(&mut self) {
+    /// Keep all the locals untouched, so they can be reused by the passes if needed.
+    pub fn clear_body(&mut self, kind: TerminatorKind) {
         self.blocks.clear();
-        let terminator = Terminator { kind: TerminatorKind::Return, span: self.span };
+        let terminator = Terminator { kind, span: self.span };
         self.blocks.push(BasicBlock { statements: Vec::default(), terminator })
     }
+
+    /// Replace a terminator from the given basic block
+    pub fn replace_terminator(
+        &mut self,
+        source_instruction: &SourceInstruction,
+        new_term: Terminator,
+    ) {
+        self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term;
+    }
 }
 
 #[derive(Clone, Debug)]
@@ -469,6 +495,12 @@ impl SourceInstruction {
             SourceInstruction::Terminator { bb } => blocks[bb].terminator.span,
         }
     }
+
+    pub fn bb(&self) -> BasicBlockIdx {
+        match *self {
+            SourceInstruction::Statement { bb, .. } | SourceInstruction::Terminator { bb } => bb,
+        }
+    }
 }
 
 fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option<Instance> {
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index 3a835c7f3cb6..71e06f5c49cd 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -3,16 +3,21 @@
 //! This module contains code related to the MIR-to-MIR pass to enable contracts.
 use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::codegen_units::CodegenUnit;
-use crate::kani_middle::transform::body::MutableBody;
+use crate::kani_middle::find_fn_def;
+use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use cbmc::{InternString, InternedString};
+use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
+use rustc_span::Symbol;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind};
-use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind, TypeAndMut};
-use stable_mir::{CrateDef, DefId};
+use stable_mir::mir::{
+    Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents,
+};
+use stable_mir::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy};
+use stable_mir::CrateDef;
 use std::collections::HashSet;
 use std::fmt::Debug;
 use tracing::{debug, trace};
@@ -34,7 +39,6 @@ pub struct AnyModifiesPass {
     kani_write_any_slim: Option<FnDef>,
     kani_write_any_slice: Option<FnDef>,
     kani_write_any_str: Option<FnDef>,
-    stubbed: HashSet<DefId>,
     target_fn: Option<InternedString>,
 }
 
@@ -50,7 +54,7 @@ impl TransformPass for AnyModifiesPass {
     where
         Self: Sized,
     {
-        // TODO: Check if this is the harness has proof_for_contract
+        // TODO: Check if the harness has proof_for_contract
         query_db.args().unstable_features.contains(&"function-contracts".to_string())
             && self.kani_any.is_some()
     }
@@ -62,8 +66,8 @@ impl TransformPass for AnyModifiesPass {
         if instance.def.def_id() == self.kani_any.unwrap().def_id() {
             // Ensure kani::any is valid.
             self.any_body(tcx, body)
-        } else if self.should_apply(tcx, instance) {
-            // Replace any modifies occurrences.
+        } else if instance.ty().kind().is_closure() {
+            // Replace any modifies occurrences. They should only happen in the contract closures.
             self.replace_any_modifies(body)
         } else {
             (false, body)
@@ -74,38 +78,19 @@ impl TransformPass for AnyModifiesPass {
 impl AnyModifiesPass {
     /// Build the pass with non-extern function stubs.
     pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> AnyModifiesPass {
-        let item_fn_def = |item| {
-            let TyKind::RigidTy(RigidTy::FnDef(def, _)) =
-                rustc_internal::stable(tcx.type_of(item)).value.kind()
-            else {
-                unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item))
-            };
-            def
-        };
-        let kani_any =
-            tcx.get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny")).map(item_fn_def);
-        let kani_any_modifies = tcx
-            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies"))
-            .map(item_fn_def);
-        let kani_write_any = tcx
-            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAny"))
-            .map(item_fn_def);
-        let kani_write_any_slim = tcx
-            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlim"))
-            .map(item_fn_def);
-        let kani_write_any_slice = tcx
-            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlice"))
-            .map(item_fn_def);
-        let kani_write_any_str = tcx
-            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnyStr"))
-            .map(item_fn_def);
-        let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() {
+        let kani_any = find_fn_def(tcx, "KaniAny");
+        let kani_any_modifies = find_fn_def(tcx, "KaniAnyModifies");
+        let kani_write_any = find_fn_def(tcx, "KaniWriteAny");
+        let kani_write_any_slim = find_fn_def(tcx, "KaniWriteAnySlim");
+        let kani_write_any_slice = find_fn_def(tcx, "KaniWriteAnySlice");
+        let kani_write_any_str = find_fn_def(tcx, "KaniWriteAnyStr");
+        let target_fn = if let Some(harness) = unit.harnesses.first() {
             let attributes = KaniAttributes::for_instance(tcx, *harness);
             let target_fn =
                 attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern());
-            (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::<HashSet<_>>())
+            target_fn
         } else {
-            (None, HashSet::new())
+            None
         };
         AnyModifiesPass {
             kani_any,
@@ -115,27 +100,17 @@ impl AnyModifiesPass {
             kani_write_any_slice,
             kani_write_any_str,
             target_fn,
-            stubbed,
         }
     }
 
-    /// If we apply `transform_any_modifies` in all contract-generated items,
-    /// we will end up instantiating `kani::any_modifies` for the replace function
-    /// every time, even if we are only checking the contract, because the function
-    /// is always included during contract instrumentation. Thus, we must only apply
-    /// the transformation if we are using a verified stub or in the presence of recursion.
-    fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        let item_attributes =
-            KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id()));
-        self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion()
-    }
-
     /// Replace calls to `any_modifies` by calls to `any`.
     fn replace_any_modifies(&self, mut body: Body) -> (bool, Body) {
         let mut changed = false;
         let locals = body.locals().to_vec();
         for bb in body.blocks.iter_mut() {
-            let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else { continue };
+            let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else {
+                continue;
+            };
             if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) =
                 func.ty(&locals).unwrap().kind()
                 && Some(def) == self.kani_any_modifies
@@ -199,7 +174,9 @@ impl AnyModifiesPass {
         let mut valid = true;
         let locals = body.locals().to_vec();
         for bb in body.blocks.iter_mut() {
-            let TerminatorKind::Call { func, .. } = &mut bb.terminator.kind else { continue };
+            let TerminatorKind::Call { func, .. } = &mut bb.terminator.kind else {
+                continue;
+            };
             if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = func.ty(&locals).unwrap().kind() {
                 match Instance::resolve(def, &args) {
                     Ok(_) => {}
@@ -232,8 +209,306 @@ impl AnyModifiesPass {
             (true, body)
         } else {
             let mut new_body = MutableBody::from(body);
-            new_body.clear_body();
-            (false, new_body.into())
+            new_body.clear_body(TerminatorKind::Unreachable);
+            (true, new_body.into())
         }
     }
 }
+
+/// This pass will transform functions annotated with contracts based on the harness configuration.
+///
+/// Functions with contract will always follow the same structure:
+///
+/// ```ignore
+/// #[kanitool::recursion_check = "__kani_recursion_check_modify"]
+/// #[kanitool::checked_with = "__kani_check_modify"]
+/// #[kanitool::replaced_with = "__kani_replace_modify"]
+/// #[kanitool::modifies_wrapper = "__kani_modifies_modify"]
+/// fn name_fn(ptr: &mut u32) {
+///     #[kanitool::fn_marker = "kani_register_contract"]
+///     pub const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+///         kani::panic("internal error: entered unreachable code: ")
+///     }
+///     let kani_contract_mode = kani::internal::mode();
+///     match kani_contract_mode {
+///         kani::internal::RECURSION_CHECK => {
+///             #[kanitool::is_contract_generated(recursion_check)]
+///             let mut __kani_recursion_check_name_fn = || { /* recursion check body */ };
+///             kani_register_contract(__kani_recursion_check_modify)
+///         }
+///         kani::internal::REPLACE => {
+///             #[kanitool::is_contract_generated(replace)]
+///             let mut __kani_replace_name_fn = || { /* replace body */ };
+///             kani_register_contract(__kani_replace_name_fn)
+///         }
+///         kani::internal::SIMPLE_CHECK => {
+///             #[kanitool::is_contract_generated(check)]
+///             let mut __kani_check_name_fn = || { /* check body */ };
+///             kani_register_contract(__kani_check_name_fn)
+///         }
+///         _ => { /* original body */ }
+///     }
+/// }
+/// ```
+///
+/// This pass will perform the following operations:
+/// 1. For functions with contract that are not being used for check or replacement:
+///    - Set `kani_contract_mode` to the value ORIGINAL.
+///    - Replace the generated closures body with unreachable.
+/// 2. For functions with contract that are being used:
+///    - Set `kani_contract_mode` to the value corresponding to the expected usage.
+///    - Replace the non-used generated closures body with unreachable.
+/// 3. Replace the body of `kani_register_contract` by `kani::internal::run_contract_fn` to
+///    invoke the closure.
+#[derive(Debug, Default)]
+pub struct FunctionWithContractPass {
+    /// Function that is being checked, if any.
+    check_fn: Option<InternalDefId>,
+    /// Functions that should be stubbed by their contract.
+    replace_fns: HashSet<InternalDefId>,
+    /// Functions annotated with contract attributes will contain contract closures even if they
+    /// are not to be used in this harness.
+    /// In order to avoid bringing unnecessary logic, we clear their body.
+    unused_closures: HashSet<ClosureDef>,
+    /// Cache KaniRunContract function used to implement contracts.
+    run_contract_fn: Option<FnDef>,
+}
+
+impl TransformPass for FunctionWithContractPass {
+    fn transformation_type() -> TransformationType
+    where
+        Self: Sized,
+    {
+        TransformationType::Stubbing
+    }
+
+    fn is_enabled(&self, _query_db: &QueryDb) -> bool
+    where
+        Self: Sized,
+    {
+        true
+    }
+
+    /// Transform the function body by replacing it with the stub body.
+    fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+        trace!(function=?instance.name(), "FunctionWithContractPass::transform");
+        match instance.ty().kind().rigid().unwrap() {
+            RigidTy::FnDef(def, args) => {
+                if let Some(mode) = self.contract_mode(tcx, *def) {
+                    self.mark_unused(tcx, *def, &body, mode);
+                    let new_body = self.set_mode(tcx, body, mode);
+                    (true, new_body)
+                } else if KaniAttributes::for_instance(tcx, instance).fn_marker()
+                    == Some(Symbol::intern("kani_register_contract"))
+                {
+                    let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap();
+                    (true, run.body().unwrap())
+                } else {
+                    // Not a contract annotated function
+                    (false, body)
+                }
+            }
+            RigidTy::Closure(def, _args) => {
+                if self.unused_closures.contains(def) {
+                    // Delete body and mark it as unreachable.
+                    let mut new_body = MutableBody::from(body);
+                    new_body.clear_body(TerminatorKind::Unreachable);
+                    (true, new_body.into())
+                } else {
+                    // Not a contract annotated function
+                    (false, body)
+                }
+            }
+            _ => {
+                /* static variables case */
+                (false, body)
+            }
+        }
+    }
+}
+
+impl FunctionWithContractPass {
+    /// Build the pass by collecting which functions we are stubbing and which ones we are
+    /// verifying.
+    pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> FunctionWithContractPass {
+        if let Some(harness) = unit.harnesses.first() {
+            let attrs = KaniAttributes::for_instance(tcx, *harness);
+            let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id);
+            let replace_fns: HashSet<_> = attrs
+                .interpret_stub_verified_attribute()
+                .iter()
+                .map(|(_, def_id, _)| *def_id)
+                .collect();
+            let run_contract_fn = find_fn_def(tcx, "KaniRunContract");
+            assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function");
+            FunctionWithContractPass {
+                check_fn,
+                replace_fns,
+                unused_closures: Default::default(),
+                run_contract_fn,
+            }
+        } else {
+            // If reachability mode is PubFns or Tests, we just remove any contract logic.
+            // Note that in this path there is no proof harness.
+            FunctionWithContractPass::default()
+        }
+    }
+
+    /// Functions with contract have the following structure:
+    /// ```ignore
+    /// fn original([self], args*) {
+    ///    let kani_contract_mode = kani::internal::mode(); // ** Replace this call
+    ///    match kani_contract_mode {
+    ///        kani::internal::RECURSION_CHECK => {
+    ///            let closure = |/*args*/|{ /*body*/};
+    ///            kani_register_contract(closure) // ** Replace this call
+    ///        }
+    ///        kani::internal::REPLACE => {
+    ///            // same as above
+    ///        }
+    ///        kani::internal::SIMPLE_CHECK => {
+    ///            // same as above
+    ///        }
+    ///        _ => { /* original code */}
+    ///    }
+    /// }
+    /// ```
+    /// See function `handle_untouched` inside `kani_macros`.
+    ///
+    /// Thus, we need to:
+    /// 1. Initialize `kani_contract_mode` variable to the value corresponding to the mode.
+    ///
+    /// Thus replace this call:
+    /// ```ignore
+    ///    let kani_contract_mode = kani::internal::mode(); // ** Replace this call
+    /// ```
+    /// by:
+    /// ```ignore
+    ///    let kani_contract_mode = mode_const;
+    ///    goto bbX;
+    /// ```
+    /// 2. Replace `kani_register_contract` by the call to the closure.
+    fn set_mode(&self, tcx: TyCtxt, body: Body, mode: ContractMode) -> Body {
+        debug!(?mode, "set_mode");
+        let mut new_body = MutableBody::from(body);
+        let (mut mode_call, ret, target) = new_body
+            .blocks()
+            .iter()
+            .enumerate()
+            .find_map(|(bb_idx, bb)| {
+                if let TerminatorKind::Call { func, target, destination, .. } = &bb.terminator.kind
+                {
+                    let (callee, _) = func.ty(new_body.locals()).unwrap().kind().fn_def()?;
+                    let marker = KaniAttributes::for_def_id(tcx, callee.def_id()).fn_marker();
+                    if marker.is_some_and(|s| s.as_str() == "kani_contract_mode") {
+                        return Some((
+                            SourceInstruction::Terminator { bb: bb_idx },
+                            destination.clone(),
+                            target.unwrap(),
+                        ));
+                    }
+                }
+                None
+            })
+            .unwrap();
+
+        let span = mode_call.span(new_body.blocks());
+        let mode_const = new_body.new_uint_operand(mode as _, UintTy::U8, span);
+        new_body.assign_to(
+            ret.clone(),
+            Rvalue::Use(mode_const),
+            &mut mode_call,
+            InsertPosition::Before,
+        );
+        new_body.replace_terminator(
+            &mode_call,
+            Terminator { kind: TerminatorKind::Goto { target }, span },
+        );
+
+        new_body.into()
+    }
+
+    /// Return which contract mode to use for this function if any.
+    fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option<ContractMode> {
+        let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id());
+        kani_attributes.has_contract().then(|| {
+            let fn_def_id = rustc_internal::internal(tcx, fn_def.def_id());
+            if self.check_fn == Some(fn_def_id) {
+                if kani_attributes.has_recursion() {
+                    ContractMode::RecursiveCheck
+                } else {
+                    ContractMode::SimpleCheck
+                }
+            } else if self.replace_fns.contains(&fn_def_id) {
+                ContractMode::Replace
+            } else {
+                ContractMode::Original
+            }
+        })
+    }
+
+    /// Select any unused closure for body deletion.
+    fn mark_unused(&mut self, tcx: TyCtxt, fn_def: FnDef, body: &Body, mode: ContractMode) {
+        let contract =
+            KaniAttributes::for_def_id(tcx, fn_def.def_id()).contract_attributes().unwrap();
+        let recursion_closure = find_closure(tcx, fn_def, &body, contract.recursion_check.as_str());
+        let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str());
+        let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str());
+        match mode {
+            ContractMode::Original => {
+                // No contract instrumentation needed. Add all closures to the list of unused.
+                self.unused_closures.insert(recursion_closure);
+                self.unused_closures.insert(check_closure);
+                self.unused_closures.insert(replace_closure);
+            }
+            ContractMode::RecursiveCheck => {
+                self.unused_closures.insert(replace_closure);
+                self.unused_closures.insert(check_closure);
+            }
+            ContractMode::SimpleCheck => {
+                self.unused_closures.insert(replace_closure);
+                self.unused_closures.insert(recursion_closure);
+            }
+            ContractMode::Replace => {
+                self.unused_closures.insert(recursion_closure);
+                self.unused_closures.insert(check_closure);
+            }
+        }
+    }
+}
+
+/// Enumeration that store the value of which implementation should be selected.
+///
+/// Keep the discriminant values in sync with [kani::internal::mode].
+#[derive(Copy, Clone, Debug, PartialEq, Eq)]
+enum ContractMode {
+    Original = 0,
+    RecursiveCheck = 1,
+    SimpleCheck = 2,
+    Replace = 3,
+}
+
+fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef {
+    body.var_debug_info
+        .iter()
+        .find_map(|var_info| {
+            if var_info.name.as_str() == name {
+                let ty = match &var_info.value {
+                    VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
+                    VarDebugInfoContents::Const(const_op) => const_op.ty(),
+                };
+                if let TyKind::RigidTy(RigidTy::Closure(def, _args)) = ty.kind() {
+                    return Some(def);
+                }
+            }
+            None
+        })
+        .unwrap_or_else(|| {
+            tcx.sess.dcx().err(format!(
+                "Failed to find contract closure `{name}` in function `{}`",
+                fn_def.name()
+            ));
+            tcx.sess.dcx().abort_if_errors();
+            unreachable!()
+        })
+}
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index d6475465d1b1..82ff25bb2442 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -19,7 +19,8 @@ use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
-    BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
+    BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind,
+    RETURN_LOCAL,
 };
 use stable_mir::target::MachineInfo;
 use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy};
@@ -86,7 +87,7 @@ impl IntrinsicGeneratorPass {
     /// ```
     fn valid_value_body(&self, tcx: TyCtxt, body: Body) -> Body {
         let mut new_body = MutableBody::from(body);
-        new_body.clear_body();
+        new_body.clear_body(TerminatorKind::Return);
 
         // Initialize return variable with True.
         let ret_var = RETURN_LOCAL;
@@ -163,7 +164,7 @@ impl IntrinsicGeneratorPass {
     /// ```
     fn is_initialized_body(&mut self, tcx: TyCtxt, body: Body) -> Body {
         let mut new_body = MutableBody::from(body);
-        new_body.clear_body();
+        new_body.clear_body(TerminatorKind::Return);
 
         // Initialize return variable with True.
         let ret_var = RETURN_LOCAL;
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index 5b497b09619d..4f3125e59868 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -21,7 +21,7 @@ use crate::kani_middle::reachability::CallGraph;
 use crate::kani_middle::transform::body::CheckType;
 use crate::kani_middle::transform::check_uninit::UninitPass;
 use crate::kani_middle::transform::check_values::ValidValuePass;
-use crate::kani_middle::transform::contracts::AnyModifiesPass;
+use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass};
 use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
 use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass};
 use crate::kani_queries::QueryDb;
@@ -66,7 +66,9 @@ impl BodyTransformation {
         let check_type = CheckType::new_assert_assume(tcx);
         transformer.add_pass(queries, FnStubPass::new(&unit.stubs));
         transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs));
-        // This has to come after stubs since we want this to replace the stubbed body.
+        transformer.add_pass(queries, FunctionWithContractPass::new(tcx, &unit));
+        // This has to come after the contract pass since we want this to only replace the closure
+        // body that is relevant for this harness.
         transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit));
         transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() });
         // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by
diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs
index ae76be150871..d31d4dae90f6 100644
--- a/kani-driver/src/call_goto_instrument.rs
+++ b/kani-driver/src/call_goto_instrument.rs
@@ -167,18 +167,20 @@ impl KaniSession {
     pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
         let Some(assigns) = harness.contract.as_ref() else { return Ok(()) };
 
-        let args: &[std::ffi::OsString] = &[
+        let mut args: Vec<OsString> = vec![
             "--dfcc".into(),
             (&harness.mangled_name).into(),
             "--enforce-contract".into(),
             assigns.contracted_function_name.as_str().into(),
-            "--nondet-static-exclude".into(),
-            assigns.recursion_tracker.as_str().into(),
             "--no-malloc-may-fail".into(),
             file.into(),
             file.into(),
         ];
-        self.call_goto_instrument(args)
+        if let Some(tracker) = &assigns.recursion_tracker {
+            args.push("--nondet-static-exclude".into());
+            args.push(tracker.as_str().into());
+        }
+        self.call_goto_instrument(&args)
     }
 
     /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table
diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
index 41eb4eb20919..426cf8d9e960 100644
--- a/kani_metadata/src/harness.rs
+++ b/kani_metadata/src/harness.rs
@@ -11,7 +11,8 @@ pub struct AssignsContract {
     /// The target of the contract
     pub contracted_function_name: String,
     /// A static global variable used to track recursion that must not be havocked.
-    pub recursion_tracker: String,
+    /// This is only needed if the function is tagged with `#[kani::recursive]`
+    pub recursion_tracker: Option<String>,
 }
 
 /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find.
@@ -50,6 +51,8 @@ pub struct HarnessAttributes {
     pub unwind_value: Option<u32>,
     /// The stubs used in this harness.
     pub stubs: Vec<Stub>,
+    /// The name of the functions being stubbed by their contract.
+    pub verified_stubs: Vec<String>,
 }
 
 #[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
@@ -71,6 +74,7 @@ impl HarnessAttributes {
             solver: None,
             unwind_value: None,
             stubs: vec![],
+            verified_stubs: vec![],
         }
     }
 
diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
index 22026065106a..68b15316b4c1 100644
--- a/library/kani/src/internal.rs
+++ b/library/kani/src/internal.rs
@@ -8,60 +8,39 @@ use std::ptr;
 ///
 /// We allow the user to provide us with a pointer-like object that we convert as needed.
 #[doc(hidden)]
-pub trait Pointer<'a> {
+pub trait Pointer {
     /// Type of the pointed-to data
     type Inner: ?Sized;
 
-    /// Used for checking assigns contracts where we pass immutable references to the function.
-    ///
-    /// We're using a reference to self here, because the user can use just a plain function
-    /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it.
-    unsafe fn decouple_lifetime(&self) -> &'a Self::Inner;
-
+    /// used for havocking on replecement of a `modifies` clause.
     unsafe fn assignable(self) -> *mut Self::Inner;
 }
 
-impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T {
+impl<T: ?Sized> Pointer for &T {
     type Inner = T;
-    unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-        std::mem::transmute(*self)
-    }
-
     unsafe fn assignable(self) -> *mut Self::Inner {
-        std::mem::transmute(self as *const T)
+        self as *const T as *mut T
     }
 }
 
-impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T {
+impl<T: ?Sized> Pointer for &mut T {
     type Inner = T;
 
-    #[allow(clippy::transmute_ptr_to_ref)]
-    unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-        std::mem::transmute::<_, &&'a T>(self)
-    }
-
     unsafe fn assignable(self) -> *mut Self::Inner {
         self as *mut T
     }
 }
 
-impl<'a, T: ?Sized> Pointer<'a> for *const T {
+impl<T: ?Sized> Pointer for *const T {
     type Inner = T;
-    unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-        &**self as &'a T
-    }
 
     unsafe fn assignable(self) -> *mut Self::Inner {
-        std::mem::transmute(self)
+        self as *mut T
     }
 }
 
-impl<'a, T: ?Sized> Pointer<'a> for *mut T {
+impl<T: ?Sized> Pointer for *mut T {
     type Inner = T;
-    unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-        &**self as &'a T
-    }
-
     unsafe fn assignable(self) -> *mut Self::Inner {
         self
     }
@@ -69,6 +48,8 @@ impl<'a, T: ?Sized> Pointer<'a> for *mut T {
 
 /// A way to break the ownerhip rules. Only used by contracts where we can
 /// guarantee it is done safely.
+/// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if
+/// they really need to. See <https://github.com/model-checking/kani/issues/3293>.
 #[inline(never)]
 #[doc(hidden)]
 #[rustc_diagnostic_item = "KaniUntrackedDeref"]
@@ -92,6 +73,8 @@ pub fn init_contracts() {}
 
 /// This should only be used within contracts. The intent is to
 /// perform type inference on a closure's argument
+/// TODO: This should be generated inside the function that has contract. This is used for
+/// remembers.
 #[doc(hidden)]
 pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
     f(x)
@@ -142,3 +125,36 @@ pub unsafe fn write_any_str(_s: *mut str) {
     //TODO: String validation
     unimplemented!("Kani does not support creating arbitrary `str`")
 }
+
+/// Function that calls a closure used to implement contracts.
+///
+/// In contracts, we cannot invoke the generated closures directly, instead, we call register
+/// contract. This function is a no-op. However, in the reality, we do want to call the closure,
+/// so we swap the register body by this function body.
+#[doc(hidden)]
+#[allow(dead_code)]
+#[rustc_diagnostic_item = "KaniRunContract"]
+#[crate::unstable(
+    feature = "function-contracts",
+    issue = "none",
+    reason = "internal function required to run contract closure"
+)]
+fn run_contract_fn<T, F: FnOnce() -> T>(func: F) -> T {
+    func()
+}
+
+/// This is used by contracts to select which version of the contract to use during codegen.
+#[doc(hidden)]
+pub type Mode = u8;
+
+/// Keep the original body.
+pub const ORIGINAL: Mode = 0;
+
+/// Run the check with recursion support.
+pub const RECURSION_CHECK: Mode = 1;
+
+/// Run the simple check with no recursion support.
+pub const SIMPLE_CHECK: Mode = 2;
+
+/// Stub the body with its contract.
+pub const REPLACE: Mode = 3;
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 9baba1abe886..b7263816800a 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -306,60 +306,39 @@ macro_rules! kani_intrinsics {
             ///
             /// We allow the user to provide us with a pointer-like object that we convert as needed.
             #[doc(hidden)]
-            pub trait Pointer<'a> {
+            pub trait Pointer {
                 /// Type of the pointed-to data
                 type Inner: ?Sized;
 
-                /// Used for checking assigns contracts where we pass immutable references to the function.
-                ///
-                /// We're using a reference to self here, because the user can use just a plain function
-                /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it.
-                unsafe fn decouple_lifetime(&self) -> &'a Self::Inner;
-
+                /// used for havocking on replecement of a `modifies` clause.
                 unsafe fn assignable(self) -> *mut Self::Inner;
             }
 
-            impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T {
+            impl<T: ?Sized> Pointer for &T {
                 type Inner = T;
-                unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-                    core::mem::transmute(*self)
-                }
-
                 unsafe fn assignable(self) -> *mut Self::Inner {
-                    core::mem::transmute(self as *const T)
+                    self as *const T as *mut T
                 }
             }
 
-            impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T {
+            impl<T: ?Sized> Pointer for &mut T {
                 type Inner = T;
 
-                #[allow(clippy::transmute_ptr_to_ref)]
-                unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-                    core::mem::transmute::<_, &&'a T>(self)
-                }
-
                 unsafe fn assignable(self) -> *mut Self::Inner {
                     self as *mut T
                 }
             }
 
-            impl<'a, T: ?Sized> Pointer<'a> for *const T {
+            impl<T: ?Sized> Pointer for *const T {
                 type Inner = T;
-                unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-                    &**self as &'a T
-                }
 
                 unsafe fn assignable(self) -> *mut Self::Inner {
-                    core::mem::transmute(self)
+                    self as *mut T
                 }
             }
 
-            impl<'a, T: ?Sized> Pointer<'a> for *mut T {
+            impl<T: ?Sized> Pointer for *mut T {
                 type Inner = T;
-                unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-                    &**self as &'a T
-                }
-
                 unsafe fn assignable(self) -> *mut Self::Inner {
                     self
                 }
@@ -436,6 +415,34 @@ macro_rules! kani_intrinsics {
                 //TODO: String validation
                 unimplemented!("Kani does not support creating arbitrary `str`")
             }
+
+            /// Function that calls a closure used to implement contracts.
+            ///
+            /// In contracts, we cannot invoke the generated closures directly, instead, we call register
+            /// contract. This function is a no-op. However, in the reality, we do want to call the closure,
+            /// so we swap the register body by this function body.
+            #[doc(hidden)]
+            #[allow(dead_code)]
+            #[rustc_diagnostic_item = "KaniRunContract"]
+            fn run_contract_fn<T, F: FnOnce() -> T>(func: F) -> T {
+                func()
+            }
+
+            /// This is used by contracts to select which version of the contract to use during codegen.
+            #[doc(hidden)]
+            pub type Mode = u8;
+
+            /// Keep the original body.
+            pub const ORIGINAL: Mode = 0;
+
+            /// Run the check with recursion support.
+            pub const RECURSION_CHECK: Mode = 1;
+
+            /// Run the simple check with no recursion support.
+            pub const SIMPLE_CHECK: Mode = 2;
+
+            /// Stub the body with its contract.
+            pub const REPLACE: Mode = 3;
         }
     };
 }
diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index dee0bca42c54..8ad21e8a9c6b 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -4,106 +4,152 @@
 //! Special way we handle the first time we encounter a contract attribute on a
 //! function.
 
-use proc_macro2::{Ident, Span};
+use proc_macro2::{Ident, Span, TokenStream};
 use quote::quote;
-use syn::ItemFn;
+use syn::{Expr, ItemFn, Stmt};
 
-use super::{
-    helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler,
-    INTERNAL_RESULT_IDENT,
-};
+use super::{helpers::*, ContractConditionsHandler, INTERNAL_RESULT_IDENT};
 
 impl<'a> ContractConditionsHandler<'a> {
-    /// The complex case. We are the first time a contract is handled on this function, so
-    /// we're responsible for
+    /// Generate initial contract.
     ///
-    /// 1. Generating a name for the check function
-    /// 2. Emitting the original, unchanged item and register the check
-    ///    function on it via attribute
-    /// 3. Renaming our item to the new name
-    /// 4. And (minor point) adding #[allow(dead_code)] and
-    ///    #[allow(unused_variables)] to the check function attributes
+    /// 1. Generating the body for the recursion closure used by contracts.
+    ///    - The recursion closure body will contain the check and replace closure.
     pub fn handle_untouched(&mut self) {
-        // We'll be using this to postfix the generated names for the "check"
-        // and "replace" functions.
-        let item_hash = self.hash.unwrap();
-
-        let original_function_name = self.annotated_fn.sig.ident.clone();
-
-        let check_fn_name =
-            identifier_for_generated_function(&original_function_name, "check", item_hash);
-        let replace_fn_name =
-            identifier_for_generated_function(&original_function_name, "replace", item_hash);
-        let recursion_wrapper_name = identifier_for_generated_function(
-            &original_function_name,
-            "recursion_wrapper",
-            item_hash,
-        );
-
-        // Constructing string literals explicitly here, because `stringify!`
-        // doesn't work. Let's say we have an identifier `check_fn` and we were
-        // to do `quote!(stringify!(check_fn))` to try to have it expand to
-        // `"check_fn"` in the generated code. Then when the next macro parses
-        // this it will *not* see the literal `"check_fn"` as you may expect but
-        // instead the *expression* `stringify!(check_fn)`.
-        let replace_fn_name_str = syn::LitStr::new(&replace_fn_name.to_string(), Span::call_site());
-        let wrapper_fn_name_str =
-            syn::LitStr::new(&self.make_wrapper_name().to_string(), Span::call_site());
-        let recursion_wrapper_name_str =
-            syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site());
+        let replace_name = &self.replace_name;
+        let modifies_name = &self.modify_name;
+        let recursion_name = &self.recursion_name;
+        let check_name = &self.check_name;
+
+        let replace_closure = self.replace_closure();
+        let check_closure = self.check_closure();
+        let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure);
+
+        let span = Span::call_site();
+        let replace_ident = Ident::new(&self.replace_name, span);
+        let check_ident = Ident::new(&self.check_name, span);
+        let recursion_ident = Ident::new(&self.recursion_name, span);
 
         // The order of `attrs` and `kanitool::{checked_with,
         // is_contract_generated}` is important here, because macros are
         // expanded outside in. This way other contract annotations in `attrs`
         // sees those attributes and can use them to determine
         // `function_state`.
-        //
-        // The same care is taken when we emit check and replace functions.
-        // emit the check function.
-        let is_impl_fn = is_probably_impl_fn(&self.annotated_fn);
         let ItemFn { attrs, vis, sig, block } = &self.annotated_fn;
         self.output.extend(quote!(
             #(#attrs)*
-            #[kanitool::checked_with = #recursion_wrapper_name_str]
-            #[kanitool::replaced_with = #replace_fn_name_str]
-            #[kanitool::inner_check = #wrapper_fn_name_str]
+            #[kanitool::recursion_check = #recursion_name]
+            #[kanitool::checked_with = #check_name]
+            #[kanitool::replaced_with = #replace_name]
+            #[kanitool::modifies_wrapper = #modifies_name]
             #vis #sig {
-                #block
+                // Dummy function used to force the compiler to capture the environment.
+                // We cannot call closures inside constant functions.
+                // This function gets replaced by `kani::internal::call_closure`.
+                #[inline(never)]
+                #[kanitool::fn_marker = "kani_register_contract"]
+                const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+                    unreachable!()
+                }
+                // Dummy function that we replace to pick the contract mode.
+                // By default, return ORIGINAL
+                #[inline(never)]
+                #[kanitool::fn_marker = "kani_contract_mode"]
+                const fn kani_contract_mode() -> kani::internal::Mode {
+                    kani::internal::ORIGINAL
+                }
+                let kani_contract_mode = kani_contract_mode();
+                match kani_contract_mode {
+                    kani::internal::RECURSION_CHECK => {
+                        #recursion_closure;
+                        kani_register_contract(#recursion_ident)
+                    }
+                    kani::internal::REPLACE => {
+                        #replace_closure;
+                        kani_register_contract(#replace_ident)
+                    }
+                    kani::internal::SIMPLE_CHECK => {
+                        #check_closure;
+                        kani_register_contract(#check_ident)
+                    }
+                    _ => #block
+                }
             }
         ));
+    }
+
+    /// Handle subsequent contract attributes.
+    ///
+    /// Find the closures added by the initial setup, parse them and expand their body according
+    /// to the attribute being handled.
+    pub fn handle_expanded(&mut self) {
+        let mut annotated_fn = self.annotated_fn.clone();
+        let ItemFn { block, .. } = &mut annotated_fn;
+        let recursion_closure = expect_closure_in_match(&mut block.stmts, "recursion_check");
+        self.expand_recursion(recursion_closure);
 
-        let mut wrapper_sig = sig.clone();
-        wrapper_sig.ident = recursion_wrapper_name;
-        // We use non-constant functions, thus, the wrapper cannot be constant.
-        wrapper_sig.constness = None;
+        let replace_closure = expect_closure_in_match(&mut block.stmts, "replace");
+        self.expand_replace(replace_closure);
 
-        let args = pats_to_idents(&mut wrapper_sig.inputs).collect::<Vec<_>>();
-        let also_args = args.iter();
-        let (call_check, call_replace) = if is_impl_fn {
-            (quote!(Self::#check_fn_name), quote!(Self::#replace_fn_name))
-        } else {
-            (quote!(#check_fn_name), quote!(#replace_fn_name))
-        };
+        let check_closure = expect_closure_in_match(&mut block.stmts, "check");
+        self.expand_check(check_closure);
 
-        let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-        self.output.extend(quote!(
+        self.output.extend(quote!(#annotated_fn));
+    }
+
+    /// Generate the tokens for the recursion closure.
+    fn new_recursion_closure(
+        &self,
+        replace_closure: &TokenStream,
+        check_closure: &TokenStream,
+    ) -> TokenStream {
+        let ItemFn { ref sig, .. } = self.annotated_fn;
+        let output = &sig.output;
+        let span = Span::call_site();
+        let result = Ident::new(INTERNAL_RESULT_IDENT, span);
+        let replace_ident = Ident::new(&self.replace_name, span);
+        let check_ident = Ident::new(&self.check_name, span);
+        let recursion_ident = Ident::new(&self.recursion_name, span);
+
+        quote!(
+            #[kanitool::is_contract_generated(recursion_check)]
             #[allow(dead_code, unused_variables, unused_mut)]
-            #[kanitool::is_contract_generated(recursion_wrapper)]
-            #wrapper_sig {
+            let mut #recursion_ident = || #output
+            {
+                #[kanitool::recursion_tracker]
                 static mut REENTRY: bool = false;
                 if unsafe { REENTRY } {
-                    #call_replace(#(#args),*)
+                    #replace_closure
+                    #replace_ident()
                 } else {
                     unsafe { REENTRY = true };
-                    let #result = #call_check(#(#also_args),*);
+                    #check_closure
+                    let #result = #check_ident();
                     unsafe { REENTRY = false };
                     #result
                 }
-            }
-        ));
+            };
+        )
+    }
+
+    /// Expand an existing recursion closure with the new condition.
+    fn expand_recursion(&self, closure: &mut Stmt) {
+        // TODO: Need to enter if / else. Make this traverse body and return list statements :(
+        let body = closure_body(closure);
+        let stmts = &mut body.block.stmts;
+        let if_reentry = stmts
+            .iter_mut()
+            .find_map(|stmt| {
+                if let Stmt::Expr(Expr::If(if_expr), ..) = stmt { Some(if_expr) } else { None }
+            })
+            .unwrap();
+
+        let replace_closure = expect_closure(&mut if_reentry.then_branch.stmts, "replace");
+        self.expand_replace(replace_closure);
 
-        self.emit_check_function(Some(check_fn_name));
-        self.emit_replace_function(Some(replace_fn_name));
-        self.emit_augmented_modifies_wrapper();
+        let else_branch = if_reentry.else_branch.as_mut().unwrap();
+        let Expr::Block(else_block) = else_branch.1.as_mut() else { unreachable!() };
+        let check_closure = expect_closure(&mut else_block.block.stmts, "check");
+        self.expand_check(check_closure);
     }
 }
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index f804fc70c5f5..69f280ad9335 100644
--- a/library/kani_macros/src/sysroot/contracts/check.rs
+++ b/library/kani_macros/src/sysroot/contracts/check.rs
@@ -5,33 +5,28 @@
 
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::quote;
-use syn::{Expr, FnArg, ItemFn, Token};
+use std::mem;
+use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt};
 
 use super::{
-    helpers::*,
-    shared::{build_ensures, try_as_result_assign_mut},
-    ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
+    helpers::*, shared::build_ensures, ContractConditionsData, ContractConditionsHandler,
+    INTERNAL_RESULT_IDENT,
 };
 
-const WRAPPER_ARG_PREFIX: &str = "_wrapper_arg_";
+const WRAPPER_ARG: &str = "_wrapper_arg";
 
 impl<'a> ContractConditionsHandler<'a> {
     /// Create the body of a check function.
     ///
     /// Wraps the conditions from this attribute around `self.body`.
-    ///
-    /// Mutable because a `modifies` clause may need to extend the inner call to
-    /// the wrapper with new arguments.
-    pub fn make_check_body(&mut self) -> TokenStream2 {
-        let mut inner = self.ensure_bootstrapped_check_body();
+    pub fn make_check_body(&self, mut body_stmts: Vec<Stmt>) -> TokenStream2 {
         let Self { attr_copy, .. } = self;
-
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
-                quote!(
+                quote!({
                     kani::assume(#attr);
-                    #(#inner)*
-                )
+                    #(#body_stmts)*
+                })
             }
             ContractConditionsData::Ensures { attr } => {
                 let (remembers, ensures_clause) = build_ensures(attr);
@@ -42,257 +37,157 @@ impl<'a> ContractConditionsHandler<'a> {
                     kani::assert(#ensures_clause, stringify!(#attr_copy));
                 );
 
-                assert!(matches!(
-                    inner.pop(),
-                    Some(syn::Stmt::Expr(syn::Expr::Path(pexpr), None))
-                        if pexpr.path.get_ident().map_or(false, |id| id == INTERNAL_RESULT_IDENT)
-                ));
-
-                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                quote!(
+                let return_expr = body_stmts.pop();
+                quote!({
                     #remembers
-                    #(#inner)*
+                    #(#body_stmts)*
                     #exec_postconditions
-                    #result
-                )
+                    #return_expr
+                })
             }
             ContractConditionsData::Modifies { attr } => {
-                let wrapper_name = self.make_wrapper_name().to_string();
-
-                let wrapper_args = if let Some(wrapper_call_args) =
-                    inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name))
-                {
-                    let wrapper_args = make_wrapper_idents(
-                        wrapper_call_args.len(),
-                        attr.len(),
-                        WRAPPER_ARG_PREFIX,
-                    );
-                    wrapper_call_args
-                        .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a))));
-                    wrapper_args
+                let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site());
+                let wrapper_tuple = body_stmts.iter_mut().find_map(|stmt| {
+                    if let Stmt::Local(Local {
+                        pat: Pat::Ident(PatIdent { ident, .. }),
+                        init: Some(LocalInit { expr, .. }),
+                        ..
+                    }) = stmt
+                    {
+                        (ident == &wrapper_arg_ident).then_some(expr.as_mut())
+                    } else {
+                        None
+                    }
+                });
+                if let Some(Expr::Tuple(values)) = wrapper_tuple {
+                    values.elems.extend(attr.iter().map(|attr| {
+                        let expr: Expr = parse_quote!(#attr
+                        as *const _);
+                        expr
+                    }));
                 } else {
-                    unreachable!(
-                        "Invariant broken, check function did not contain a call to the wrapper function"
-                    )
-                };
-
-                quote!(
-                    #(let #wrapper_args = unsafe { kani::internal::Pointer::decouple_lifetime(&#attr) };)*
-                    #(#inner)*
-                )
+                    unreachable!("Expected tuple but found `{wrapper_tuple:?}`")
+                }
+                quote!({#(#body_stmts)*})
             }
         }
     }
 
-    /// Get the sequence of statements of the previous check body or create the default one.
-    fn ensure_bootstrapped_check_body(&self) -> Vec<syn::Stmt> {
-        let wrapper_name = self.make_wrapper_name();
+    /// Initialize the list of statements for the check closure body.
+    fn initial_check_stmts(&self) -> Vec<syn::Stmt> {
+        let modifies_ident = Ident::new(&self.modify_name, Span::call_site());
+        let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site());
         let return_type = return_type_to_type(&self.annotated_fn.sig.output);
-        if self.is_first_emit() {
-            let args = exprs_for_args(&self.annotated_fn.sig.inputs);
-            let wrapper_call = if is_probably_impl_fn(self.annotated_fn) {
-                quote!(Self::#wrapper_name)
-            } else {
-                quote!(#wrapper_name)
-            };
-            let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-            syn::parse_quote!(
-                let #result : #return_type = #wrapper_call(#(#args),*);
-                #result
-            )
-        } else {
-            self.annotated_fn.block.stmts.clone()
-        }
+        let mut_recv = self.has_mutable_receiver().then(|| quote!(core::ptr::addr_of!(self),));
+        let redefs = self.arg_redefinitions();
+        let modifies_closure =
+            self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs);
+        let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+        parse_quote!(
+            let #wrapper_arg_ident = (#mut_recv);
+            #modifies_closure
+            let #result : #return_type = #modifies_ident(#wrapper_arg_ident);
+            #result
+        )
     }
 
-    /// Emit the check function into the output stream.
+    /// Generate a token stream that represents the check closure.
     ///
     /// See [`Self::make_check_body`] for the most interesting parts of this
     /// function.
-    pub fn emit_check_function(&mut self, override_function_dent: Option<Ident>) {
-        self.emit_common_header();
-
-        if self.function_state.emit_tag_attr() {
-            // If it's the first time we also emit this marker. Again, order is
-            // important so this happens as the last emitted attribute.
-            self.output.extend(quote!(#[kanitool::is_contract_generated(check)]));
-        }
-        let body = self.make_check_body();
-        let mut sig = self.annotated_fn.sig.clone();
-        // We use non-constant functions, thus, the wrapper cannot be constant.
-        sig.constness = None;
-        if let Some(ident) = override_function_dent {
-            sig.ident = ident;
-        }
-        self.output.extend(quote!(
-            #sig {
-                #body
-            }
-        ))
+    pub fn check_closure(&self) -> TokenStream2 {
+        let check_ident = Ident::new(&self.check_name, Span::call_site());
+        let sig = &self.annotated_fn.sig;
+        let output = &sig.output;
+        let body_stmts = self.initial_check_stmts();
+        let body = self.make_check_body(body_stmts);
+
+        quote!(
+            #[kanitool::is_contract_generated(check)]
+            #[allow(dead_code, unused_variables, unused_mut)]
+            let mut #check_ident = || #output #body;
+        )
     }
 
-    /// Emit a modifies wrapper, possibly augmenting a prior, existing one.
+    /// Expand the check body.
     ///
-    /// We only augment if this clause is a `modifies` clause. Before,
-    /// we annotated the wrapper arguments with `impl kani::Arbitrary`,
-    /// so Rust would infer the proper types for each argument.
-    /// We want to remove the restriction that these arguments must
-    /// implement `kani::Arbitrary` for checking. Now, we annotate each
-    /// argument with a generic type parameter, so the compiler can
-    /// continue inferring the correct types.
-    pub fn emit_augmented_modifies_wrapper(&mut self) {
-        if let ContractConditionsData::Modifies { attr } = &self.condition_type {
-            let wrapper_args = make_wrapper_idents(
-                self.annotated_fn.sig.inputs.len(),
-                attr.len(),
-                WRAPPER_ARG_PREFIX,
-            );
-            // Generate a unique type parameter identifier
-            let type_params = make_wrapper_idents(
-                self.annotated_fn.sig.inputs.len(),
-                attr.len(),
-                "WrapperArgType",
-            );
-            let sig = &mut self.annotated_fn.sig;
-            for (arg, arg_type) in wrapper_args.clone().zip(type_params) {
-                // Add the type parameter to the function signature's generic parameters list
-                let mut bounds: syn::punctuated::Punctuated<syn::TypeParamBound, syn::token::Plus> =
-                    syn::punctuated::Punctuated::new();
-                bounds.push(syn::TypeParamBound::Trait(syn::TraitBound {
-                    paren_token: None,
-                    modifier: syn::TraitBoundModifier::Maybe(Token![?](Span::call_site())),
-                    lifetimes: None,
-                    path: syn::Ident::new("Sized", Span::call_site()).into(),
-                }));
-                sig.generics.params.push(syn::GenericParam::Type(syn::TypeParam {
-                    attrs: vec![],
-                    ident: arg_type.clone(),
-                    colon_token: Some(Token![:](Span::call_site())),
-                    bounds: bounds,
-                    eq_token: None,
-                    default: None,
-                }));
-                let lifetime = syn::Lifetime { apostrophe: Span::call_site(), ident: arg.clone() };
-                sig.inputs.push(FnArg::Typed(syn::PatType {
-                    attrs: vec![],
-                    colon_token: Token![:](Span::call_site()),
-                    pat: Box::new(syn::Pat::Verbatim(quote!(#arg))),
-                    ty: Box::new(syn::parse_quote! { &#arg_type }),
-                }));
-                sig.generics.params.push(syn::GenericParam::Lifetime(syn::LifetimeParam {
-                    lifetime,
-                    colon_token: None,
-                    bounds: Default::default(),
-                    attrs: vec![],
-                }));
-            }
-
-            self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)]))
-        }
-        self.emit_common_header();
-
-        if self.function_state.emit_tag_attr() {
-            // If it's the first time we also emit this marker. Again, order is
-            // important so this happens as the last emitted attribute.
-            self.output.extend(quote!(#[kanitool::is_contract_generated(wrapper)]));
-        }
-
-        let name = self.make_wrapper_name();
-        let ItemFn { vis, sig, block, .. } = self.annotated_fn;
-
-        let mut sig = sig.clone();
-        sig.ident = name;
-        self.output.extend(quote!(
-            #vis #sig #block
+    /// First find the modifies body and expand that. Then expand the rest of the body.
+    pub fn expand_check(&self, closure: &mut Stmt) {
+        let body = closure_body(closure);
+        self.expand_modifies(find_contract_closure(&mut body.block.stmts, "wrapper").expect(
+            &format!("Internal Failure: Expected to find `wrapper` closure, but found none"),
         ));
+        *body = syn::parse2(self.make_check_body(mem::take(&mut body.block.stmts))).unwrap();
     }
-}
-
-/// Try to interpret this statement as `let result : <...> = <wrapper_fn_name>(args ...);` and
-/// return a mutable reference to the parameter list.
-fn try_as_wrapper_call_args<'a>(
-    stmt: &'a mut syn::Stmt,
-    wrapper_fn_name: &str,
-) -> Option<&'a mut syn::punctuated::Punctuated<syn::Expr, syn::token::Comma>> {
-    let syn::LocalInit { diverge: None, expr: init_expr, .. } = try_as_result_assign_mut(stmt)?
-    else {
-        return None;
-    };
-
-    match init_expr.as_mut() {
-        Expr::Call(syn::ExprCall { func: box_func, args, .. }) => match box_func.as_ref() {
-            syn::Expr::Path(syn::ExprPath { qself: None, path, .. })
-                if path.get_ident().map_or(false, |id| id == wrapper_fn_name) =>
-            {
-                Some(args)
-            }
-            _ => None,
-        },
-        _ => None,
-    }
-}
 
-/// Make `num` [`Ident`]s with the names `prefix{i}` with `i` starting at `low` and
-/// increasing by one each time.
-fn make_wrapper_idents(
-    low: usize,
-    num: usize,
-    prefix: &'static str,
-) -> impl Iterator<Item = syn::Ident> + Clone + 'static {
-    (low..).map(move |i| Ident::new(&format!("{prefix}{i}"), Span::mixed_site())).take(num)
-}
-
-#[cfg(test)]
-mod test {
-    macro_rules! detect_impl_fn {
-        ($expect_pass:expr, $($tt:tt)*) => {{
-            let syntax = stringify!($($tt)*);
-            let ast = syn::parse_str(syntax).unwrap();
-            assert!($expect_pass == super::is_probably_impl_fn(&ast),
-                "Incorrect detection.\nExpected is_impl_fun: {}\nInput Expr; {}\nParsed: {:?}",
-                $expect_pass,
-                syntax,
-                ast
-            );
-        }}
+    /// Emit a modifies wrapper. It's only argument is the list of addresses that may be modified.
+    pub fn modifies_closure(
+        &self,
+        output: &ReturnType,
+        body: &Block,
+        redefs: TokenStream2,
+    ) -> TokenStream2 {
+        // Filter receiver
+        let wrapper_ident = Ident::new(WRAPPER_ARG, Span::call_site());
+        let modifies_ident = Ident::new(&self.modify_name, Span::call_site());
+        let stmts = &body.stmts;
+        quote!(
+            #[kanitool::is_contract_generated(wrapper)]
+            #[allow(dead_code, unused_variables, unused_mut)]
+            let mut #modifies_ident = |#wrapper_ident: _| #output {
+                #redefs
+                #(#stmts)*
+            };
+        )
     }
 
-    #[test]
-    fn detect_impl_fn_by_receiver() {
-        detect_impl_fn!(true, fn self_by_ref(&self, u: usize) -> bool {});
-
-        detect_impl_fn!(true, fn self_by_self(self, u: usize) -> bool {});
+    /// Expand the modifies closure if we are handling a modifies attribute. Otherwise, no-op.
+    pub fn expand_modifies(&self, closure_stmt: &mut Stmt) {
+        if matches!(&self.condition_type, ContractConditionsData::Modifies { .. }) {
+            let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure_stmt else {
+                unreachable!()
+            };
+            let Expr::Closure(closure) = expr.as_ref() else { unreachable!() };
+            let Expr::Block(body) = closure.body.as_ref() else { unreachable!() };
+            let stream = self.modifies_closure(&closure.output, &body.block, TokenStream2::new());
+            *closure_stmt = syn::parse2(stream).unwrap();
+        }
     }
 
-    #[test]
-    fn detect_impl_fn_by_self_ty() {
-        detect_impl_fn!(true, fn self_by_construct(u: usize) -> Self {});
-        detect_impl_fn!(true, fn self_by_wrapped_construct(u: usize) -> Arc<Self> {});
-
-        detect_impl_fn!(true, fn self_by_other_arg(u: usize, slf: Self) {});
-
-        detect_impl_fn!(true, fn self_by_other_wrapped_arg(u: usize, slf: Vec<Self>) {})
+    /// Return whether the original function has a mutable receiver.
+    fn has_mutable_receiver(&self) -> bool {
+        let first_arg = self.annotated_fn.sig.inputs.first();
+        first_arg
+            .map(|arg| {
+                matches!(
+                    arg,
+                    FnArg::Receiver(syn::Receiver { mutability: Some(_), reference: None, .. },)
+                )
+            })
+            .unwrap_or(false)
     }
 
-    #[test]
-    fn detect_impl_fn_by_qself() {
-        detect_impl_fn!(
-            true,
-            fn self_by_mention(u: usize) {
-                Self::other(u)
+    /// Generate argument re-definitions for mutable arguments.
+    ///
+    /// This is used so Kani doesn't think that modifying a local argument value is a side effect.
+    fn arg_redefinitions(&self) -> TokenStream2 {
+        let mut result = TokenStream2::new();
+        for (mutability, ident) in self.arg_bindings() {
+            if mutability == MutBinding::Mut {
+                result.extend(quote!(let mut #ident = #ident;))
+            } else {
+                // This would make some replace some temporary variables from error messages.
+                //result.extend(quote!(let #ident = #ident; ))
             }
-        );
+        }
+        result
     }
 
-    #[test]
-    fn detect_no_impl_fn() {
-        detect_impl_fn!(
-            false,
-            fn self_by_mention(u: usize) {
-                let self_name = 18;
-                let self_lit = "self";
-                let self_lit = "Self";
-            }
-        );
+    /// Extract all arguments bindings and their mutability.
+    fn arg_bindings(&self) -> impl Iterator<Item = (MutBinding, &Ident)> {
+        self.annotated_fn.sig.inputs.iter().flat_map(|arg| match arg {
+            FnArg::Receiver(_) => vec![],
+            FnArg::Typed(typed) => pat_to_bindings(typed.pat.as_ref()),
+        })
     }
 }
diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs
index 174f0f9483d7..410c2d971c44 100644
--- a/library/kani_macros/src/sysroot/contracts/helpers.rs
+++ b/library/kani_macros/src/sysroot/contracts/helpers.rs
@@ -5,9 +5,9 @@
 //! specific to Kani and contracts.
 
 use proc_macro2::{Ident, Span};
-use quote::{quote, ToTokens};
 use std::borrow::Cow;
-use syn::{spanned::Spanned, visit::Visit, Expr, FnArg, ItemFn};
+use syn::spanned::Spanned;
+use syn::{parse_quote, Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt};
 
 /// If an explicit return type was provided it is returned, otherwise `()`.
 pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<syn::Type> {
@@ -20,10 +20,16 @@ pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<syn::Type> {
     }
 }
 
-/// Create an expression that reconstructs a struct that was matched in a pattern.
+#[derive(Copy, Clone, Eq, PartialEq)]
+pub enum MutBinding {
+    Mut,
+    NotMut,
+}
+
+/// Extract all local bindings from a given pattern.
 ///
-/// Does not support enums, wildcards, pattern alternatives (`|`), range patterns, or verbatim.
-pub fn pat_to_expr(pat: &syn::Pat) -> Expr {
+/// Does not support range patterns, or verbatim.
+pub fn pat_to_bindings(pat: &syn::Pat) -> Vec<(MutBinding, &Ident)> {
     use syn::Pat;
     let mk_err = |typ| {
         pat.span()
@@ -33,167 +39,90 @@ pub fn pat_to_expr(pat: &syn::Pat) -> Expr {
         unreachable!()
     };
     match pat {
-        Pat::Const(c) => Expr::Const(c.clone()),
-        Pat::Ident(id) => Expr::Verbatim(id.ident.to_token_stream()),
-        Pat::Lit(lit) => Expr::Lit(lit.clone()),
-        Pat::Reference(rf) => Expr::Reference(syn::ExprReference {
-            attrs: vec![],
-            and_token: rf.and_token,
-            mutability: rf.mutability,
-            expr: Box::new(pat_to_expr(&rf.pat)),
-        }),
-        Pat::Tuple(tup) => Expr::Tuple(syn::ExprTuple {
-            attrs: vec![],
-            paren_token: tup.paren_token,
-            elems: tup.elems.iter().map(pat_to_expr).collect(),
-        }),
-        Pat::Slice(slice) => Expr::Reference(syn::ExprReference {
-            attrs: vec![],
-            and_token: syn::Token!(&)(Span::call_site()),
-            mutability: None,
-            expr: Box::new(Expr::Array(syn::ExprArray {
-                attrs: vec![],
-                bracket_token: slice.bracket_token,
-                elems: slice.elems.iter().map(pat_to_expr).collect(),
-            })),
-        }),
-        Pat::Path(pth) => Expr::Path(pth.clone()),
-        Pat::Or(_) => mk_err("or"),
-        Pat::Rest(_) => mk_err("rest"),
-        Pat::Wild(_) => mk_err("wildcard"),
-        Pat::Paren(inner) => pat_to_expr(&inner.pat),
-        Pat::Range(_) => mk_err("range"),
+        Pat::Const(_) => vec![],
+        Pat::Ident(PatIdent { ident, subpat: Some(subpat), mutability, .. }) => {
+            let mut idents = pat_to_bindings(subpat.1.as_ref());
+            idents.push((mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident));
+            idents
+        }
+        Pat::Ident(PatIdent { ident, mutability, .. }) => {
+            vec![(mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)]
+        }
+        Pat::Lit(_) => vec![],
+        Pat::Reference(_) => vec![],
+        Pat::Tuple(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(),
+        Pat::Slice(slice) => slice.elems.iter().flat_map(pat_to_bindings).collect(),
+        Pat::Path(_) => {
+            vec![]
+        }
+        Pat::Or(pat_or) => {
+            // Note: Patterns are not accepted in function arguments.
+            // No matter what, the same bindings must exist in all the patterns.
+            pat_or.cases.first().map(pat_to_bindings).unwrap_or_default()
+        }
+        Pat::Rest(_) => vec![],
+        Pat::Wild(_) => vec![],
+        Pat::Paren(inner) => pat_to_bindings(&inner.pat),
+        Pat::Range(_) => vec![],
         Pat::Struct(strct) => {
-            if strct.rest.is_some() {
-                mk_err("..");
-            }
-            Expr::Struct(syn::ExprStruct {
-                attrs: vec![],
-                path: strct.path.clone(),
-                brace_token: strct.brace_token,
-                dot2_token: None,
-                rest: None,
-                qself: strct.qself.clone(),
-                fields: strct
-                    .fields
-                    .iter()
-                    .map(|field_pat| syn::FieldValue {
-                        attrs: vec![],
-                        member: field_pat.member.clone(),
-                        colon_token: field_pat.colon_token,
-                        expr: pat_to_expr(&field_pat.pat),
-                    })
-                    .collect(),
-            })
+            strct.fields.iter().flat_map(|field_pat| pat_to_bindings(&field_pat.pat)).collect()
         }
         Pat::Verbatim(_) => mk_err("verbatim"),
-        Pat::Type(pt) => pat_to_expr(pt.pat.as_ref()),
-        Pat::TupleStruct(_) => mk_err("tuple struct"),
+        Pat::Type(pt) => pat_to_bindings(pt.pat.as_ref()),
+        Pat::TupleStruct(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(),
         _ => mk_err("unknown"),
     }
 }
 
-/// For each argument create an expression that passes this argument along unmodified.
-///
-/// Reconstructs structs that may have been deconstructed with patterns.
-pub fn exprs_for_args<T>(
-    args: &syn::punctuated::Punctuated<FnArg, T>,
-) -> impl Iterator<Item = Expr> + Clone + '_ {
-    args.iter().map(|arg| match arg {
-        FnArg::Receiver(_) => Expr::Verbatim(quote!(self)),
-        FnArg::Typed(typed) => pat_to_expr(&typed.pat),
+/// Find a closure statement attached with `kanitool::is_contract_generated` attribute.
+pub fn find_contract_closure<'a>(
+    stmts: &'a mut [Stmt],
+    name: &'static str,
+) -> Option<&'a mut Stmt> {
+    stmts.iter_mut().find(|stmt| {
+        if let Stmt::Local(local) = stmt {
+            let ident = Ident::new(name, Span::call_site());
+            let attr: Attribute = parse_quote!(#[kanitool::is_contract_generated(#ident)]);
+            local.attrs.contains(&attr)
+        } else {
+            false
+        }
     })
 }
 
-/// The visitor used by [`is_probably_impl_fn`]. See function documentation for
-/// more information.
-struct SelfDetector(bool);
-
-impl<'ast> Visit<'ast> for SelfDetector {
-    fn visit_ident(&mut self, i: &'ast syn::Ident) {
-        self.0 |= i == &Ident::from(syn::Token![Self](Span::mixed_site()))
-    }
-
-    fn visit_receiver(&mut self, _node: &'ast syn::Receiver) {
-        self.0 = true;
-    }
+/// Find a closure defined in one of the provided statements.
+///
+/// Panic if no closure was found.
+pub fn expect_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt {
+    find_contract_closure(stmts, name)
+        .expect(&format!("Internal Failure: Expected to find `{name}` closure, but found none"))
 }
 
-/// Try to determine if this function is part of an `impl`.
-///
-/// Detects *methods* by the presence of a receiver argument. Heuristically
-/// detects *associated functions* by the use of `Self` anywhere.
-///
-/// Why do we need this? It's because if we want to call this `fn`, or any other
-/// `fn` we generate into the same context we need to use `foo()` or
-/// `Self::foo()` respectively depending on whether this is a plain or
-/// associated function or Rust will complain. For the contract machinery we
-/// need to generate and then call various functions we generate as well as the
-/// original contracted function and so we need to determine how to call them
-/// correctly.
-///
-/// We can only solve this heuristically. The fundamental problem with Rust
-/// macros is that they only see the syntax that's given to them and no other
-/// context. It is however that context (of an `impl` block) that definitively
-/// determines whether the `fn` is a plain function or an associated function.
+/// Find a closure inside a match block.
 ///
-/// The heuristic itself is flawed, but it's the best we can do. For instance
-/// this is perfectly legal
-///
-/// ```
-/// struct S;
-/// impl S {
-///     #[i_want_to_call_you]
-///     fn helper(u: usize) -> bool {
-///       u < 8
-///     }
-///   }
-/// ```
-///
-/// This function would have to be called `S::helper()` but to the
-/// `#[i_want_to_call_you]` attribute this function looks just like a bare
-/// function because it never mentions `self` or `Self`. While this is a rare
-/// case, the following is much more likely and suffers from the same problem,
-/// because we can't know that `Vec == Self`.
-///
-/// ```
-/// impl<T> Vec<T> {
-///   fn new() -> Vec<T> {
-///     Vec { cap: 0, buf: NonNull::dangling() }
-///   }
-/// }
-/// ```
-///
-/// **Side note:** You may be tempted to suggest that we could try and parse
-/// `syn::ImplItemFn` and distinguish that from `syn::ItemFn` to distinguish
-/// associated function from plain functions. However parsing in an attribute
-/// placed on *any* `fn` will always succeed for *both* `syn::ImplItemFn` and
-/// `syn::ItemFn`, thus not letting us distinguish between the two.
-pub fn is_probably_impl_fn(fun: &ItemFn) -> bool {
-    let mut self_detector = SelfDetector(false);
-    self_detector.visit_item_fn(fun);
-    self_detector.0
+/// Panic if no closure was found.
+pub fn expect_closure_in_match<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt {
+    let closure = stmts.iter_mut().find_map(|stmt| {
+        if let Stmt::Expr(Expr::Match(match_expr), ..) = stmt {
+            match_expr.arms.iter_mut().find_map(|arm| {
+                let Expr::Block(block) = arm.body.as_mut() else { return None };
+                find_contract_closure(&mut block.block.stmts, name)
+            })
+        } else {
+            None
+        }
+    });
+    closure.expect(&format!("Internal Failure: Expected to find `{name}` closure, but found none"))
 }
 
-/// Convert every use of a pattern in this signature to a simple, fresh, binding-only
-/// argument ([`syn::PatIdent`]) and return the [`Ident`] that was generated.
-pub fn pats_to_idents<P>(
-    sig: &mut syn::punctuated::Punctuated<syn::FnArg, P>,
-) -> impl Iterator<Item = Ident> + '_ {
-    sig.iter_mut().enumerate().map(|(i, arg)| match arg {
-        syn::FnArg::Receiver(_) => Ident::from(syn::Token![self](Span::call_site())),
-        syn::FnArg::Typed(syn::PatType { pat, .. }) => {
-            let ident = Ident::new(&format!("arg{i}"), Span::mixed_site());
-            *pat.as_mut() = syn::Pat::Ident(syn::PatIdent {
-                attrs: vec![],
-                by_ref: None,
-                mutability: None,
-                ident: ident.clone(),
-                subpat: None,
-            });
-            ident
-        }
-    })
+/// Extract the body of a closure declaration.
+pub fn closure_body(closure: &mut Stmt) -> &mut ExprBlock {
+    let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure else {
+        unreachable!()
+    };
+    let Expr::Closure(closure) = expr.as_mut() else { unreachable!() };
+    let Expr::Block(body) = closure.body.as_mut() else { unreachable!() };
+    body
 }
 
 /// Does the provided path have the same chain of identifiers as `mtch` (match)
@@ -240,35 +169,6 @@ pub fn chunks_by<'a, T, C: Default + Extend<T>>(
     })
 }
 
-/// Create a unique hash for a token stream (basically a [`std::hash::Hash`]
-/// impl for `proc_macro2::TokenStream`).
-fn hash_of_token_stream<H: std::hash::Hasher>(hasher: &mut H, stream: proc_macro2::TokenStream) {
-    use proc_macro2::TokenTree;
-    use std::hash::Hash;
-    for token in stream {
-        match token {
-            TokenTree::Ident(i) => i.hash(hasher),
-            TokenTree::Punct(p) => p.as_char().hash(hasher),
-            TokenTree::Group(g) => {
-                std::mem::discriminant(&g.delimiter()).hash(hasher);
-                hash_of_token_stream(hasher, g.stream());
-            }
-            TokenTree::Literal(lit) => lit.to_string().hash(hasher),
-        }
-    }
-}
-
-/// Hash this `TokenStream` and return an integer that is at most digits
-/// long when hex formatted.
-pub fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 {
-    const SIX_HEX_DIGITS_MASK: u64 = 0x1_000_000;
-    use std::hash::Hasher;
-    let mut hasher = std::collections::hash_map::DefaultHasher::default();
-    hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone()));
-    let long_hash = hasher.finish();
-    long_hash % SIX_HEX_DIGITS_MASK
-}
-
 macro_rules! assert_spanned_err {
     ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => {
         if !$condition {
diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index 73621b2aeec5..50c63173b601 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -4,8 +4,8 @@
 //! Initialization routine for the contract handler
 
 use proc_macro::{Diagnostic, TokenStream};
-use proc_macro2::{Ident, TokenStream as TokenStream2};
-use syn::{spanned::Spanned, ItemFn};
+use proc_macro2::TokenStream as TokenStream2;
+use syn::ItemFn;
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
@@ -19,24 +19,9 @@ impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
     /// Find out if this attribute could be describing a "contract handling"
     /// state and if so return it.
     fn try_from(attribute: &'a syn::Attribute) -> Result<Self, Self::Error> {
-        if let syn::Meta::List(lst) = &attribute.meta {
-            if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) {
-                let ident = syn::parse2::<Ident>(lst.tokens.clone())
-                    .map_err(|e| Some(lst.span().unwrap().error(format!("{e}"))))?;
-                let ident_str = ident.to_string();
-                return match ident_str.as_str() {
-                    "check" => Ok(Self::Check),
-                    "replace" => Ok(Self::Replace),
-                    "wrapper" => Ok(Self::ModifiesWrapper),
-                    _ => {
-                        Err(Some(lst.span().unwrap().error("Expected `check` or `replace` ident")))
-                    }
-                };
-            }
-        }
         if let syn::Meta::NameValue(nv) = &attribute.meta {
             if matches_path(&nv.path, &["kanitool", "checked_with"]) {
-                return Ok(ContractFunctionState::Original);
+                return Ok(ContractFunctionState::Expanded);
             }
         }
         Err(None)
@@ -66,12 +51,10 @@ impl<'a> ContractConditionsHandler<'a> {
     /// Initialize the handler. Constructs the required
     /// [`ContractConditionsType`] depending on `is_requires`.
     pub fn new(
-        function_state: ContractFunctionState,
         is_requires: ContractConditionsType,
         attr: TokenStream,
         annotated_fn: &'a mut ItemFn,
         attr_copy: TokenStream2,
-        hash: Option<u64>,
     ) -> Result<Self, syn::Error> {
         let mut output = TokenStream2::new();
         let condition_type = match is_requires {
@@ -86,7 +69,23 @@ impl<'a> ContractConditionsHandler<'a> {
             }
         };
 
-        Ok(Self { function_state, condition_type, annotated_fn, attr_copy, output, hash })
+        let fn_name = &annotated_fn.sig.ident;
+        let generate_name = |purpose| format!("__kani_{purpose}_{fn_name}");
+        let check_name = generate_name("check");
+        let replace_name = generate_name("replace");
+        let recursion_name = generate_name("recursion_check");
+        let modifies_name = generate_name("modifies");
+
+        Ok(Self {
+            condition_type,
+            annotated_fn,
+            attr_copy,
+            output,
+            check_name,
+            replace_name,
+            recursion_name,
+            modify_name: modifies_name,
+        })
     }
 }
 impl ContractConditionsData {
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index 12a1215de2c7..db5f30131405 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -10,7 +10,7 @@
 //! implements a state machine in order to be able to handle multiple attributes
 //! on the same function correctly.
 //!
-//! ## How the handling for `requires` and `ensures` works.
+//! ## How the handling for `requires`, `modifies`, and `ensures` works.
 //!
 //! Our aim is to generate a "check" function that can be used to verify the
 //! validity of the contract and a "replace" function that can be used as a
@@ -26,102 +26,48 @@
 //! instead of throwing a hard error but this means we cannot detect if a given
 //! function has further contract attributes placed on it during any given
 //! expansion. As a result every expansion needs to leave the code in a valid
-//! state that could be used for all contract functionality but it must alow
+//! state that could be used for all contract functionality, but it must allow
 //! further contract attributes to compose with what was already generated. In
-//! addition we also want to make sure to support non-contract attributes on
+//! addition, we also want to make sure to support non-contract attributes on
 //! functions with contracts.
 //!
-//! To this end we use a state machine. The initial state is an "untouched"
-//! function with possibly multiple contract attributes, none of which have been
-//! expanded. When we expand the first (outermost) `requires` or `ensures`
-//! attribute on such a function we re-emit the function unchanged but we also
-//! generate fresh "check" and "replace" functions that enforce the condition
-//! carried by the attribute currently being expanded.
-//!
-//! We don't copy all attributes from the original function since they may have
-//! unintended consequences for the stubs, such as `inline` or `rustc_diagnostic_item`.
-//!
-//! We also add new marker attributes to
-//! advance the state machine. The "check" function gets a
-//! `kanitool::is_contract_generated(check)` attributes and analogous for
-//! replace. The re-emitted original meanwhile is decorated with
-//! `kanitool::checked_with(name_of_generated_check_function)` and an analogous
-//! `kanittool::replaced_with` attribute also. The next contract attribute that
-//! is expanded will detect the presence of these markers in the attributes of
-//! the item and be able to determine their position in the state machine this
-//! way. If the state is either a "check" or "replace" then the body of the
-//! function is augmented with the additional conditions carried by the macro.
-//! If the state is the "original" function, no changes are performed.
-//!
-//! We place marker attributes at the bottom of the attribute stack (innermost),
-//! otherwise they would not be visible to the future macro expansions.
+//! To this end we generate attributes in a two-phase approach: initial and subsequent expansions.
 //!
-//! Below you can see a graphical rendering where boxes are states and each
-//! arrow represents the expansion of a `requires` or `ensures` macro.
-//!
-//! ```plain
-//!                           │ Start
-//!                           ▼
-//!                     ┌───────────┐
-//!                     │ Untouched │
-//!                     │ Function  │
-//!                     └─────┬─────┘
-//!                           │
-//!            Emit           │  Generate      + Copy Attributes
-//!         ┌─────────────────┴─────┬──────────┬─────────────────┐
-//!         │                       │          │                 │
-//!         │                       │          │                 │
-//!         ▼                       ▼          ▼                 ▼
-//!  ┌──────────┐           ┌───────────┐  ┌───────┐        ┌─────────┐
-//!  │ Original │◄─┐        │ Recursion │  │ Check │◄─┐     │ Replace │◄─┐
-//!  └──┬───────┘  │        │ Wrapper   │  └───┬───┘  │     └────┬────┘  │
-//!     │          │ Ignore └───────────┘      │      │ Augment  │       │ Augment
-//!     └──────────┘                           └──────┘          └───────┘
-//!
-//! │               │       │                                             │
-//! └───────────────┘       └─────────────────────────────────────────────┘
-//!
-//!     Presence of                            Presence of
-//!    "checked_with"                    "is_contract_generated"
-//!
-//!                        State is detected via
-//! ```
+//! The initial expansion modifies the original function to contains all necessary instrumentation
+//! contracts need to be analyzed. It will do the following:
+//! 1. Annotate the function with extra `kanitool` attributes
+//! 2. Generate closures for each contract processing scenario (recursive check, simple check,
+//! replacement, and regular execution).
 //!
-//! All named arguments of the annotated function are unsafely shallow-copied
-//! with the `kani::internal::untracked_deref` function to circumvent the borrow checker
-//! for postconditions. The case where this is relevant is if you want to return
-//! a mutable borrow from the function which means any immutable borrow in the
-//! postcondition would be illegal. We must ensure that those copies are not
-//! dropped (causing a double-free) so after the postconditions we call
-//! `mem::forget` on each copy.
+//! Subsequent expansions will detect the existence of the extra `kanitool` attributes,
+//! and they will only expand the body of the closures generated in the initial phase.
 //!
-//! ## Check function
+//! Note: We place marker attributes at the bottom of the attribute stack (innermost),
+//! otherwise they would not be visible to the future macro expansions.
 //!
-//! Generates a `<fn_name>_check_<fn_hash>` function that assumes preconditions
-//! and asserts postconditions. The check function is also marked as generated
+//! ## Check closure
+//!
+//! Generates a `__kani_<fn_name>_check` closure that assumes preconditions
+//! and asserts postconditions. The check closure is also marked as generated
 //! with the `#[kanitool::is_contract_generated(check)]` attribute.
 //!
 //! Decorates the original function with `#[kanitool::checked_by =
-//! "<fn_name>_check_<fn_hash>"]`.
+//! "__kani_check_<fn_name>"]`.
 //!
 //! The check function is a copy of the original function with preconditions
 //! added before the body and postconditions after as well as injected before
-//! every `return` (see [`PostconditionInjector`]). Attributes on the original
-//! function are also copied to the check function.
+//! every `return` (see [`PostconditionInjector`]). All arguments are captured
+//! by the closure.
 //!
 //! ## Replace Function
 //!
-//! As the mirror to that also generates a `<fn_name>_replace_<fn_hash>`
-//! function that asserts preconditions and assumes postconditions. The replace
+//! As the mirror to that also generates a `__kani_replace_<fn_name>`
+//! closure that asserts preconditions and assumes postconditions. The replace
 //! function is also marked as generated with the
 //! `#[kanitool::is_contract_generated(replace)]` attribute.
 //!
 //! Decorates the original function with `#[kanitool::replaced_by =
-//! "<fn_name>_replace_<fn_hash>"]`.
-//!
-//! The replace function has the same signature as the original function but its
-//! body is replaced by `kani::any()`, which generates a non-deterministic
-//! value.
+//! "__kani_replace_<fn_name>"]`.
 //!
 //! ## Inductive Verification
 //!
@@ -148,26 +94,27 @@
 //! flip the tracker variable back to `false` in case the function is called
 //! more than once in its harness.
 //!
-//! To facilitate all this we generate a `<fn_name>_recursion_wrapper_<fn_hash>`
-//! function with the following shape:
+//! To facilitate all this we generate a `__kani_recursion_check_<fn_name>`
+//! closure with the following shape:
 //!
 //! ```ignored
-//! fn recursion_wrapper_...(fn args ...) {
+//! let __kani_recursion_check_func = || {
 //!     static mut REENTRY: bool = false;
 //!
 //!     if unsafe { REENTRY } {
-//!         call_replace(fn args...)
+//!         let __kani_replace_func = || { /* replace body */ }
+//!         __kani_replace_func()
 //!     } else {
 //!         unsafe { reentry = true };
-//!         let result_kani_internal = call_check(fn args...);
+//!         let __kani_check_func = || { /* check body */ }
+//!         let result_kani_internal = __kani_check_func();
 //!         unsafe { reentry = false };
 //!         result_kani_internal
 //!     }
-//! }
+//! };
 //! ```
 //!
-//! We register this function as `#[kanitool::checked_with =
-//! "recursion_wrapper_..."]` instead of the check function.
+//! We register this closure as `#[kanitool::recursion_check = "__kani_recursion_..."]`.
 //!
 //! # Complete example
 //!
@@ -180,56 +127,106 @@
 //! ```
 //!
 //! Turns into
-//!
 //! ```
-//! #[kanitool::checked_with = "div_recursion_wrapper_965916"]
-//! #[kanitool::replaced_with = "div_replace_965916"]
-//! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor }
-//!
-//! #[allow(dead_code, unused_variables)]
-//! #[kanitool :: is_contract_generated(check)] fn
-//! div_check_b97df2(dividend : u32, divisor : u32) -> u32
-//! {
-//!     let dividend_renamed = kani::internal::untracked_deref(& dividend);
-//!     let divisor_renamed = kani::internal::untracked_deref(& divisor);
-//!     kani::assume(divisor != 0);
-//!     let result_kani_internal : u32 = div_wrapper_b97df2(dividend, divisor);
-//!     kani::assert(
-//!     (| result : & u32 | *result <= dividend_renamed)(& result_kani_internal),
-//!     stringify!(|result : &u32| *result <= dividend));
-//!     std::mem::forget(dividend_renamed);
-//!     std::mem::forget(divisor_renamed);
-//!     result_kani_internal
-//! }
-//!
-//! #[allow(dead_code, unused_variables)]
-//! #[kanitool :: is_contract_generated(replace)] fn
-//! div_replace_b97df2(dividend : u32, divisor : u32) -> u32
-//! {
-//!     let divisor_renamed = kani::internal::untracked_deref(& divisor);
-//!     let dividend_renamed = kani::internal::untracked_deref(& dividend);
-//!     kani::assert(divisor != 0, stringify! (divisor != 0));
-//!     let result_kani_internal : u32 = kani::any_modifies();
-//!     kani::assume(
-//!     (|result : & u32| *result <= dividend_renamed)(&result_kani_internal));
-//!     std::mem::forget(divisor_renamed);
-//!     std::mem::forget(dividend_renamed);
-//!     result_kani_internal
-//! }
-//!
-//! #[allow(dead_code)]
-//! #[allow(unused_variables)]
-//! #[kanitool::is_contract_generated(recursion_wrapper)]
-//! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 {
-//!     static mut REENTRY: bool = false;
-//!
-//!     if unsafe { REENTRY } {
-//!         div_replace_b97df2(dividend, divisor)
-//!     } else {
-//!         unsafe { reentry = true };
-//!         let result_kani_internal = div_check_b97df2(dividend, divisor);
-//!         unsafe { reentry = false };
-//!         result_kani_internal
+//! #[kanitool::recursion_check = "__kani_recursion_check_div"]
+//! #[kanitool::checked_with = "__kani_check_div"]
+//! #[kanitool::replaced_with = "__kani_replace_div"]
+//! #[kanitool::modifies_wrapper = "__kani_modifies_div"]
+//! fn div(dividend: u32, divisor: u32) -> u32 {
+//!     #[inline(never)]
+//!     #[kanitool::fn_marker = "kani_register_contract"]
+//!     pub const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+//!         kani::panic("internal error: entered unreachable code: ")
+//!     }
+//!     let kani_contract_mode = kani::internal::mode();
+//!     match kani_contract_mode {
+//!         kani::internal::RECURSION_CHECK => {
+//!             #[kanitool::is_contract_generated(recursion_check)]
+//!             #[allow(dead_code, unused_variables, unused_mut)]
+//!             let mut __kani_recursion_check_div =
+//!                 || -> u32
+//!                     {
+//!                         #[kanitool::recursion_tracker]
+//!                         static mut REENTRY: bool = false;
+//!                         if unsafe { REENTRY } {
+//!                                 #[kanitool::is_contract_generated(replace)]
+//!                                 #[allow(dead_code, unused_variables, unused_mut)]
+//!                                 let mut __kani_replace_div =
+//!                                     || -> u32
+//!                                         {
+//!                                             kani::assert(divisor != 0, "divisor != 0");
+//!                                             let result_kani_internal: u32 = kani::any_modifies();
+//!                                             kani::assume(kani::internal::apply_closure(|result: &u32|
+//!                                                         *result <= dividend, &result_kani_internal));
+//!                                             result_kani_internal
+//!                                         };
+//!                                 __kani_replace_div()
+//!                             } else {
+//!                                unsafe { REENTRY = true };
+//!                                #[kanitool::is_contract_generated(check)]
+//!                                #[allow(dead_code, unused_variables, unused_mut)]
+//!                                let mut __kani_check_div =
+//!                                    || -> u32
+//!                                        {
+//!                                            kani::assume(divisor != 0);
+//!                                            let _wrapper_arg = ();
+//!                                            #[kanitool::is_contract_generated(wrapper)]
+//!                                            #[allow(dead_code, unused_variables, unused_mut)]
+//!                                            let mut __kani_modifies_div =
+//!                                                |_wrapper_arg| -> u32 { dividend / divisor };
+//!                                            let result_kani_internal: u32 =
+//!                                                __kani_modifies_div(_wrapper_arg);
+//!                                            kani::assert(kani::internal::apply_closure(|result: &u32|
+//!                                                        *result <= dividend, &result_kani_internal),
+//!                                                "|result : &u32| *result <= dividend");
+//!                                            result_kani_internal
+//!                                        };
+//!                                let result_kani_internal = __kani_check_div();
+//!                                unsafe { REENTRY = false };
+//!                                result_kani_internal
+//!                            }
+//!                     };
+//!             ;
+//!             kani_register_contract(__kani_recursion_check_div)
+//!         }
+//!         kani::internal::REPLACE => {
+//!             #[kanitool::is_contract_generated(replace)]
+//!             #[allow(dead_code, unused_variables, unused_mut)]
+//!             let mut __kani_replace_div =
+//!                 || -> u32
+//!                     {
+//!                         kani::assert(divisor != 0, "divisor != 0");
+//!                         let result_kani_internal: u32 = kani::any_modifies();
+//!                         kani::assume(kani::internal::apply_closure(|result: &u32|
+//!                                     *result <= dividend, &result_kani_internal));
+//!                         result_kani_internal
+//!                     };
+//!             ;
+//!             kani_register_contract(__kani_replace_div)
+//!         }
+//!         kani::internal::SIMPLE_CHECK => {
+//!             #[kanitool::is_contract_generated(check)]
+//!             #[allow(dead_code, unused_variables, unused_mut)]
+//!             let mut __kani_check_div =
+//!                 || -> u32
+//!                     {
+//!                         kani::assume(divisor != 0);
+//!                         let _wrapper_arg = ();
+//!                         #[kanitool::is_contract_generated(wrapper)]
+//!                         #[allow(dead_code, unused_variables, unused_mut)]
+//!                         let mut __kani_modifies_div =
+//!                             |_wrapper_arg| -> u32 { dividend / divisor };
+//!                         let result_kani_internal: u32 =
+//!                             __kani_modifies_div(_wrapper_arg);
+//!                         kani::assert(kani::internal::apply_closure(|result: &u32|
+//!                                     *result <= dividend, &result_kani_internal),
+//!                             "|result : &u32| *result <= dividend");
+//!                         result_kani_internal
+//!                     };
+//!             ;
+//!             kani_register_contract(__kani_check_div)
+//!         }
+//!         _ => { dividend / divisor }
 //!     }
 //! }
 //! ```
@@ -264,78 +261,140 @@
 //! This expands to
 //!
 //! ```
-//! #[kanitool::checked_with = "modify_recursion_wrapper_633496"]
-//! #[kanitool::replaced_with = "modify_replace_633496"]
-//! #[kanitool::inner_check = "modify_wrapper_633496"]
-//! fn modify(ptr: &mut u32) { { *ptr += 1; } }
-//! #[allow(dead_code, unused_variables, unused_mut)]
-//! #[kanitool::is_contract_generated(recursion_wrapper)]
-//! fn modify_recursion_wrapper_633496(arg0: &mut u32) {
-//!     static mut REENTRY: bool = false;
-//!     if unsafe { REENTRY } {
-//!             modify_replace_633496(arg0)
-//!         } else {
-//!            unsafe { REENTRY = true };
-//!            let result_kani_internal = modify_check_633496(arg0);
-//!            unsafe { REENTRY = false };
-//!            result_kani_internal
-//!        }
-//! }
-//! #[allow(dead_code, unused_variables, unused_mut)]
-//! #[kanitool::is_contract_generated(check)]
-//! fn modify_check_633496(ptr: &mut u32) {
-//!     let _wrapper_arg_1 =
-//!         unsafe { kani::internal::Pointer::decouple_lifetime(&ptr) };
-//!     kani::assume(*ptr < 100);
-//!     let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
-//!     let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
-//!     let result_kani_internal: () = modify_wrapper_633496(ptr, _wrapper_arg_1);
-//!     kani::assert((|result|
-//!                     (remember_kani_internal_92cc419d8aca576c) ==
-//!                         *ptr)(&result_kani_internal),
-//!         "|result| old(*ptr + 1) == *ptr");
-//!     kani::assert((|result|
-//!                     (remember_kani_internal_92cc419d8aca576c) ==
-//!                         *ptr)(&result_kani_internal),
-//!         "|result| old(*ptr + 1) == *ptr");
-//!     result_kani_internal
-//! }
-//! #[allow(dead_code, unused_variables, unused_mut)]
-//! #[kanitool::is_contract_generated(replace)]
-//! fn modify_replace_633496(ptr: &mut u32) {
-//!     kani::assert(*ptr < 100, "*ptr < 100");
-//!     let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
-//!     let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
-//!     let result_kani_internal: () = kani::any_modifies();
-//!     *unsafe {
-//!                 kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr)))
-//!             } = kani::any_modifies();
-//!     kani::assume((|result|
-//!                     (remember_kani_internal_92cc419d8aca576c) ==
-//!                         *ptr)(&result_kani_internal));
-//!     kani::assume((|result|
-//!                     (remember_kani_internal_92cc419d8aca576c) ==
-//!                         *ptr)(&result_kani_internal));
-//!     result_kani_internal
-//! }
-//! #[kanitool::modifies(_wrapper_arg_1)]
-//! #[allow(dead_code, unused_variables, unused_mut)]
-//! #[kanitool::is_contract_generated(wrapper)]
-//! fn modify_wrapper_633496<'_wrapper_arg_1,
-//!     WrapperArgType1>(ptr: &mut u32, _wrapper_arg_1: &WrapperArgType1) {
-//!     *ptr += 1;
-//! }
-//! #[allow(dead_code)]
-//! #[kanitool::proof_for_contract = "modify"]
-//! fn main() {
-//!     kani::internal::init_contracts();
-//!     { let mut i = kani::any(); modify(&mut i); }
+//! #[kanitool::recursion_check = "__kani_recursion_check_modify"]
+//! #[kanitool::checked_with = "__kani_check_modify"]
+//! #[kanitool::replaced_with = "__kani_replace_modify"]
+//! #[kanitool::modifies_wrapper = "__kani_modifies_modify"]
+//! fn modify(ptr: &mut u32) {
+//!     #[inline(never)]
+//!     #[kanitool::fn_marker = "kani_register_contract"]
+//!     pub const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+//!         kani::panic("internal error: entered unreachable code: ")
+//!     }
+//!     let kani_contract_mode = kani::internal::mode();
+//!     match kani_contract_mode {
+//!         kani::internal::RECURSION_CHECK => {
+//!             #[kanitool::is_contract_generated(recursion_check)]
+//!             #[allow(dead_code, unused_variables, unused_mut)]
+//!             let mut __kani_recursion_check_modify =
+//!                 ||
+//!                     {
+//!                         #[kanitool::recursion_tracker]
+//!                         static mut REENTRY: bool = false;
+//!                         if unsafe { REENTRY } {
+//!                                 #[kanitool::is_contract_generated(replace)]
+//!                                 #[allow(dead_code, unused_variables, unused_mut)]
+//!                                 let mut __kani_replace_modify =
+//!                                     ||
+//!                                         {
+//!                                             kani::assert(*ptr < 100, "*ptr < 100");
+//!                                             let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                                             let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                                             let result_kani_internal: () = kani::any_modifies();
+//!                                             *unsafe {
+//!                                                         kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr)))
+//!                                                     } = kani::any_modifies();
+//!                                             kani::assume(kani::internal::apply_closure(|result|
+//!                                                         (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                                     &result_kani_internal));
+//!                                             kani::assume(kani::internal::apply_closure(|result|
+//!                                                         (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                                     &result_kani_internal));
+//!                                             result_kani_internal
+//!                                         };
+//!                                 __kani_replace_modify()
+//!                             } else {
+//!                                unsafe { REENTRY = true };
+//!                                #[kanitool::is_contract_generated(check)]
+//!                                #[allow(dead_code, unused_variables, unused_mut)]
+//!                                let mut __kani_check_modify =
+//!                                    ||
+//!                                        {
+//!                                            kani::assume(*ptr < 100);
+//!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                                            let _wrapper_arg = (ptr as *const _,);
+//!                                            #[kanitool::is_contract_generated(wrapper)]
+//!                                            #[allow(dead_code, unused_variables, unused_mut)]
+//!                                            let mut __kani_modifies_modify =
+//!                                                |_wrapper_arg| { *ptr += 1; };
+//!                                            let result_kani_internal: () =
+//!                                                __kani_modifies_modify(_wrapper_arg);
+//!                                            kani::assert(kani::internal::apply_closure(|result|
+//!                                                        (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                                    &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                                            kani::assert(kani::internal::apply_closure(|result|
+//!                                                        (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                                    &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                                            result_kani_internal
+//!                                        };
+//!                                let result_kani_internal = __kani_check_modify();
+//!                                unsafe { REENTRY = false };
+//!                                result_kani_internal
+//!                            }
+//!                     };
+//!             ;
+//!             kani_register_contract(__kani_recursion_check_modify)
+//!         }
+//!         kani::internal::REPLACE => {
+//!             #[kanitool::is_contract_generated(replace)]
+//!             #[allow(dead_code, unused_variables, unused_mut)]
+//!             let mut __kani_replace_modify =
+//!                 ||
+//!                     {
+//!                         kani::assert(*ptr < 100, "*ptr < 100");
+//!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                         let result_kani_internal: () = kani::any_modifies();
+//!                         *unsafe {
+//!                                     kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr)))
+//!                                 } = kani::any_modifies();
+//!                         kani::assume(kani::internal::apply_closure(|result|
+//!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                 &result_kani_internal));
+//!                         kani::assume(kani::internal::apply_closure(|result|
+//!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                 &result_kani_internal));
+//!                         result_kani_internal
+//!                     };
+//!             ;
+//!             kani_register_contract(__kani_replace_modify)
+//!         }
+//!         kani::internal::SIMPLE_CHECK => {
+//!             #[kanitool::is_contract_generated(check)]
+//!             #[allow(dead_code, unused_variables, unused_mut)]
+//!             let mut __kani_check_modify =
+//!                 ||
+//!                     {
+//!                         kani::assume(*ptr < 100);
+//!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
+//!                         let _wrapper_arg = (ptr as *const _,);
+//!                         #[kanitool::is_contract_generated(wrapper)]
+//!                         #[allow(dead_code, unused_variables, unused_mut)]
+//!                         let mut __kani_modifies_modify =
+//!                             |_wrapper_arg| { *ptr += 1; };
+//!                         let result_kani_internal: () =
+//!                             __kani_modifies_modify(_wrapper_arg);
+//!                         kani::assert(kani::internal::apply_closure(|result|
+//!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                         kani::assert(kani::internal::apply_closure(|result|
+//!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
+//!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                         result_kani_internal
+//!                     };
+//!             ;
+//!             kani_register_contract(__kani_check_modify)
+//!         }
+//!         _ => { *ptr += 1; }
+//!     }
 //! }
 //! ```
 
 use proc_macro::TokenStream;
 use proc_macro2::{Ident, TokenStream as TokenStream2};
-use quote::{quote, ToTokens};
+use quote::quote;
 use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn};
 
 mod bootstrap;
@@ -397,36 +456,35 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream {
     .into()
 }
 
-/// Classifies the state a function is in in the contract handling pipeline.
+/// Classifies the state a function is in the contract handling pipeline.
 #[derive(Clone, Copy, PartialEq, Eq)]
 enum ContractFunctionState {
-    /// This is the original code, re-emitted from a contract attribute.
-    Original,
+    /// This is the function already expanded with the closures.
+    Expanded,
     /// This is the first time a contract attribute is evaluated on this
     /// function.
     Untouched,
-    /// This is a check function that was generated from a previous evaluation
-    /// of a contract attribute.
-    Check,
-    /// This is a replace function that was generated from a previous evaluation
-    /// of a contract attribute.
-    Replace,
-    ModifiesWrapper,
 }
 
 /// The information needed to generate the bodies of check and replacement
 /// functions that integrate the conditions from this contract attribute.
 struct ContractConditionsHandler<'a> {
-    function_state: ContractFunctionState,
     /// Information specific to the type of contract attribute we're expanding.
     condition_type: ContractConditionsData,
     /// Body of the function this attribute was found on.
-    annotated_fn: &'a mut ItemFn,
+    annotated_fn: &'a ItemFn,
     /// An unparsed, unmodified copy of `attr`, used in the error messages.
     attr_copy: TokenStream2,
     /// The stream to which we should write the generated code.
     output: TokenStream2,
-    hash: Option<u64>,
+    /// The name of the check closure.
+    check_name: String,
+    /// The name of the replace closure.
+    replace_name: String,
+    /// The name of the recursion closure.
+    recursion_name: String,
+    /// The name of the modifies closure.
+    modify_name: String,
 }
 
 /// Which kind of contract attribute are we dealing with?
@@ -460,23 +518,8 @@ impl<'a> ContractConditionsHandler<'a> {
     /// Handle the contract state and return the generated code
     fn dispatch_on(mut self, state: ContractFunctionState) -> TokenStream2 {
         match state {
-            ContractFunctionState::ModifiesWrapper => self.emit_augmented_modifies_wrapper(),
-            ContractFunctionState::Check => {
-                // The easy cases first: If we are on a check or replace function
-                // emit them again but with additional conditions layered on.
-                //
-                // Since we are already on the check function, it will have an
-                // appropriate, unique generated name which we are just going to
-                // pass on.
-                self.emit_check_function(None);
-            }
-            ContractFunctionState::Replace => {
-                // Analogous to above
-                self.emit_replace_function(None);
-            }
-            ContractFunctionState::Original => {
-                unreachable!("Impossible: This is handled via short circuiting earlier.")
-            }
+            // We are on the already expanded function.
+            ContractFunctionState::Expanded => self.handle_expanded(),
             ContractFunctionState::Untouched => self.handle_untouched(),
         }
         self.output
@@ -493,35 +536,9 @@ fn contract_main(
     is_requires: ContractConditionsType,
 ) -> TokenStream {
     let attr_copy = TokenStream2::from(attr.clone());
-
-    let item_stream_clone = item.clone();
     let mut item_fn = parse_macro_input!(item as ItemFn);
-
     let function_state = ContractFunctionState::from_attributes(&item_fn.attrs);
-
-    if matches!(function_state, ContractFunctionState::Original) {
-        // If we're the original function that means we're *not* the first time
-        // that a contract attribute is handled on this function. This means
-        // there must exist a generated check function somewhere onto which the
-        // attributes have been copied and where they will be expanded into more
-        // checks. So we just return ourselves unchanged.
-        //
-        // Since this is the only function state case that doesn't need a
-        // handler to be constructed, we do this match early, separately.
-        return item_fn.into_token_stream().into();
-    }
-
-    let hash = matches!(function_state, ContractFunctionState::Untouched)
-        .then(|| helpers::short_hash_of_token_stream(&item_stream_clone));
-
-    let handler = match ContractConditionsHandler::new(
-        function_state,
-        is_requires,
-        attr,
-        &mut item_fn,
-        attr_copy,
-        hash,
-    ) {
+    let handler = match ContractConditionsHandler::new(is_requires, attr, &mut item_fn, attr_copy) {
         Ok(handler) => handler,
         Err(e) => return e.into_compile_error().into(),
     };
diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs
index 280839dcafca..02ac4a772348 100644
--- a/library/kani_macros/src/sysroot/contracts/replace.rs
+++ b/library/kani_macros/src/sysroot/contracts/replace.rs
@@ -3,8 +3,10 @@
 
 //! Logic used for generating the code that replaces a function with its contract.
 
-use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
+use proc_macro2::{Ident, Span, TokenStream};
 use quote::quote;
+use std::mem;
+use syn::Stmt;
 
 use super::{
     helpers::*,
@@ -13,6 +15,13 @@ use super::{
 };
 
 impl<'a> ContractConditionsHandler<'a> {
+    /// Create initial set of replace statements which is the return havoc.
+    fn initial_replace_stmts(&self) -> Vec<syn::Stmt> {
+        let return_type = return_type_to_type(&self.annotated_fn.sig.output);
+        let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+        vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)]
+    }
+
     /// Split an existing replace body of the form
     ///
     /// ```ignore
@@ -35,26 +44,21 @@ impl<'a> ContractConditionsHandler<'a> {
     /// Such that the first vector contains everything up to and including the single result havoc
     /// and the second one the rest, excluding the return.
     ///
-    /// If this is the first time we're emitting replace we create the return havoc and nothing else.
-    fn ensure_bootstrapped_replace_body(&self) -> (Vec<syn::Stmt>, Vec<syn::Stmt>) {
-        if self.is_first_emit() {
-            let return_type = return_type_to_type(&self.annotated_fn.sig.output);
-            let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-            (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![])
-        } else {
-            let stmts = &self.annotated_fn.block.stmts;
-            let idx = stmts
-                .iter()
-                .enumerate()
-                .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i))
-                .unwrap_or_else(|| {
-                    panic!("ICE: Could not find result let binding in statement sequence")
-                });
-            // We want the result assign statement to end up as the last statement in the first
-            // vector, hence the `+1`.
-            let (before, after) = stmts.split_at(idx + 1);
-            (before.to_vec(), after.split_last().unwrap().1.to_vec())
-        }
+    fn split_replace(&self, mut stmts: Vec<Stmt>) -> (Vec<Stmt>, Vec<Stmt>) {
+        // Pop the return result since we always re-add it.
+        stmts.pop();
+
+        let idx = stmts
+            .iter()
+            .enumerate()
+            .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i))
+            .unwrap_or_else(|| {
+                panic!("ICE: Could not find result let binding in statement sequence")
+            });
+        // We want the result assign statement to end up as the last statement in the first
+        // vector, hence the `+1`.
+        let (before, after) = stmts.split_at_mut(idx + 1);
+        (before.to_vec(), after.to_vec())
     }
 
     /// Create the body of a stub for this contract.
@@ -65,69 +69,65 @@ impl<'a> ContractConditionsHandler<'a> {
     ///
     /// `use_nondet_result` will only be true if this is the first time we are
     /// generating a replace function.
-    fn make_replace_body(&self) -> TokenStream2 {
-        let (before, after) = self.ensure_bootstrapped_replace_body();
-
+    fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 let Self { attr_copy, .. } = self;
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                quote!(
+                quote!({
                     kani::assert(#attr, stringify!(#attr_copy));
                     #(#before)*
                     #(#after)*
                     #result
-                )
+                })
             }
             ContractConditionsData::Ensures { attr } => {
                 let (remembers, ensures_clause) = build_ensures(attr);
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                quote!(
+                quote!({
                     #remembers
                     #(#before)*
                     #(#after)*
                     kani::assume(#ensures_clause);
                     #result
-                )
+                })
             }
             ContractConditionsData::Modifies { attr } => {
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                quote!(
+                quote!({
                     #(#before)*
                     #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)*
                     #(#after)*
                     #result
-                )
+                })
             }
         }
     }
 
-    /// Emit the replace funtion into the output stream.
+    /// Emit the replace function into the output stream.
     ///
-    /// See [`Self::make_replace_body`] for the most interesting parts of this
+    /// See [`Self::expand_replace_body`] for the most interesting parts of this
     /// function.
-    pub fn emit_replace_function(&mut self, override_function_ident: Option<Ident>) {
-        self.emit_common_header();
+    pub fn replace_closure(&self) -> TokenStream {
+        let replace_ident = Ident::new(&self.replace_name, Span::call_site());
+        let sig = &self.annotated_fn.sig;
+        let output = &sig.output;
+        let before = self.initial_replace_stmts();
+        let body = self.expand_replace_body(&before, &vec![]);
 
-        if self.function_state.emit_tag_attr() {
-            // If it's the first time we also emit this marker. Again, order is
-            // important so this happens as the last emitted attribute.
-            self.output.extend(quote!(#[kanitool::is_contract_generated(replace)]));
-        }
-        let mut sig = self.annotated_fn.sig.clone();
-        // We use non-constant functions, thus, the wrapper cannot be constant.
-        sig.constness = None;
-        let body = self.make_replace_body();
-        if let Some(ident) = override_function_ident {
-            sig.ident = ident;
-        }
+        quote!(
+            #[kanitool::is_contract_generated(replace)]
+            #[allow(dead_code, unused_variables, unused_mut)]
+            let mut #replace_ident = || #output #body;
+        )
+    }
 
-        // Finally emit the check function itself.
-        self.output.extend(quote!(
-            #sig {
-                #body
-            }
-        ));
+    /// Expand the `replace` body with the new attribute.
+    pub fn expand_replace(&self, closure: &mut Stmt) {
+        let body = closure_body(closure);
+        let (before, after) = self.split_replace(mem::take(&mut body.block.stmts));
+        let stream = self.expand_replace_body(&before, &after);
+        *body = syn::parse2(stream).unwrap();
     }
 }
 
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index 1ab791d9a117..f189a9f98b0c 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -10,96 +10,11 @@
 use std::collections::HashMap;
 
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
-use quote::{quote, ToTokens};
+use quote::quote;
 use std::hash::{DefaultHasher, Hash, Hasher};
-use syn::{
-    spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path,
-};
+use syn::{spanned::Spanned, visit_mut::VisitMut, Expr, ExprCall, ExprClosure, ExprPath, Path};
 
-use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT};
-
-impl ContractFunctionState {
-    /// Do we need to emit the `is_contract_generated` tag attribute on the
-    /// generated function(s)?
-    pub fn emit_tag_attr(self) -> bool {
-        matches!(self, ContractFunctionState::Untouched)
-    }
-}
-
-impl<'a> ContractConditionsHandler<'a> {
-    pub fn is_first_emit(&self) -> bool {
-        matches!(self.function_state, ContractFunctionState::Untouched)
-    }
-
-    /// Create a new name for the assigns wrapper function *or* get the name of
-    /// the wrapper we must have already generated. This is so that we can
-    /// recognize a call to that wrapper inside the check function.
-    pub fn make_wrapper_name(&self) -> Ident {
-        if let Some(hash) = self.hash {
-            identifier_for_generated_function(&self.annotated_fn.sig.ident, "wrapper", hash)
-        } else {
-            let str_name = self.annotated_fn.sig.ident.to_string();
-            let splits = str_name.rsplitn(3, '_').collect::<Vec<_>>();
-            let [hash, _, base] = splits.as_slice() else {
-                unreachable!("Odd name for function {str_name}, splits were {}", splits.len());
-            };
-
-            Ident::new(&format!("{base}_wrapper_{hash}"), Span::call_site())
-        }
-    }
-
-    /// Emit attributes common to check or replace function into the output
-    /// stream.
-    pub fn emit_common_header(&mut self) {
-        if self.function_state.emit_tag_attr() {
-            self.output.extend(quote!(
-                #[allow(dead_code, unused_variables, unused_mut)]
-            ));
-        }
-
-        #[cfg(not(feature = "no_core"))]
-        self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream));
-
-        // When verifying core and standard library, we need to add an unstable attribute to
-        // the functions generated by Kani.
-        // We also need to filter `rustc_diagnostic_item` attribute.
-        // We should consider a better strategy than just duplicating all attributes.
-        #[cfg(feature = "no_core")]
-        {
-            self.output.extend(quote!(
-                #[unstable(feature="kani", issue="none")]
-            ));
-            self.output.extend(
-                self.annotated_fn
-                    .attrs
-                    .iter()
-                    .filter(|attr| {
-                        if let Some(ident) = attr.path().get_ident() {
-                            let name = ident.to_string();
-                            !name.starts_with("rustc")
-                                && !(name == "stable")
-                                && !(name == "unstable")
-                        } else {
-                            true
-                        }
-                    })
-                    .flat_map(Attribute::to_token_stream),
-            );
-        }
-    }
-}
-
-/// Makes consistent names for a generated function which was created for
-/// `purpose`, from an attribute that decorates `related_function` with the
-/// hash `hash`.
-pub fn identifier_for_generated_function(
-    related_function_name: &Ident,
-    purpose: &str,
-    hash: u64,
-) -> Ident {
-    let identifier = format!("{}_{purpose}_{hash:x}", related_function_name);
-    Ident::new(&identifier, proc_macro2::Span::mixed_site())
-}
+use super::INTERNAL_RESULT_IDENT;
 
 /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`]
 /// since we can't abstract over mutability. Input is the object to match on and the name of the
@@ -147,19 +62,6 @@ pub fn try_as_result_assign(stmt: &syn::Stmt) -> Option<&syn::LocalInit> {
     try_as_result_assign_pat!(stmt, as_ref)
 }
 
-/// Try to parse this statement as `let result : <...> = <init>;` and return a mutable reference to
-/// `init`.
-///
-/// This is the shape of statement we create in check functions (with `init` being a call to check
-/// function with additional pointer arguments for the `modifies` clause) and we need to recognize
-/// it to then edit this call if we find another `modifies` clause and add its additional arguments.
-/// additional conditions.
-///
-/// It's a thin wrapper around [`try_as_result_assign_pat!`] to create a mutable match.
-pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalInit> {
-    try_as_result_assign_pat!(stmt, as_mut)
-}
-
 /// When a `#[kani::ensures(|result|expr)]` is expanded, this function is called on with `build_ensures(|result|expr)`.
 /// This function goes through the expr and extracts out all the `old` expressions and creates a sequence
 /// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;`
diff --git a/tests/cargo-kani/iss2857/Cargo.toml b/tests/cargo-kani/iss2857/Cargo.toml
new file mode 100644
index 000000000000..9f2a72342c19
--- /dev/null
+++ b/tests/cargo-kani/iss2857/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "iss2857"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+sec1 = "0.7.3"
diff --git a/tests/cargo-kani/iss2857/expected b/tests/cargo-kani/iss2857/expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/cargo-kani/iss2857/expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/cargo-kani/iss2857/src/main.rs b/tests/cargo-kani/iss2857/src/main.rs
new file mode 100644
index 000000000000..6a0ed40a006e
--- /dev/null
+++ b/tests/cargo-kani/iss2857/src/main.rs
@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that https://github.com/model-checking/kani/issues/2857 is
+// fixed
+
+#[kani::proof]
+fn check_der_error() {
+    let e = sec1::der::Error::incomplete(sec1::der::Length::ZERO);
+    let _ = format!("{e:?}");
+}
+
+fn main() {}
diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs
index 39c0b0efb54f..2941ec126f3c 100644
--- a/tests/coverage/unreachable/abort/main.rs
+++ b/tests/coverage/unreachable/abort/main.rs
@@ -5,7 +5,7 @@
 
 use std::process;
 
-#[cfg_attr(kani, kani::proof, kani::unwind(5))]
+#[kani::proof]
 fn main() {
     for i in 0..4 {
         if i == 1 {
diff --git a/tests/expected/abort/main.rs b/tests/expected/abort/main.rs
index 9e2f5b7a808c..2941ec126f3c 100644
--- a/tests/expected/abort/main.rs
+++ b/tests/expected/abort/main.rs
@@ -6,7 +6,6 @@
 use std::process;
 
 #[kani::proof]
-#[kani::unwind(5)]
 fn main() {
     for i in 0..4 {
         if i == 1 {
diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected
index 29c61cf9437c..b522716cc001 100644
--- a/tests/expected/function-contract/gcd_rec_replacement_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected
@@ -10,7 +10,7 @@ Frac::check_equals.assertion\
 - Status: SUCCESS\
 - Description: "assertion failed: gcd1 == gcd2"
 
-gcd.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "x != 0 && y != 0"
 
diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected
index 48d3565ef9f1..1c6df8455267 100644
--- a/tests/expected/function-contract/gcd_replacement_pass.expected
+++ b/tests/expected/function-contract/gcd_replacement_pass.expected
@@ -1,4 +1,4 @@
-gcd.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "x != 0 && y != 0"
 
diff --git a/tests/expected/function-contract/modifies/global_fail.expected b/tests/expected/function-contract/modifies/global_fail.expected
index 04e0359ad8a4..a9ecaf689376 100644
--- a/tests/expected/function-contract/modifies/global_fail.expected
+++ b/tests/expected/function-contract/modifies/global_fail.expected
@@ -1,9 +1,9 @@
 assigns\
 - Status: FAILURE\
-- Description: "Check that *var_1 is assignable"\
-in function modify_wrapper
+- Description: "Check that *var_3 is assignable"\
+in function modify
 
-Failed Checks: Check that *var_1 is assignable\
-in modify_wrapper
+Failed Checks: Check that *var_3 is assignable\
+in modify
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected
index 02ce972ef370..d5679f71b74c 100644
--- a/tests/expected/function-contract/modifies/havoc_pass.expected
+++ b/tests/expected/function-contract/modifies/havoc_pass.expected
@@ -1,38 +1,13 @@
-copy_replace.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "equality"\
 in function copy_replace
 
 VERIFICATION:- SUCCESSFUL
 
-copy.assigns\
+.assigns\
 - Status: SUCCESS\
 - Description: "Check that var_4 is assignable"\
 in function copy
 
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that var_3 is assignable"\
-in function copy\
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that var_5 is assignable"\
-in function copy
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that *var_5 is assignable"\
-in function copy\
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that var_7 is assignable"\
-in function copy
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that *var_7 is assignable"\
-in function copy
-
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected
index 02ce972ef370..2ea601aa26a0 100644
--- a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected
+++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected
@@ -5,34 +5,9 @@ in function copy_replace
 
 VERIFICATION:- SUCCESSFUL
 
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that var_4 is assignable"\
-in function copy
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that var_3 is assignable"\
-in function copy\
-
 copy.assigns\
 - Status: SUCCESS\
 - Description: "Check that var_5 is assignable"\
 in function copy
 
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that *var_5 is assignable"\
-in function copy\
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that var_7 is assignable"\
-in function copy
-
-copy.assigns\
-- Status: SUCCESS\
-- Description: "Check that *var_7 is assignable"\
-in function copy
-
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/simple_fail.expected b/tests/expected/function-contract/modifies/simple_fail.expected
index ffaee2293931..269ffa6cc2e2 100644
--- a/tests/expected/function-contract/modifies/simple_fail.expected
+++ b/tests/expected/function-contract/modifies/simple_fail.expected
@@ -1,7 +1,7 @@
 assigns\
 - Status: FAILURE\
-- Description: "Check that *ptr is assignable"
+- Description: "Check that *var_6 is assignable"
 
-Failed Checks: Check that *ptr is assignable
+Failed Checks: Check that *var_6 is assignable
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected
index 4d5407fdd850..4ac03d025558 100644
--- a/tests/expected/function-contract/modifies/vec_pass.expected
+++ b/tests/expected/function-contract/modifies/vec_pass.expected
@@ -1,17 +1,17 @@
-modify.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "v.len() > 0"\
 in function modify
 
-modify_replace.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "element set"\
-in function modify_replace
+in function modify
 
-modify_replace.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "vector tail equality"\
-in function modify_replace
+in function modify
 
 assertion\
 - Status: SUCCESS\
diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs
index ead1c1538b4d..b02cc776d299 100644
--- a/tests/expected/function-contract/pattern_use.rs
+++ b/tests/expected/function-contract/pattern_use.rs
@@ -1,9 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
+//! Test that contracts supports function args with pattern use and mut declaration.
 
 #[kani::ensures(|result : &u32| *result <= dividend)]
-fn div((dividend, divisor): (u32, u32)) -> u32 {
+fn div((mut dividend, divisor): (u32, u32)) -> u32 {
     dividend / divisor
 }
 
diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected
index e1fc78ca462f..7dbc9bae68bd 100644
--- a/tests/expected/function-contract/simple_replace_pass.expected
+++ b/tests/expected/function-contract/simple_replace_pass.expected
@@ -1,4 +1,4 @@
-div.assertion\
+.assertion\
 - Status: SUCCESS\
 - Description: "divisor != 0"
 
diff --git a/tests/expected/function-contract/trait_impls/associated_fn.expected b/tests/expected/function-contract/trait_impls/associated_fn.expected
new file mode 100644
index 000000000000..c6f4c6382f17
--- /dev/null
+++ b/tests/expected/function-contract/trait_impls/associated_fn.expected
@@ -0,0 +1,7 @@
+Checking harness check_foo_b...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_foo_a...
+VERIFICATION:- SUCCESSFUL
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total
diff --git a/tests/expected/function-contract/trait_impls/associated_fn.rs b/tests/expected/function-contract/trait_impls/associated_fn.rs
new file mode 100644
index 000000000000..807469bcc7e3
--- /dev/null
+++ b/tests/expected/function-contract/trait_impls/associated_fn.rs
@@ -0,0 +1,36 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check that we can add contracts to associated functions.
+
+extern crate kani;
+
+#[derive(PartialEq, Eq)]
+enum Foo {
+    A(u8),
+    B(char),
+}
+
+impl Foo {
+    #[kani::ensures(|result| *result == Foo::A(inner))]
+    pub fn new_a(inner: u8) -> Foo {
+        Foo::A(inner)
+    }
+
+    #[kani::requires(char::from_u32(inner).is_some())]
+    #[kani::ensures(|result| matches!(*result, Foo::B(c) if u32::from(c) == inner))]
+    pub unsafe fn new_b(inner: u32) -> Foo {
+        Foo::B(char::from_u32_unchecked(inner))
+    }
+}
+
+#[kani::proof_for_contract(Foo::new_a)]
+fn check_foo_a() {
+    let _ = Foo::new_a(kani::any());
+}
+
+#[kani::proof_for_contract(Foo::new_b)]
+fn check_foo_b() {
+    let _ = unsafe { Foo::new_b(kani::any()) };
+}
diff --git a/tests/expected/function-contract/trait_impls/methods.expected b/tests/expected/function-contract/trait_impls/methods.expected
new file mode 100644
index 000000000000..3906a6fd7a10
--- /dev/null
+++ b/tests/expected/function-contract/trait_impls/methods.expected
@@ -0,0 +1,17 @@
+Checking harness check_next_y...
+
+Status: SUCCESS\
+Description: "|result| result.y == old(self.y) + 1"\
+in function Point::next_y
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_add_x...
+
+Status: SUCCESS\
+Description: "|_| val < 0 || self.x >= old(self.x)"\
+in function Point::add_x
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/function-contract/trait_impls/methods.rs b/tests/expected/function-contract/trait_impls/methods.rs
new file mode 100644
index 000000000000..128710f1436d
--- /dev/null
+++ b/tests/expected/function-contract/trait_impls/methods.rs
@@ -0,0 +1,67 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+// kani-flags: -Zfunction-contracts
+
+//! Check that we can add contract to methods and trait implementations.
+//! Original code taken from:
+//! <https://github.com/rust-lang/rust/blob/c4225812/library/core/src/ops/arith.rs#L1-L35>
+
+use std::ops::Add;
+
+#[derive(Debug, Copy, Clone, PartialEq, kani::Arbitrary)]
+struct Point {
+    x: i32,
+    y: i32,
+}
+
+impl Add for Point {
+    type Output = Self;
+
+    #[kani::requires(!self.x.overflowing_add(other.x).1)]
+    #[kani::requires(!self.y.overflowing_add(other.y).1)]
+    #[kani::ensures(|result| result.x == self.x + other.x)]
+    #[kani::ensures(|result| result.y == self.y + other.y)]
+    fn add(self, other: Self) -> Self {
+        Self { x: self.x + other.x, y: self.y + other.y }
+    }
+}
+
+impl Point {
+    #[kani::modifies(&mut self.x)]
+    #[kani::requires(!self.x.overflowing_add(val).1)]
+    #[kani::ensures(|_| val < 0 || self.x >= old(self.x))]
+    #[kani::ensures(|_| val > 0 || self.x <= old(self.x))]
+    pub fn add_x(&mut self, val: i32) {
+        self.x += val;
+    }
+
+    #[kani::requires(self.y < i32::MAX)]
+    #[kani::ensures(|result| result.y == old(self.y) + 1)]
+    pub fn next_y(mut self) -> Self {
+        self.y += 1;
+        self
+    }
+}
+
+#[kani::proof_for_contract(Point::add_x)]
+fn check_add_x() {
+    let mut p1: Point = kani::any();
+    let _ = p1.add_x(kani::any());
+}
+
+#[kani::proof_for_contract(Point::next_y)]
+fn check_next_y() {
+    let p1: Point = kani::any();
+    let _ = p1.next_y();
+}
+
+/// We should enable this once we add support to specifying trait methods:
+/// <https://github.com/model-checking/kani/issues/1997>
+#[cfg(ignore)]
+#[kani::proof_for_contract(Point::add)]
+fn check_add() {
+    let (p1, p2): (Point, Point) = kani::any();
+    let _ = p1.add(p2);
+}
diff --git a/tests/expected/iterator/main.rs b/tests/expected/iterator/main.rs
index 5cf9402bcb23..b1cb4a89cfbf 100644
--- a/tests/expected/iterator/main.rs
+++ b/tests/expected/iterator/main.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
-#[kani::unwind(4)]
 fn main() {
     let mut z = 1;
     for i in 1..4 {
diff --git a/tests/kani/Coroutines/main.rs b/tests/kani/Coroutines/main.rs
index e059305a6da2..0742d14a6ada 100644
--- a/tests/kani/Coroutines/main.rs
+++ b/tests/kani/Coroutines/main.rs
@@ -10,7 +10,6 @@ use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
-#[kani::unwind(3)]
 fn main() {
     let mut add_one = #[coroutine]
     |mut resume: u8| {
diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs
new file mode 100644
index 000000000000..b485ddf2b32b
--- /dev/null
+++ b/tests/kani/FunctionContracts/fn_params.rs
@@ -0,0 +1,73 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that function contracts work with different type of parameter expressions:
+//! Source: <https://doc.rust-lang.org/reference/items/functions.html>
+//!
+//! Note: See `receiver_contracts` for receiver parameters.
+// kani-flags: -Zfunction-contracts
+
+extern crate kani;
+use std::convert::TryFrom;
+
+/// Dummy structure to check different patterns in contract.
+#[derive(Copy, Clone, PartialEq, Eq, kani::Arbitrary)]
+struct MyStruct {
+    c: char,
+    u: u32,
+}
+
+/// Add contracts to ensure that all parameters are representing the same pair (char, u32).
+#[kani::requires(val.u == second)]
+#[kani::requires(val.u == tup_u)]
+#[kani::requires(Ok(val.c) == char::try_from(first))]
+#[kani::requires(val.c == tup_c)]
+/// We need this extra clause due to <https://github.com/model-checking/kani/issues/3370>.
+#[kani::requires(char::try_from(first).is_ok())]
+pub fn odd_parameters_eq(
+    [first, second]: [u32; 2],
+    (tup_c, tup_u): (char, u32),
+    val @ MyStruct { c: val_c, u }: MyStruct,
+) {
+    assert_eq!(tup_c, char::try_from(first).unwrap());
+    assert_eq!(tup_c, val_c);
+
+    assert_eq!(tup_u, second);
+    assert_eq!(tup_u, u);
+    assert_eq!(val, MyStruct { c: val_c, u });
+}
+
+/// Similar to the function above, but with one requirement missing.
+#[kani::requires(val.u == second)]
+#[kani::requires(val.u == tup_u)]
+#[kani::requires(Ok(val.c) == char::try_from(first))]
+// MISSING: #[kani::requires(val.c == tup_c)]
+// We need this extra clause due to <https://github.com/model-checking/kani/issues/3370>.
+#[kani::requires(char::try_from(first).is_ok())]
+pub fn odd_parameters_eq_wrong(
+    [first, second]: [u32; 2],
+    (tup_c, tup_u): (char, u32),
+    val @ MyStruct { c: val_c, u }: MyStruct,
+) {
+    assert_eq!(tup_c, char::try_from(first).unwrap());
+    assert_eq!(tup_c, val_c);
+
+    assert_eq!(tup_u, second);
+    assert_eq!(tup_u, u);
+    assert_eq!(val, MyStruct { c: val_c, u });
+}
+
+mod verify {
+    use super::*;
+    use kani::Arbitrary;
+
+    #[kani::proof_for_contract(odd_parameters_eq)]
+    fn check_params() {
+        odd_parameters_eq(kani::any(), kani::any(), kani::any())
+    }
+
+    #[kani::should_panic]
+    #[kani::proof_for_contract(odd_parameters_eq_wrong)]
+    fn check_params_wrong() {
+        odd_parameters_eq_wrong(kani::any(), kani::any(), kani::any())
+    }
+}
diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/receiver_contracts.rs
new file mode 100644
index 000000000000..5ca63f1558c3
--- /dev/null
+++ b/tests/kani/FunctionContracts/receiver_contracts.rs
@@ -0,0 +1,155 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that function contracts work with different types of receivers. I.e.:
+//! - &Self (i.e. &self)
+//! - &mut Self (i.e &mut self)
+//! - Box<Self>
+//! - Rc<Self>
+//! - Arc<Self>
+//! - Pin<P> where P is one of the types above
+//! Source: <https://doc.rust-lang.org/reference/items/traits.html?highlight=receiver#object-safety>
+// compile-flags: --edition 2021
+// kani-flags: -Zfunction-contracts
+
+#![feature(rustc_attrs)]
+
+extern crate kani;
+
+use std::boxed::Box;
+use std::pin::Pin;
+use std::rc::Rc;
+use std::sync::Arc;
+
+/// Type representing a valid ASCII value going from `0..=128`.
+#[derive(Copy, Clone, PartialEq, Eq)]
+#[rustc_layout_scalar_valid_range_start(0)]
+#[rustc_layout_scalar_valid_range_end(128)]
+struct CharASCII(u8);
+
+impl kani::Arbitrary for CharASCII {
+    fn any() -> CharASCII {
+        let val = kani::any_where(|inner: &u8| *inner <= 128);
+        unsafe { CharASCII(val) }
+    }
+}
+
+/// This type contains unsafe setter functions with the same contract but different type of
+/// receivers.
+impl CharASCII {
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_val(&mut self, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_mut_ref(self: &mut Self, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_box(mut self: Box<Self>, new_val: u8) {
+        self.as_mut().0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_rc(mut self: Rc<Self>, new_val: u8) {
+        Rc::<_>::get_mut(&mut self).unwrap().0 = new_val
+    }
+
+    /// We cannot specify the counter today which is modified in this function.
+    /// <https://github.com/model-checking/kani/issues/3372>
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_arc(mut self: Arc<Self>, new_val: u8) {
+        Arc::<_>::get_mut(&mut self).unwrap().0 = new_val;
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_pin(mut self: Pin<&mut Self>, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_pin_box(mut self: Pin<Box<Self>>, new_val: u8) {
+        self.0 = new_val
+    }
+}
+
+mod verify {
+    use super::*;
+    use kani::Arbitrary;
+
+    #[kani::proof_for_contract(CharASCII::set_val)]
+    fn check_set_val() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { obj.set_val(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_mut_ref)]
+    fn check_mut_ref() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { obj.set_mut_ref(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_box)]
+    fn check_box() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Box::new(obj).set_box(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_rc)]
+    fn check_rc() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Rc::new(obj).set_rc(new_val) };
+    }
+
+    /// This test currently fails because we cannot specify that the counter will be modified.
+    /// The counter is behind a pointer, but `Arc` only provide access to the data portion of
+    /// the allocation.
+    /// <https://github.com/model-checking/kani/issues/3372>
+    #[cfg(arc_fails)]
+    #[kani::proof_for_contract(CharASCII::set_arc)]
+    fn check_arc() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Arc::new(obj).set_arc(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_pin)]
+    fn check_pin() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Pin::new(&mut obj).set_pin(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_pin_box)]
+    fn check_pin_box() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) };
+    }
+}
diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index 2d5e891f3fdc..75afd77dfa88 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit 2d5e891f3fdc8a88b2d457baceedea5751efaa0d
+Subproject commit 75afd77dfa88d696900f12ee747409ddb208a745