Is frequently calling simplify expensive?

[momvart]

Hi there. I'm using Z3 for expression building in symbolic execution.

Expression simplifications are vital and effective for symbolic execution to avoid creating large expression trees. An example is a counter in a loop that is incremented in each iteration, where instead of having an expression x + 1 + 1 + 1 + ... you would like to keep x + C.

Therefore, I want to call simplify whenever an expression is built. However, I'm concerned about its cost. To my understanding it recurses over all subexpressions for rewriting which can be a concern when the expression is not simplifiable. In this specific context, rewriting only for the top most expression should be enough as the subexpressions would be previously simplified.

So:

1. Is my assumption true that repetitive calls to simplify cause redundant checks?
2. Is there a way to simplify only up to a level? I've tried max_steps but that doesn't seem to be meant for this purpose.