title: How to alter assertions in a solver without having to repeatedly create a new solver in z3 Python API
body: <p>I am currently running into the problem that I create a large SMT formula (that I get from an external source) and I run Solver.check() with it. If the call fails I perform a rewrite on some assertions in the solver using the <code>rewrite(s,f,t)</code> presented <a href="https://stackoverflow.com/questions/15236450/substituting-function-symbols-in-z3-formulas">here</a>.</p>
  <p>Now I am wondering how I can change the assertions in the solver that failed to the new ones obtained after the rewrite. That is assertions that still contain the same function defintions/declarations etc. as the previous solver except with the updated assertions that have been rewritten.</p>
  <p>For example, this is how I would do it now. I wonder if there was a better/more efficient way:</p>
  <pre><code>solver = z3.Solver()
  f = z3.Function(f, z3.Int(),z3.Int())
  solver.add(f(3)== 5)
  solver.check()
  solver.model()
  # I don't like the model let's rewrite
  new_assertions = solver.assertions().rewrite(...)
  new_solver = z3.Solver()
  new_solver.add(new_assertions)
  new_solver.check()
  ...
  </code></pre>