lifting-bits
Investigate simplification using Z3's `ctx-solver-simplify`
In rellic-decomp we currently employ a our own Z3 simplifiers made of various Z3 tactics. This is done here and here.
However Z3 also contains ctx-solver-simplify which is a heavyweight solver-based simplifier. It's brief description by it's author is here. We have avoided using this simplifier in rellic::Z3CondSimplify since it's been too aggressive at times, leading to degradation in performance of rellic::CondBasedRefine, rellic::ReachBasedRefine, etc.
Given that we sometimes struggle with if and while conditions that are too complex we should investigate using ctx-solver-simplify again.
Also it is quite possible that that the reason why ctx-solver-simplify is too aggressive is because the translation from C AST to Z3 expression isn't done properly. The translation code lives in Z3ConvVisitor.(h|cpp).