Wildcard patterns on integers are missing assumptions

[Lysxia]

extern crate creusot_contracts;

pub fn f(x: usize) {
    match x {
        1 => assert!(x == 1),
        _ => assert!(x != 1),
    }
}

The assert(x != 1) fails because we generate a default branch with no assumptions.