Open celinval opened 3 months ago
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()
}
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).
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
I tried this code:
using the following command line invocation:
with Kani version: 0.53.0-dev
I expected to see this happen: Verification should succeed
Instead, this happened: Verification failed.