Kani miss overflow when computing size_of_val

[celinval]

I tried this code:

#[kani::proof]
pub fn check_size_of_overflows() {
    let var:  [u64; 4] = kani::any();
    let fat_ptr: *const [u64] = &var as *const _;
    let (thin_ptr, size) = fat_ptr.to_raw_parts();
    let new_size: usize = kani::any();
    let new_ptr:  *const [u64] = ptr::from_raw_parts(thin_ptr, new_size);
    if let Some(expected_size) = new_size.checked_mul(size_of::<u64>()) {
        assert_eq!(unsafe { size_of_val_raw(new_ptr) }, expected_size);
    } else {
        // Expect UB detection
        let _should_ub = unsafe { size_of_val_raw(new_ptr) };
    }
}

using the following command line invocation:

kani slice.rs

with Kani version: 0.56.0

I expected to see this happen: UB should be detected

Instead, this happened: Verification succeed