Dear Ronan, The extract command is to be used to translate WhyML to some programming language (currently OCaml and C).
To get the verification conditions in some format such as smt-lib (I guess that's what you mean by "translate an mlw file into an smt-lib file"), you can use the "why3 prove" command, as follows: why3 prove -P z3 your-file.mlw -o some-dir Note that a *prover* is specified, and not simply a format such as smt-lib, since the translation involves more than the format (logical transformations, built-in symbols, etc.) You'll get a bunch of .smt2 files in some-dir/. Best regards, -- Jean-Christophe On 09/24/2020 04:39 PM, Ronan Saillard wrote: > Hello, > > I would like to use the extraction functionality to translate an mlw > file into an smt-lib file. > > So far I tried the following command: > > why3 extract -D smt-libv2 hello.mlw > > But I get a parsing error from the driver file > > /home/ronan/.opam/4.07.1/lib/why3/plugins/python cannot be loaded: > Format python is already registered > /home/ronan/.opam/4.07.1/lib/why3/plugins/dimacs cannot be loaded: > Format dimacs is already registered > /home/ronan/.opam/4.07.1/lib/why3/plugins/tptp cannot be loaded: Format > tptp is already registered > /home/ronan/.opam/4.07.1/lib/why3/plugins/genequlin cannot be loaded: > Format equlin is already registered > File "/home/ronan/.opam/4.07.1/share/why3/drivers/smt-libv2.gen", line > 19, characters 0-8: > syntax error > > Am I missing something? > > Ronan. > > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
