Unexpected order of verification errors

[fpoli]

While preparing a Prusti demo last week, I found that the order of the reported errors is a bit counter-intuitive. In the second function below, I'd expect the verification error in the second branch of the implementation to be reported before the verification error of a failing postcondition. Since Silicon only reports one error per function, the result is that verification errors jump around the code when working on it with Prusti. I don't think this was always the case. Was it perhaps the result of some Viper change?

use prusti_contracts::*;

#[ensures(false)]
fn good(b: bool) {
    if b {
        assert!(false); // <-- an error is reported here, as expected
    } else {
        assert!(true);
    }
}

#[ensures(false)] // <-- an error is reported here
fn bad(b: bool) {
    if b {
        assert!(true);
    } else {
        assert!(false); // <-- the expected error is this one
    }
}