Edit: Seems like I misread the documentation... ~~What I was implying is that Kani just can't figure out all of the paths;~~ ~~Consider this example from Kani

Edit: Seems like I misread the documentation... ~~What I was implying is that Kani just can't figure out all of the paths;~~ ~~Consider this example from Kani documentation [1]:~~ fn estimate_size(x: u32) -> u32 { if x < 256 { if x < 128 { return 1; } else { return 3; } } else if x < 1024 { if x > 1022 { panic!("Oh no, a failing corner case!"); } else { return 5; } } else { if x < 2048 { return 7; } else { return 9; } } } ~~Kani is very unlikely to find x=1023.~~ https://model-checking.github.io/kani/tutorial-first-steps.html https://model-checking.github.io/kani/tutorial-first-steps.h...