filipeom

@zapashcanon Could you remind me again what's preventing us from implementing these? We should be able to do this already. I'm just thinking that a memory model that allows us...

> I'm not sure, I think it was not written by me so I think I've never known and simply kept asking about it regularly :D I'll try to have...

@zapashcanon I feel this is good to go :)

> What should we do with this PR? Seems that @filipeom fixed a few things on archlinux since then. I closed that PR because I only extended the `conf-*` to...

This one also seems very promising: [Empc: Effective Path Prioritization for Symbolic Execution with Path Cover](https://www.computer.org/csdl/proceedings-article/sp/2025/223600c772/26hiV7CvoMU)

We can probably benefit a lot from this due to the principle of locality. However, I'm also concerned that you might spend more time merging memories than simply traversing the...

Maybe I misunderstood this, but it seems like a lot of work, we'd essentially be trying to reimplement quantifier elimination for fixed size bitvectors? This makes the analysis inherently undecidable...

> The error is fixed, but a new one occurs, in which `rotate_left` is called with two bit-vectors, not a numeral and a bit-vector (as expected from the smt-lib https://smt-lib.org/logics-all.shtml)....

Also when I run the `rotate_left` test in smtml with alt-ergo I get: ``` $ dune exec -- smtml run test/cli/smt2/test_bitv_rotl.smt2 --solver alt-ergo sat smtml: internal error, uncaught exception: File...

> Did something change in the `Symbols.ml` module? In the mapping I use `Symbol.make` to create the smtml symbol that corresponds to a dolmen/alt-ergo symbol and with this function the...