Pointer sub() operation is giving spurious overflow check error

[celinval]

I tried this code:

#[kani::proof]
fn check_thin_ptr() {
    let array = [0, 1, 2, 3, 4, 5, 6];
    let second_ptr: *const i32 = &array[3];
    unsafe {
        let before = second_ptr.sub(1);
        assert_eq!(*before, 2);
    }
}

using the following command line invocation:

kani <test_file>

with Kani version:

I expected to see this happen: Verification succeed.

Instead, this happened: It fails with the following message:

SUMMARY:
 ** 1 of 9 failed
Failed Checks: attempt to compute offset which would overflow
 File: "rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 295, in std::ptr::const_ptr::<impl *const T>::offset

VERIFICATION:- FAILED