Regression in contract verification from 0.45.0 to 0.46.0

[roypat]

While upgrading the kani version used in Firecracker's CI to 0.46.0 I started noticing one of our harnesses started to fail with a failure that should have been ruled out by the contract's requires clause ("Failed Checks: x > 0 && y > 0", see https://buildkite.com/firecracker/firecracker-pr/builds/9140#018dc0ef-ba26-42b3-8b0f-124c00dad946 for the verification failure).

I was able to minimize the example to the following:

#[kani::requires(x != 0)]
fn function(x: u32) {
    assert_ne!(x, 0);
}

#[kani::proof_for_contract(function)]
fn function_harness() {
    function(kani::any());
}

using the following command line invocation:

cargo kani -p vmm --harness function_harness --enable-unstable -Zfunction-contracts

with Kani version:

I expected to see this happen: The verification passes with kani 0.45.0 (both the firecracker example, and the minimal reproducer), so I was expecting it to also pass in 0.46.0 (although the interesting thing is that 0.45.0 only has 20 checks, while 0.46.0 has over 1000, so maybe there was something wrong in 0.45.0 that got fixed in 0.46.0?)

Instead, this happened: Verification failed (output: https://pastebin.com/EDUN0TVq, sorry it was too long for a github comment :( )