Unparsable output from Boogie

[tillarnold]

I have found two examples that verify with silicon but when using carbon result in An internal error occurred. Found an unparsable output from Boogie.

The error messages differ in the two cases.

Case 1

method x()
    ensures (forall q: Bool :: id(q == q))
{}

function id(a : Bool): Bool { a }

Results in an error of equality is not allowed in triggers.

Case 2

method test()
  ensures (forall q: Int :: id(let x == (q) in (true)))
  {}

function id(b: Bool): Bool  {
    b
}

Results in an error of trigger must mention all quantified variables.