I tried this code:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// rmc-verify-fail

pub fn main() {
    for i in 0..4 {
        if i == 1 {
            panic!("This comes first");
        }
        if i == 2 {
            panic!("This should never happen");
        }
    }
}

using the following command line invocation:

rmc loop.rs

I expected to see this happen: The first assertion should fail but the second one should be unreachable. The panic call should abort the execution in the second iteration of the loop.

Instead, this happened: Both assertions fail. The trace for the second assertion includes the first panic call.

Note that the same behavior happens if we replace the panic!() statement by process::abort().