Attributes in variant clause with custom order are lost
This issue is a follow-up on #587 (closed).
use int.Int
predicate my_order (x y : int) =
x < y /\ x >= 0
use export why3.WellFounded.WellFounded
lemma my_order_wf : well_founded my_order
meta "vc:proved_wf" predicate my_order, lemma my_order_wf
let rec f () =
let ref x = 10 in
while x > 0 do
variant { [@variant:x] x with my_order }
x <- x - 1
done
In this case, the goal generated for the VC corresponding to the variant clause is does not contains the attributes [@variant:x]
as shown above:
goal f'vc [@expl:VC for f] :
[@vc:annotation] [@expl:loop variant decrease]
my_order ([@hyp_name:Variant] [@variant:x] x)
([@hyp_name:Variant] [@variant:x] x1)