What are the benefits of incremental solving?

Question

If "pop" completely destroys context (i.e., learned lemmas) in incremental constraint solving what is the purpose of using "stack mode"?

Rationale: I imagine that if I have just 1 constraint (several conjuncts) it would be preferable to make a single query as opposed to stacking the conjuncts in separate frames onto the stack. If I have more than 1 constraint and decide to use incremental solving with stack, then I would need to (make at least one) pop after querying one constraint and that would presumably "destroy learned lemmas". So, what is the advantage of using incremental solving (with stacks)? What "destroying learned lemmas in pop" really means?

Observation: My experiments indicate this is really beneficial but I find the indication (see smt formulas, there are in total of 500 queries, incremental solving finished in 0.01sec, while noninc. solving finished in 16sec. ) contradictory with this observation.

Answer 1

When push/pop commands are present, Z3 essentially switches to a completely different solver, because it detects that it needs support for incrementality. The incremental solver is usually (but not always) slower on non-incremental queries, but in turn can take advantage of incrementality. See also here: Incremental calls to Z3 on UFBV with and without push calls, Soft/Hard constraints in Z3.

Destroying learned lemmas means that those lemmas that are not valid after pop will be removed. They become invalid because they depend on some constraints within the innermost scope and therefore all the lemmas that follow from them are now invalid. There may be some exceptions, but usually Z3 will try to destroy only invalidated lemmas.

Sorry if there was any confusion that may have arisen from a previous post (Efficiency of constraint strengthening in SMT solvers). That post was not completely clear about which lemmas are removed and has since been updated.