Confusing coverage result: Uncovered end of block on `if` statement

[adpaco]

We noticed a confusing coverage result in #3119 where, for the code

#[kani::proof]
fn main() {
    let x: u32 = kani::any_where(|val| *val == 5);
    if x > 3 {
        assert!(x > 4);
    }
}

we get the result

Source-based code coverage results:

test.rs (main)\
 * 5:1 - 6:34 COVERED\
 * 7:14 - 9:6 COVERED\
 * 9:6 - 9:7 UNCOVERED

test.rs (main::{closure#0})\
 * 6:40 - 6:49 COVERED

It's not clear to me why this is happening. It's also strange that no region is associated to if x > 3 here. Maybe it's due to an artifact introduced by the closure?