Contract requirement not respected

[celinval]

I tried this code:

// indirect.rs
extern crate kani;

use std::convert::TryFrom;

/// Constrain `val` to be a valid character.
#[kani::requires(u32::from(_char) == val)]
#[kani::ensures(|res| *res == _char)]
pub fn indirect_assumption(val: u32, _char: char) -> char {
    char::try_from(val).unwrap()
}

mod verify {
    use super::*;
    use kani::Arbitrary;

    #[kani::proof_for_contract(indirect_assumption)]
    fn check_indirect_contract() {
        indirect_assumption(kani::any(), kani::any());
    }

    /// This harness that encodes the pre-condition using`kani::assume` succeeds
    #[kani::proof]
    fn check_indirect() {
        let val = kani::any();
        let c = kani::any();
        kani::assume(u32::from(c) == val);
        indirect_assumption(val, c);
    }
}

using the following command line invocation:

kani indirect.rs -Z function-contracts

with Kani version: 0.53.0-dev

I expected to see this happen: Verification should succeed

Instead, this happened: Verification failed.

Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-07-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs", line 1679, in std::result::unwrap_failed

[celinval]

Note that this contract also fails:

#[kani::requires(char::try_from(val) == Ok(_char))]
#[kani::ensures(|res| *res == _char)]
pub fn indirect_assumption(val: u32, _char: char) -> char {
    char::try_from(val).unwrap()
}

but this one succeeds :exploding_head:

#[kani::requires(char::try_from(val).is_ok())] // ** New requires **
#[kani::requires(char::try_from(val) == Ok(_char))]
#[kani::ensures(|res| *res == _char)]
pub fn indirect_assumption(val: u32, _char: char) -> char {
    char::try_from(val).unwrap()
}

[carolynzech]

Verification succeeds in Kani v0.56. git bisect revealed that #3305 fixed the issue. @celinval I can go ahead and close, but I see you have an open PR for fixme tests that references this issue, so wanted to loop you in first. (It doesn't seem like #3305 was meant to fix this problem, so I can do some investigation as to why it did if we think it's worth it).

[celinval]

Do you mind updating the PR and changing the test to no longer be fixme test? We can close this once we merge the PR to avoid any future regression