filipeom

Yes, this is the expected the result. The issue here is probably because Owi raises a `Types.Trap "integer overflow"` whereas smtml raises a `IntegerOverflow` exception. So they are not being...

I was thinking of doing something similar to this: Because the primitives for concrete interpreter `trunc_f{32|64}_{s|u}` raise the trap: https://github.com/OCamlPro/owi/blob/aef0bd62b3dd028023a63547928f686c3438c3e5/src/primitives/convert.ml#L22 And, in smtml we raise: https://github.com/formalsec/smtml/blob/a21054602aa9900a2f07d489dba9a313df833b8a/src/eval.ml#L767 I could just change...

Yes, since we're not concretely simplifying `extract`. I will address this once I change the representation of bitvectors in `smtml`.

> * @filipeom, is it expected that Z3 can not handle `sqrt` ? After a quick search online, I believe we would have to use the non-linear solver or something...

Also, using `assert`: ```wast (call $assert (f32.ne (f32.sqrt (local.get $f)) (f32.const 0.0))) ``` Instead of: ```wast (f32.eq (f32.sqrt (call $f32_symbol)) (f32.const 0)) (if (then unreachable)) ``` Dropped execution time to...

Where would printing the solver statistics make more sense? In this example you're doing it after each solver interaction. I was thinking it might be more appropriate at the end...

This is already available in [smtml](https://github.com/formalsec/smtml/blob/main/src/statistics.ml). We would just need to collect solver statistics and merge them at the end

I'll take a look into this, if it's quick I can make a PR to address this

I think it probably breaks hash-consing. I'm exploring a solution where we don't perform hashconsing on integers which should fix this issue :smile:

I think I added `trunc`, `copysign` can probably be implemented without an encoding operator. I can take a look at these when I get more free time :smiley: