title: Incremental solving in Z3 using push command
body: <p>I am using Z3's python api to do some kind of incremental solving. I push constraints to the solver iteratively while checking for unsatisfiability at each step using <code>solver.push()</code> command. I want to understand whether Z3 would use the learned lemmas from previous constraints or the satisfying solution previously obtained when solving with a newly added constraint. I never use the <code>solver.pop()</code> command. Where can I get more details about how the work done in previous iterations is used?</p>