I tried this code:

#[no_mangle]
fn main() {
    let x: bool = rmc::nondet();
    if x {
        assert!(1 + 1 == 1);
    }
    assert!(1 + 1 == 3);
}

using the following command line invocation:

rmc test.rs

with RMC version: 2141a76f98d

I expected to see this happen: both assertions fail.

Instead, this happened: it runs forever (CBMC keeps unwinding forever). If I specify an unwinding depth, the unwinding assertion fails:

$ rmc test.rs --cbmc-args --unwind 10
.
.
.

** 3 of 78 failed (2 iterations)
VERIFICATION FAILED
[RMC] info: Verification output shows one or more unwinding failures.
[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.