z3 may generate internal constraints from incremental solves - these get lost during serialization

Howdy, and thank you very much for this awesome piece of work!

I'm building a model, which takes about 50 seconds with a script. I was wondering if it is possible to serialize the solver object and later reload it, and thus shave of most of the static pre-computation time. I tried a naive:
```python
solver = pickle.loads(pickle.dumps(solver, -1))
```
but not only does it take a lot of time, it also fails to compute the correct solution. Without this line everything works fine. Any help appreciated.

and thank you again for your hard and awesome work on claripy (and angr)