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
• exit
• clock
  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:
http://pubs.opengroup.org/onlinepubs/009696899/functions/xsh_chap02_04.html#tag_02_04

Here is the linux specific list (it would be better to use the previous list):
http://www.kernel.org/doc/man-pages/online/pages/man7/signal.7.html

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.

clock_t end_time = clock();
if ((g_solver || g_cmd_context) && g_display_statistics) {
    std::cout.flush();
    std::cerr.flush();
    if (g_solver) {
        g_solver->display_statistics();
        memory::display_max_usage(std::cout);
        std::cout << "time:               " << ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC) << " secs\n";
    }
    else if (g_cmd_context) {
        g_cmd_context->set_regular_stream("stdout");
        g_cmd_context->display_statistics(true, ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
    }
}

display_statistics();
exit(0);

signal (SIGINT, SIG_DFL);
display_statistics();
raise(SIGINT);