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, 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 = vec![kani::any()]; - let mut compare = vec![]; + let v_len : usize = kani::any_where(|i| *i < 4); + let mut v: Vec = 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);