unused variables
When function parameters are not used in spec/code, Why3 emits a warning, which is useful. But it does not for unused variables in the function result. For instance
val f (x: int) : (y:int, z: int)
ensures { true }
emits a warning about x
being unused, but does not complain about y
and z
being ununsed.