Incorrect handling of QPs in combination with Inhale-Exhale-Assertions

[marcoeilers]

The following program misbehaves in both Silicon and Carbon:

predicate P(r: Int)

method m()
{
  exhale forall i: Int :: i > 0 && i < 123 ==> [i < 400, i > 45 ==> acc(P(i))]
}

In Silicon, this results in an exception in the evaluator.
In Carbon, this program verifies, which it shouldn't.

My guess is that this is actually a problem in the rewriting of QPs in Silver, which is why I'm filing it here; if this turns out to be two separate issues in the backends, this issue should be move.