GitLab

Using today's master branch (commit e55e1d35), I'm running into the following issue.

If I have an .mlw file with a sequence of statements such as the following:

$ cat unitbug.mlw 
module UnitBug
  use import io.StdIO

  let test () =
    print_int 1;
    print_int 2;
    print_int 3

end

... and then I extract it with the following command:

$ why3 extract -D ocaml64 unitbug.mlw -o unitbug.ml

... this is the resulting, extracted file:

$ cat unitbug.ml
let test (us: unit) : unit =
  Pervasives.print_int (Z.to_int (Z.of_string "3"))

Not 100% sure this is a bug, but I expected the extracted file to contain 3 calls to Pervasives.print_int, one for each of the integers (1, 2, 3).