Does Z3 discard lemmas after pop() in incremental mode?

3
votes

When using Z3 in incremental mode, does the solver discard all lemmas after performing a pop() operation?

In 2012, Leonardo de Moura affirmed that Z3 in fact discards lemmas after a pop() [1]. However my benchmarks using Z3 4.3.1 do not show statistically significant performance slowdown of a check-sat after a pop().

[1] Efficiency of constraint strengthening in SMT solvers

1
z3smt

1 Answers

2
votes

Yes, upon pop() Z3 discards all the lemmas that were derived within the scope(s) of that pop and its corresponding push.

Sorry about the confusion, the old post was not completely clear about that and has since been updated.