Multi-threaded Z3?
Question: I'm working on a Python project, where I'm currently trying to speed things up
in some horrible ways: I set up my Z3 solvers, then I fork the process, and
have Z3 perform the solve in the child process and pass a pickle-able
representation of the model back to the parent.

This works great, and represents the first stage of what I'm trying to do: the
parent process is now no longer CPU-bound. The next step is to multi-thread
the parent, so that we can solve multiple Z3 solvers in parallel.

I'm pretty sure I've mutexed away any concurrent accesses of Z3 in the setup
phase, and only one thread should be touching Z3 at any one time. However,
despite this, I'm getting random segfaults in libz3.so. It's important to
note, at this point, that it's not always the _same_ thread that touches Z3 --
the same object (not the solvers themselves, but the expressions) might be
handled by different threads at different times.

My question is, is it possible to multi-thread Z3? There is a brief note here
(<http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html>) saying
"It is not safe to access Z3 objects from multiple threads.", which I guess
would answer my question, but I'm holding out hope that it _means_ to say that
one shouldn't access Z3 from multiple threads _simultaneously_. Another
resource ([Again: Installing Z3 + Python on
Windows](http://stackoverflow.com/questions/14854956/again-
installing-z3-python-on-windows)) states, from Leonardo himself, that "Z3 uses
thread local storage", which, I guess, would sink this whole undertaking, but
a) that answer is from 2012, so maybe things have changed, and b) maybe it
uses thread-local storage for some unrelated stuff?

Anyways, is multi-threading Z3 possible (from Python)? I'd hate to have to
push the setup phase into the child processes...


Answer: Z3 does indeed use thread local storage, but as far as I can see, there is
only one point left in the code where it does so (to track how much memory
each thread is using; in memory_manager.cpp), but that should not be
responsible for the symptoms you see.

Z3 should behave nicely in a multi-threaded setting, if every thread strictly
uses only it's own context object (Z3_context, or in Python class Context).
This means that any object created through one of the Context's can not in any
way interact with any of the other Context's; if that is required, all objects
have to be translated from one Context to another first, e.g. in Python via
functions like translate(...) in class ASTRef.

That said, there surely are some bugs left to fix. My first target when seeing
random segfaults would be the garbage collector, because it might not interact
nicely with Z3's reference counting (which is the case in other APIs). There
is also a known bug that's triggered when many Context objects are created at
the same time (on my todo list though...)

