Incremental preprocessing vs. non-incremental solving

[ThomasHaas]

I have a non-incremental smtlib problem over QFBV + QFIDL (smtlib.txt) Z3 solves this in around 3 seconds (UNSAT). If I add a single (push) statement directly before (check-sat), the solving time gets to 10-12 seconds. Running in verbose mode, I see that when Z3 runs incrementally it skips most simplification. I tried to use (set-simplifier) to manually add the missing processing steps but the running time doesn't change (though I'm not sure how to add ctx-simplify?) So now I'm wondering: Is there a way to replicate the non-incremental preprocessing in the incremental solver, or is there a fundamental difference in how the core engine runs afterwards?

In my actual use-case, there will be statements after the push but 99% of the formula will be top-level and I hope to find a way to at least simplify that part.