Catch-all patterns

[phtown]

#[flux::sig(fn(i32[@n]) -> bool[0 < n])]
fn is_positive(x: i32) -> bool {
    match x {
        ..=0 => false,
        1.. => true,
    }
}

Flux is able to verify the function is_positive matches its signature. But if I replace the 1.. in the second match arm with _ then is says the postcondition might not hold. It seems like Flux isn't able to deduce what reaching the second match arm means about x.

I should note that I came up with the above example while trying to isolate the error I got with the following code. My apologies if I've conflated two different issues.

#[flux::refined_by(l: int)]
#[flux::invariant(l >= 0)]
pub enum List {
    #[flux::variant(List[0])]
    Nil,
    #[flux::variant((i32, Box<List[@n]>) -> List[n+1])]
    Cons(i32, Box<List>),
}

impl List {
    #[flux::sig(fn(&List[@l]) -> usize[l])]
    fn len_const_memory(&self) -> usize {
        let mut result = 0;
        let mut this: &Self = self;
        while let Self::Cons(_, tail) = this {
            result += 1;
            this = tail;
        }
        result // error: postcondition might not hold
    }
}