Divergence error message arrives too early
why3 execute foo.mlw Top.f on
let f () = while false do () done; 42
Execution of Top.f (): type: int result: 42 globals:
but I get
File "foo.mlw", line 2, characters 2-26: this expression may diverge, but this is not stated in the specification
Having to litter the code with
variant before being able to test it is a bit frustrating.