Inconsistent behavior when functions with parameters are used as harnesses #1919
Description
Consider the following program:
#[kani::proof]
fn foo(c: char) {
assert!(char::from_u32(c as u32).is_some());
}
#[kani::proof]
fn bar() {
let c = kani::any();
foo(c);
}When run with:
kani entry.rs --harness bar
verification succeeds as expected:
SUMMARY:
** 0 of 67 failed
VERIFICATION:- SUCCESSFUL
However, when run with
kani entry.rs --harness foo
verification fails:
SUMMARY:
** 1 of 11 failed
Failed Checks: assertion failed: char::from_u32(c as u32).is_some()
File: "/home/ubuntu/examples/entry.rs", line 3, in foo
VERIFICATION:- FAILED
Kani version: 4db1b09
This is caused by not applying the validity constraints on char in the foo version.