Eric Patrizio

Same on my small example, it works with `After`, thanks!

Command line example : ```console dune exec owi -- sym ./test/sym/table.wat --no-stop-at-failure --print-solver-statistics ``` Display : ```console (decisions 3) (propagations 62) (final checks 1) (mk clause 98) (num checks 1)...

> I'm wondering if we would like to merge this with the `--profiling` flag ? ```console dune exec owi -- sym ./test/sym/table.wat --no-stop-at-failure --profiling ``` displays : ```text Exec module...

> Some messages are still wrong (see #262) but it's getting better Indeed. Full compliance seems hard to achieve : our implementation approach is different and the choice of message...

For information, in the PR #194 mentioned above, float operations `div` and `mul` have been deactivated (they are very time-consuming - ~ 25 sec !) It's the same for float...

For now, statistics are displayed after `Solver.get_model` call.

After #151 PR, instructions have been implemented. However, it remains (non-exhaustive, in actual scope) : - `f32.copysign` https://github.com/OCamlPro/owi/blob/4e3a35f73a74b826f0fcfc25f0551296ca110de1/test/sym/binop_f32.wat#L39 - `f64.copysign` https://github.com/OCamlPro/owi/blob/4e3a35f73a74b826f0fcfc25f0551296ca110de1/test/sym/binop_f64.wat#L39 - `f32.trunc` https://github.com/OCamlPro/owi/blob/4e3a35f73a74b826f0fcfc25f0551296ca110de1/test/sym/unop_f32.wat#L35 - `f64.trunc` https://github.com/OCamlPro/owi/blob/4e3a35f73a74b826f0fcfc25f0551296ca110de1/test/sym/unop_f64.wat#L35

Thanks for the detailed answer. My first feeling: in one file, all the modules are independent (> separate interpretations). But your feeling makes sense! What's the best approach ? Cc....