Warning without a span

[mohammadfawaz]

The following emits a warning without a span:

predicate Foo { 
    var b: bool;
    if true {
        constraint 1 < 2;
    } 
}

Warning:

Warning: constraint is always `true`
   ╭─[:1:1]
   │
 1 │ <none>
   │ │
   │ ╰─ this constraint always evaluates to `true`
   │
   │ Help: if this is intentional, consider removing this constraint

That's because during flattening, we first convert the if statement to:

    constraint (!true || (1 < 2));

and I guess the span get lost in the process.

[otrho]

It might be worth auditing the code for anywhere we use empty_span() to see if in fact a proper span could be found.