Divergence error message arrives too early
When running why3 execute foo.mlw Top.f
on
let f () =
while false do () done;
42
I expect
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 diverges
or variant
before being able to test it is a bit frustrating.