Niche optimization encoding is broken

[celinval]

I tried this code:

#[kani::proof]
fn check_i8() {
    let v1: i8 = -10;
    let n1 = NonZeroI8::new(v1);
    assert!(n1.is_some());
}

using the following command line invocation:

kani test.rs

with Kani version:

I expected to see this happen: Harness should succeed.

Instead, this happened: Verification failed.

SUMMARY:
 ** 1 of 8 failed
Failed Checks: assertion failed: n1.is_some()
File: "/kani/tests/kani/Invariants/check_nonzero.rs", line 25, in check_i8

VERIFICATION:- FAILED

Note that we do have a test that should be checking this (tests/kani/Invariants/check_nonzero.rs), and if you run it manually, you can see that the test is failing. However, the test uses kani::expect_fail() which is also broken. So the tests actually succeeds in our CI.

[celinval]

It looks like we are failing when the value is negative. I wonder if this regression was introduced by: d0b74ca

[celinval]

That said, the following harness only fails in the second assert:

#[kani::proof]
fn check_i8() {
    let v1: i8 = -10;
    let n1 = unsafe { NonZeroI8::new_unchecked(v1) };

    assert_eq!(n1.get(), v1);
    assert!(Some(n1).is_some());
}

[celinval]

d0b74ca

It predates this commit.

[danielsn]

I figured out what's wrong: we're doing a signed comparison against 0, when we need unsigned.