Attributes before a `let` in a formula are lost
Considering the following program
let f (ref x : int) : unit
ensures { [@xxxx] [@expl:foo] let a = x in a = 0 }
= x <- 0
I would expect to see the attribute [@expl:foo]
and [@xxxx]
in the VC that correspond to the goal for the ensures. But only the attribute [@expl:foo]
is kept, the other is lost during the generation of VC as show by the verbatim:
goal f'vc [@expl:VC for f] : [@hyp_name:Ensures] [@expl:foo] x = 0
It would be better to treat those attributes as the expl ones.