Bad contract for local function inside recursive functions
In this example, Why3 should force f
to have raises {TODO}
in its contract. It should be consistent with the non-recursive case.
use int.Int
exception TODO
let rec e (a : int) : int
ensures { result = a }
raises { TODO -> a = 1 }
=
let f (a : int) : int
=
e 1 in
if a = 1 then
raise TODO
else f 2