diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected
new file mode 100644
index 000000000000..7ba6fc1af589
--- /dev/null
+++ b/tests/expected/function-contract/modifies/vec_pass.expected
@@ -0,0 +1,20 @@
+modify.assertion\
+- Status: SUCCESS\
+- Description: "v.len() > 0"\
+in function modify
+
+modify_replace.assertion\
+- Status: SUCCESS\
+- Description: "element set"\
+in function modify_replace
+
+modify_replace.assertion\
+- Status: SUCCESS\
+- Description: "vector tail equality"\
+in function modify_replace
+
+assertion\
+- Status: SUCCESS\
+- Description: "v [0] == src"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass.rs
index b904dcea6d72..1e40a2a08eb7 100644
--- a/tests/expected/function-contract/modifies/vec_pass.rs
+++ b/tests/expected/function-contract/modifies/vec_pass.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()];