Memory predicates size computation is incorrect for ADTs with non-sized tail

[celinval]

I tried this code:

extern crate kani;

use kani::mem::{can_dereference, can_write};

#[derive(Clone, Copy, kani::Arbitrary)]
struct Wrapper<T: ?Sized> {
    _size: usize,
    _value: T,
}

mod invalid_access {
    use super::*;
    use std::ptr;

    #[kani::proof]
    pub fn check_wrong_size_should_fail() {
        let mut var: Wrapper<[u64; 4]> = kani::any();
        let fat_ptr: *mut Wrapper<[u64]> = &mut var as *mut _;
        let (thin_ptr, size) = fat_ptr.to_raw_parts();
        let new_size: usize = size + 1;
        let new_ptr: *const [u64] = ptr::from_raw_parts(thin_ptr, new_size);
        // This should fail, however today we don't take the sized members into consideration.
        assert!(can_dereference(new_ptr));
    }

}

using the following command line invocation:

kani -Z mem-predicates wrapper.rs

with Kani version: 0.56.0

I expected to see this happen: Verification failed

Instead, this happened: Verification succeed