Remove cannot locate symbols
Create a session as follows: Load the following file; apply split_vc
on the verification condition; run Alt-Ergo (or any other prover) on the resulting goal; run a bisection on the proof attempt.
use int.Int
let f (x : int) ensures { result = 2 * x } = x + x
The original task contains a useless declaration constant (+)'result'unused : int = result
, which is properly detected as such by the bisection. Thus, it adds a node for the remove
transformation to the session, so as to discard this declaration. The transformation, however, fails to locate that symbol, thus complaining: Symbol '(+)'result'unused' not found, ignored
. The symbol is still present in the final task.
This issue is responsible for hundreds of warning in the multiprecision/mpz_sub
example.