Lost location for function argument
In the following example:
type t = { mutable f : int }
let set (x : t) (v : int) ensures { x.f = v} =
x.f <- v
let g (a : t) =
set a 42;
assert { a.f = 43}
The following task is generated:
[...]
axiom H :
#"bench/ce/bug/../bug.mlw" 8 2 10#
(#"bench/ce/bug/../bug.mlw" 4 36 37# a)
= (#"bench/ce/bug/../bug.mlw" 8 8 10# 42)
[...]
The second location apparently refers to the declaration of field f
. It should not appear here. Only the first location (on line 8), should be kept.