We could improve our final query performance by doing slicing

The final `Expr` can contain parts that have nothing to do with the query. This means that the solver will be given & compute things that are utterly useless from a UNSAT perspective, and could be queried if needed for a counterexample (e.g. a variable in the function call that is never touched). So what we need to do is to do slicing [1] -- figuring out what is actually needed by the final query. A simple taint analysis could do the trick.

If you think about it, this would be SOMEWHAT similar to what Certora is doing with the weakest precondition calculation. I think it would simulate SOME of it. Maybe a poor man's version of it, but I don't think it would be a bad idea. Could significantly improve performance I think?

[1] https://en.wikipedia.org/wiki/Program_slicing