On platforms where z3 uses signals to implement timeouts (anything but mac/windows), z3 has a race where it can run into problems when it invokes non-async-signal-safe functions from inside the timout signal handler.
A quick investigation reveals the following problematic calls in on_timeout (smtlib_frontend.cpp):
- various cout methods
I'm not sure that this list is exhaustive.
To be safe, it looks like the signal handler should only use functions from this page:
Here is the linux specific list (it would be better to use the previous list):
One possible fix is to avoid use of clock and use an iostream that calls write instead of going through a FILE* stream. I don't believe it is possible to safely flush cout and cerr from a signal handler.
I am working around the problem by having the calling process invoke alarm(n), and keeping z3 in the dark about the timeout.
Presumably, all scoped_timer events need to be careful about invoking only signal safe functions. I don't know if there actually are other events, or whether they are sticking to safe functions.