Can't fully prove a non-terminating function anymore (regression, since it was possible in why3 0.88)
In Why3 0.88, the following program
module M
let f "W:diverges:N" (x:int) = while true do () done
end
was provable. The equivalent code for Why3 1.0
let f [@W:diverges:N] (x:int) = while true do () done
is not provable anymore, since a new VC is generated whose goal is false
Adding the diverges
clause is not a viable solution in my context which is porting jessie to why3 1.0: the attribute W:diverges:N
was used in any case, the function being non-terminating or not.
And unfortunately adding diverges
on a terminating function is an error and not a warning.