diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs
index 0e5eccf0cd5a..b1082a8f1f80 100644
--- a/cprover_bindings/src/goto_program/symbol.rs
+++ b/cprover_bindings/src/goto_program/symbol.rs
@@ -386,7 +386,7 @@ impl Symbol {
         self
     }
 
-    /// Set `is_property` to true.
+    /// Set `is_property`.
     pub fn with_is_property(mut self, v: bool) -> Self {
         self.is_property = v;
         self
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index 8eded8b15ea4..94dae51cf0e2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -256,6 +256,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn attach_contract(&mut self, instance: Instance<'tcx>, contract: Vec<Local>) {
         // 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());
         self.set_current_fn(instance);
         let goto_contract = self.as_goto_contract(contract);
         let name = self.current_fn().name();
diff --git a/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs b/tests/expected/function-contract/modifies/vec_pass.rs
similarity index 100%
rename from tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
rename to tests/expected/function-contract/modifies/vec_pass.rs