timeout signal handler invokes non-signal-safe functions


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:

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.


leodemoura wrote Feb 7, 2013 at 12:47 AM

Thanks for reporting the problem.
Does the problem also affects the unstable ("working-in-progress") branch?
We have recently fixed some problems with timers.


dvitek wrote Feb 7, 2013 at 8:19 PM

It looks like the problem still exists -- the timer is still implemented using signals on linux and freebsd. The signal handler still invokes a bunch of functions that aren't signal safe:
static void display_statistics() {
clock_t end_time = clock();
if ((g_solver || g_cmd_context) && g_display_statistics) {
    if (g_solver) {
        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->display_statistics(true, ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));

static void on_timeout() {

The ctrl+c suffers from the problem too, since it invokes display_statistics:
static void on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);

I'm happy working around this issue for the foreseeable future, so don't fix this bug on my behalf.