Apologies in advance if this is intended behavior! I couldn't find any previous discussion of this.

I was playing around with Kani and the chrono crate when I encountered "Failed Checks: shift operand is negative". It seems chono's internals use a packed representation for dates that involves left shifting i32 years.

I tried this code in a blank project:

fn main() {}

#[cfg(kani)]
#[kani::proof]
fn proof() {
    let n: i32 = -16;
    let s: u8 = kani::any();
    kani::assume(s == 1);
    let _ = n << s;
}

using the following command line invocation: cargo kani

with Kani version: 0.25.0

I expected to see this happen: My understanding is that left shifting a negative integer is well-defined safe behavior in Rust. I wouldn't expect there to be any failed checks (at least not without an overflow).

Instead, this happened: "Failed Checks: shift operand is negative"