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).