This (somewhat reduced) query from the Mariposa benchmark is unknown, and becomes unsat when I comment out the (push 1). Interestingly, this behavior persists even when I run Z3 with combined_solver.ignore_solver1=true, so both versions of the query use the incremental solver.

After some debugging, I have found that the two versions first start diverging due to a missing rewrite on the version without the (push 1) , and that this is because the maximize_ac_sharing rewriter in initialized in its push_scope handler, and not in the constructor. Moving the call to init() into the constructor makes both versions return unknown.

I suppose one could argue that it is reasonable for the solver to behave differently in response to the push, as this is very much the case with the combined solver. But I am still curious about what motivated the choice to initialize maximize_ac_sharing lazily. Is it particularly expensive to initialize?