Wrong encoding of signed discriminants in pure code

[fpoli]

The following program is encoded to an assert false (more precisely, assert (2 == 1) ? true : false), but it should be assert true:

use std::cmp::Ordering;
use prusti_contracts::prusti_assert;

fn main() {
    prusti_assert!(matches!(Ordering::Greater, Ordering::Greater)); // Prusti raises a verification error, but it shouldn't
}

This is an unsoundness; it's enough to flip the boolean:

use std::cmp::Ordering;
use prusti_contracts::prusti_assert;

fn main() {
    prusti_assert!(!matches!(Ordering::Greater, Ordering::Greater)); // Prusti doesn't report a verification error, but it should
}

The following is encoded correctly, so the issue seems to be related to the prusti_assert! procedural macro:

use std::cmp::Ordering;
use prusti_contracts::prusti_assert;

fn main() {
    assert!(matches!(Ordering::Greater, Ordering::Greater)); //  Prusti doesn't report a verification error, as expected
}

[fpoli]

The MIR encoding of matches!(Ordering::Greater, Ordering::Greater):

MIR


So, Prusti is encoding the discriminant of Ordering::Greater as 2, while the true arm of the match (on the right) expected the discriminant of Ordering::Greater to be 1.