title: How incremental solving works in Z3?
body: <p>I have a question regarding how Z3 incrementally solves problems. After reading through some answers here, I found the following:</p>
  
  <ol>
  <li>There are two ways to use Z3 for incremental solving: one is push/pop(stack) mode, the other is using assumptions. <a href="https://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3">Soft/Hard constraints in Z3</a>. </li>
  <li>In stack mode, z3 will forget all learned lemmas in <strong>global</strong> (<em>am I right?</em>) scope even after one local "pop" <a href="https://stackoverflow.com/questions/11245992/efficiency-of-constraint-strengthening-in-smt-solvers">Efficiency of constraint strengthening in SMT solvers</a></li>
  <li>In assumptions mode (I don't know the name, that is the name that comes to my mind), z3 will not simplify some formulas, e.g. value propagation. <a href="https://stackoverflow.com/questions/15009599/z3-behaviour-changing-on-request-for-unsat-core">z3 behaviour changing on request for unsat core</a></li>
  </ol>
  
  <p>I did some comparison (you are welcome to ask for the formulas, they are just too large to put on the rise4fun), but here are my observations: On some formulas, including quantifiers, the assumptions mode is faster. On some formulas with lots of boolean variables (assumptions variables), stack mode is faster than assumptions mode. </p>
  
  <p>Are they implemented for specific purposes? How does incremental solving work in Z3? </p>