Ghost status of record fields not taken into account while typing witness
The following code fails with a
Logical symbol is used in a non-ghost context
error.
function gen: int
type c = { ghost a: int; b: int }
invariant { a = b }
by { a = gen; b = 0 }
If we comment out the witness, the following is accepted:
let f () = { a = gen; b = 0 }