Assert_eq! hits unreachable code

Testing for assert_eq! seems to be hitting unreachable code within weakest_precondition line 80.

It doesn't seem to contain "begin_panic" like our code is expecting.

Current test that doesn't work:

// Should be valid
#[condition(pre="x: i32 == 10i32", post="true")]
fn valid_simple_assertion_eq(x: i32) {
    assert_eq!(x, 10);
}

Navigation Menu