Unsound termination check
Consider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
let main (_: unit) : unit = f ()