From 1fffd53e63de978a8b055ea07e8e41e40ba67638 Mon Sep 17 00:00:00 2001
From: Justus Adam <justbldr@amazon.com>
Date: Mon, 4 Dec 2023 13:59:17 -0800
Subject: [PATCH] Tinkering with the vector test case.

---
 .../{.vec_pass.fixme-2909 => vec_pass.fixme-2909.rs}     | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)
 rename tests/expected/function-contract/modifies/{.vec_pass.fixme-2909 => vec_pass.fixme-2909.rs} (80%)

diff --git a/tests/expected/function-contract/modifies/.vec_pass.fixme-2909 b/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
similarity index 80%
rename from tests/expected/function-contract/modifies/.vec_pass.fixme-2909
rename to tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
index ec39c1d698c2..f2fc4fac3bed 100644
--- a/tests/expected/function-contract/modifies/.vec_pass.fixme-2909
+++ b/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::requires(v.len() > 1)]
+#[kani::requires(v.len() > 0)]
 #[kani::modifies(&v[0])]
 #[kani::ensures(v[0] == src)]
 fn modify(v: &mut Vec<u32>, src: u32) {
@@ -24,9 +24,10 @@ fn main() {
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn modify_replace() {
-    let v_len = kani::any_where(|i| *i < 4);
-    let mut v: Vec<u32> = vec![kani::any()];
-    let mut compare = vec![];
+    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);