Rafael Sá Menezes

> I still don't understand why you are trying to push code that breaks that pattern. @mikhailramalho Do we have any documentation about how the frontends should work? At the...

> No, but the design is clear After reading and going through a lot of code... it might be. I was asking whether this concept is written somewhere. > This...

> What do you mean by why? It will simply increase the complexity of the codebase unnecessarily. I mean, adding an `if` that solves this entire discussion and solves the...

>@rafaelsamenezes: could you please check our guidelines to see how we could move forward with this situation? There are two relevant parts: 1: > Discussions are encouraged; however, if the...

> could you please rebase this PR? Done

> Would it be possible to expose the sliceable assumptions to the programmer? Yeah, it should be simple.

> It might be that the configuration we set in z3 internally is not great for this particular problem I tried feeding back the formulas for all solver binaries. So...

> the incompatible ones happen because of data types: we replace it with our implementation of data types with the flags tuple-node and tuple-sym. Yeah, thats why I also tried...

I have asked at Z3: https://github.com/Z3Prover/z3/issues/7134#issuecomment-1957258357 > no configuration at the moment. It is all pre-processing. You have a huge set of stores into something that has no effect. Boolector...

Update: z3 team just merged a patch that should fix this issue.