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;
            }
        }
    }

https://model-checking.github.io/kani/tutorial-first-steps.h...