Postcondition failure on a match is reported with a misleading span

[utaal]

#[is_variant]
enum Enum {
    A,
    B,
}


fn test(a: u32) -> (res: Enum)
    ensures (match res {
        Enum::A => a <= 10,
        Enum::B => a > 10, // FAILS
    }) {

    Enum::B
}

results in this error message, which points to the wrong branch of the match, while it should just point to the entire match, I think:

error: postcondition not satisfied
  --> test.rs:24:8
   |
22 |           Enum::A => a <= 10,
   |           ------- failed this postcondition
23 |           Enum::B => a > 10, // FAILS
24 |       }) {
   |  ________^
25 | |
26 | |     Enum::B
27 | | }
   | |_^ at the end of the function body

Originally found by @matthias-brun.

---

• un-ignore test e726297

[utaal]

Moved to #387