Expensive copy of a solver

[TomMD]

Z3 has no native way to copy a solver, commonly useful for BFS style tree traversals of contexts of execution. Sometimes solver push/pop suffices and sometimes you just need to copy. This code uses the same operations Leonardo suggested on the topic to cope with Z3's lack.

[waywardmonkeys]

Oops, I see that you linked the place where he said it here in the PR. Please also put it as a comment in the code.

[TomMD]

@waywardmonkeys Done

[waywardmonkeys]

Thanks!