Bad range on single-branch if

[mtzguido]

This fails (rightly, since we are just admitting when x=0) but highlights the body of the then-branch as the error location. Some indication that the problem is in the else-branch would be good.

assume val f : int -> vprop
```pulse
fn test (x:int)
  requires f 0
  ensures f x
{
  ();
  ();
  if (x = 0) {
    ();
    ();
    admit();
    ();
    ();
  }
}
```