Hichem R. A.
Hichem R. A.
The culprit is `dobble.c`, simply running htop reveals it since it seems to take over 5 minutes or loop forever, the slowdown is reproducible with: ``` dune exec -- owi...
Should be fixed by: https://github.com/formalsec/smtml/pull/347
So I ran some benchmarks (z3, 30 second timeout with [d6fabb2](https://github.com/OCamlPro/owi/commit/d6fabb2d47393cd418deba7ceaa5332e2463fe41)) and here are the results. Current version: ``` | Nothing | Reached | Timeout | Other | Killed |...
Ok! Here's the output of the diff tool: ``` tool1 had 672 reached and tool2 had 671 reached tool1 had 501 timeout and tool2 had 503 timeout tool1 had 001...
> Which one of tool1/tool2 was with ite/without ite? Tool1 one is the default behavior (with ite) and tool2 is without. > You can open a PR with the flag...
Since the time difference between the two is not very large (altough tool2 two seems slightly faster) and since tool1 reaches 672 goals while tool2 reaches 671 ones, it does...
Yes that would be useful! Notably when there is a crash/error that happens either in smtml or the in smt-solver, having the smt file or a file in the smtml...
Should be fixed by https://github.com/formalsec/smtml/pull/349
Type error seems to have been fixed, but with 135, the same error as in https://github.com/OCamlPro/owi/issues/638 seems to occur
Should be fixed by https://github.com/formalsec/smtml/pull/347