Chalice: Ternary operator in precondition causes Boogie error
description
It looks as if the return type of the ternary operator "e0 ? e1 : e2" doesn't get type-checked properly. When e1 and e2 are not booleans, e.g. ints, the clause "requires e0 ? e1 : e2" causes Boogie to throw type errors.
class Test {
method test()
requires (true ? 0 : 1)
{}
}