Failed Checks: Check that ptr is freeable #3864

struct Foo {
    vec: Vec<u8>
}

#[kani::requires (e <10)]
#[kani::modifies(f)]
fn foo_push (f: &mut Foo, e: u8) {
    f.vec.push(e);
}


#[kani::proof_for_contract(foo_push)]
fn proof_foo_push_contract () {
    const FOO_SIZE: usize = 2;
    let bytes: [u8; FOO_SIZE] = kani::any();
    let mut f = Foo { vec: bytes.to_vec() };
    let e : u8 = kani::any();
    foo_push(&mut f, e);
}

#[kani::proof]
#[kani::unwind(5)]
fn proof_foo_push_no_contract () {
    const FOO_SIZE: usize = 2;
    let bytes: [u8; FOO_SIZE] = kani::any();
    let mut f = Foo { vec: bytes.to_vec() };
    let e : u8 = kani::any();
    kani::assume(e < 10);
    foo_push(&mut f, e);
}