Location of `variant` clause
The location of variant
clauses is at the enclosing loop. It should be at the clause itself (like invariants). In the example below, the loop variant should be at line 9 not 7.
use int.Int
predicate inv (x : int)
let p2 (ref c : int)
=
while c <= 10 do
invariant Ic { inv c }
variant { c }
c <- c + 2
done