filipeom

I don't think so. I'm also trying to make the current memory model concretize instead of aborting.

Also, if we could adapt the reference interpreter's binary decoder to owi we wouldn't need `wabt` https://github.com/WebAssembly/spec/blob/main/interpreter/binary/decode.ml (but this is probably to much work)

This is super cool! I'd love to see the differences between this branching approach and using ite expressions inside `aux`. Solver-wise, it would probably take much more time, but it...

> Could you clarify what you mean by "ite expressions" ? I mean the ternary operator if-then-else. It would allow us to write the same code in a single expression....

> ... We not only want an implementation that is "locally efficient", meaning that it quickly allows owi-sym to process a single `clz` instruction, we also want one that makes...

I think the issue remains. Even though we can now use `Symbolic_choice_without_memory` elsewhere, we can't use it in `Symbolic_value` because `Symbolic_choice_without_memory` is still defined using `Symbolic_value` (circular dependency). I think...

> Hi @filipeom, I'm also wondering if we could not simply add this in smtml directly? I wanted to have a look at your commit doing this for Z3 but...

> Awwww, OK. So we could simply use that now? 😅 Yeah I believe so. I think only `popcnt` is still missing, but I can add a dumb ite expression...

> I don't know whether the statistics are computed by z3 for all solver objects combined or only for each one (my guess is that it is only for each...

Yes, see https://github.com/OCamlPro/owi/issues/212#issuecomment-2245211214