Function kani::assume

pub fn assume(cond: bool)

Creates an assumption that will be valid after this statement run. Note that the assumption will only be applied for paths that follow the assumption. If the assumption doesn’t hold, the program will exit successfully.

Example:

The code snippet below should never panic.

let i : i32 = kani::any();
kani::assume(i > 10);
if i < 0 {
  panic!("This will never panic");
}

The following code may panic though:

let i : i32 = kani::any();
assert!(i < 0, "This may panic and verification should fail.");
kani::assume(i > 10);