High memory usage with a simple string vector example #1673
Description
I tried this code:
const N: usize = 9;
#[cfg_attr(kani, kani::proof, kani::unwind(10))]
fn main() {
let mut v: Vec<String> = Vec::new();
for _i in 0..N {
v.push(String::from("ABC"));
}
assert_eq!(v.len(), N);
let index: usize = kani::any();
kani::assume(index < v.len());
let x = &v[index];
assert_eq!(*x, "ABC");
}using the following command line invocation:
kani push_string.rs
with Kani version: 0fa9ee3
This finished in ~8.5 minutes and used ~23 GB of memory:
Although at some point, memory usage went up to ~27 GB.
If I bump N to 10 (and unwind to 11), it runs out of memory (>32 GB).