Unused axioms introduced by transformations
Motivating example is this small code:
module Test
use ref.Ref
use int.Int
use int.ComputerDivision
let s (x: int)
requires { 0 <= x <= 65535 }
=
let ref y: int = 42 in
assert { [@expl:check 1] 0 <= y * y <= 65535 };
y <- y * y;
assert { [@expl:check 2] x <> 0 };
y <- div y x;
assert { [@expl:check 3] 0 <= y - 100000 <= 65535 };
y <- y - 2 * y;
end
When generating VCs for this file using
why3 prove -P cvc5 test.mlw -a split_goal_right -o out
We can see that there are useless axioms about references in the VC. My guess is these axioms are introduced by transformations that run after the "remove_unused" transformation, or the transformations don't add the necessary "meta" information to attach axioms to symbols. It doesn't seem easy to fix, but maybe I'm wrong. Opinions?