SMT SAT model: handle memories

[totorigolo]

The current Python wrapper doesn't handle memory expressions. I'm opening this issue to keep track of this :slightly_smiling_face:

I wanted to use it to help me debug my WPs, but of course I cannot. Anyway, the Python wrapper still prints the model on stderr in a "Python format" which I find easier to read that Z3's output in SMT-LIB 2.0.

[andreaslindner]

Yes, you are right! And we should be able to add this relatively easy by using w2n and combintheory's update in your wrapper.py file I believe. (If I'm not missing something now.)

[totorigolo]

Removed "good first issue" because what we want in HOL4 isn't trivial.