diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index 359f296433fb..8eded8b15ea4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -260,33 +260,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let goto_contract = self.as_goto_contract(contract);
         let name = self.current_fn().name();
 
-        // CBMC has two ways of attaching the contract and it seems the
-        // difference is whether dfcc is used or not. With dfcc it's stored in
-        // `contract::<fn name>`, otherwise directly on the type of the
-        // function.
-        //
-        // Actually the issue sees to haver been something else and ataching to
-        // the symbol directly seems ot also work if dfcc is used.
-        let create_separate_contract_sym = false;
-
-        let contract_target_name = if create_separate_contract_sym {
-            let contract_sym_name = format!("contract::{}", name);
-            self.ensure(&contract_sym_name, |ctx, fname| {
-                Symbol::function(
-                    fname,
-                    ctx.fn_typ(),
-                    None,
-                    format!("contract::{}", ctx.current_fn().readable_name()),
-                    ctx.codegen_span(&ctx.current_fn().mir().span),
-                )
-                .with_is_property(true)
-            });
-            contract_sym_name
-        } else {
-            name
-        };
-
-        self.symbol_table.attach_contract(contract_target_name, goto_contract);
+        self.symbol_table.attach_contract(name, goto_contract);
         self.reset_current_fn()
     }
 
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 509a1e291eca..d82c7760360f 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -58,7 +58,16 @@ enum KaniAttributeKind {
     /// 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.
+    ///
+    /// 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,
 }
 
diff --git a/tests/expected/function-contract/modifies/expr_pass.rs b/tests/expected/function-contract/modifies/expr_pass.rs
index 18fa5ff76897..d76e20126c45 100644
--- a/tests/expected/function-contract/modifies/expr_pass.rs
+++ b/tests/expected/function-contract/modifies/expr_pass.rs
@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
+// Test that a modifies clause works when a (function call)
+// expression is provided
+
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
 fn modify(ptr: &mut Box<u32>) {
diff --git a/tests/expected/function-contract/modifies/expr_replace_fail.rs b/tests/expected/function-contract/modifies/expr_replace_fail.rs
index 63ac2d8a8027..b5677a817243 100644
--- a/tests/expected/function-contract/modifies/expr_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_fail.rs
@@ -2,6 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
+// Tests that providing the "modifies" clause havocks the pointer such
+// that the increment can no longer be observed (in the absence of an
+// "ensures" clause)
+
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
 fn modify(ptr: &mut Box<u32>) {
diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.rs b/tests/expected/function-contract/modifies/expr_replace_pass.rs
index 187b97c3cefb..8be1ef2cbaee 100644
--- a/tests/expected/function-contract/modifies/expr_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_pass.rs
@@ -4,7 +4,7 @@
 
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
-#[kani::ensures(*ptr.as_ref() == prior + 1)]
+#[kani::ensures(**ptr == prior + 1)]
 fn modify(ptr: &mut Box<u32>, prior: u32) {
     *ptr.as_mut() += 1;
 }
diff --git a/tests/expected/function-contract/modifies/havoc_pass.rs b/tests/expected/function-contract/modifies/havoc_pass.rs
index 13f3b1d057c9..aa5bcada1a26 100644
--- a/tests/expected/function-contract/modifies/havoc_pass.rs
+++ b/tests/expected/function-contract/modifies/havoc_pass.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-// These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still
 #[kani::modifies(dst)]
 #[kani::ensures(*dst == src)]
 fn copy(src: u32, dst: &mut u32) {
diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
index 13f3b1d057c9..dc5f370179e5 100644
--- a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
+++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
@@ -3,8 +3,8 @@
 // kani-flags: -Zfunction-contracts
 
 // These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still
-#[kani::modifies(dst)]
 #[kani::ensures(*dst == src)]
+#[kani::modifies(dst)]
 fn copy(src: u32, dst: &mut u32) {
     *dst = src;
 }
diff --git a/tests/expected/function-contract/modifies/simple_fail.rs b/tests/expected/function-contract/modifies/simple_fail.rs
index 26517526038b..8d1b16e9a976 100644
--- a/tests/expected/function-contract/modifies/simple_fail.rs
+++ b/tests/expected/function-contract/modifies/simple_fail.rs
@@ -9,7 +9,6 @@ fn modify(ptr: &mut u32) {
 
 #[kani::proof_for_contract(modify)]
 fn main() {
-    let _ = Box::new(());
     let mut i = kani::any();
     modify(&mut i);
 }
diff --git a/tests/expected/function-contract/modifies/simple_pass.rs b/tests/expected/function-contract/modifies/simple_pass.rs
index f76f1a6a6c22..3c90ef8c789f 100644
--- a/tests/expected/function-contract/modifies/simple_pass.rs
+++ b/tests/expected/function-contract/modifies/simple_pass.rs
@@ -10,7 +10,6 @@ fn modify(ptr: &mut u32) {
 
 #[kani::proof_for_contract(modify)]
 fn main() {
-    let _ = Box::new(());
     let mut i = kani::any();
     modify(&mut i);
 }
diff --git a/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs b/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
index f2fc4fac3bed..b904dcea6d72 100644
--- a/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
+++ b/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
@@ -9,8 +9,8 @@ fn modify(v: &mut Vec<u32>, src: u32) {
     v[0] = src
 }
 
-#[kani::unwind(10)]
-#[kani::proof_for_contract(modify)]
+//#[kani::unwind(10)]
+//#[kani::proof_for_contract(modify)]
 fn main() {
     let v_len = kani::any_where(|i| *i < 4);
     let mut v: Vec<u32> = vec![kani::any()];
@@ -24,23 +24,11 @@ fn main() {
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn modify_replace() {
-    let v_len : usize = kani::any_where(|i| *i < 4);
-    let mut v: Vec<u32> = Vec::with_capacity(v_len + 1);
-    v.push(kani::any());
-    let mut compare = Vec::with_capacity(v_len);
-    for _ in 0..v_len {
-        let elem = kani::any();
-        v.push(elem);
-        compare.push(elem);
-    }
+    let v_len = kani::any_where(|i| *i < 4 && *i > 0);
+    let mut v: Vec<u32> = vec![kani::any(); v_len].to_vec();
+    let compare = v[1..].to_vec();
     let src = kani::any();
     modify(&mut v, src);
-    kani::assert(
-        v[0] == src,
-        "element set"
-    );
-    kani::assert(
-        v[1..] == compare[..],
-        "vector tail equality"
-    );
+    kani::assert(v[0] == src, "element set");
+    kani::assert(compare == v[1..v_len], "vector tail equality");
 }