Bad error message using `old` inside abstract blocks
use int.Int
use mach.int.Int63
use ref.Ref
let test (r: ref int63) : int63 =
begin ensures { !r = old !r + 1 }
r := !r + 1;
assert { !r = old !r + 1 }
end;
42
> why3 prove test_old.mlw
File "test_old.mlw", line 5, characters 0-129:
Ident r is not yet declared
The use of old
in the assertion is incorrect (should it?), but the error message is imprecise and the localization spans the whole test
function.