Why3 doesn't extract sequence of statements, only the last one
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).