Segmentation fault in scoped_timer

[pieter-bos]

Z3 crashes with a segmentation fault, and I was able to get this backtrace:

0x0000000000ece616 in scoped_timer::imp::sig_handler(sigval) ()
#0  0x0000000000ece616 in scoped_timer::imp::sig_handler(sigval) ()
#1  0x0000000000f2b4bf in timer_sigev_thread ()
#2  0x0000000000f9f4a4 in start_thread (arg=0x7ffff7f69700) at pthread_create.c:312
#3  0x0000000000ffbab9 in clone ()

Unfortunately I cannot provide a test case that causes this, as I cannot even reproduce it on my own machine (the error occurs within travis and only under specific circumstances). I did however find a potential race condition that could cause this, between here and setting g_on_timeout to nullptr somewhere else, e.g. here. Let me know if I can provide more information!

[NikolajBjorner]

the smtlib and dimacs front-end don't set the timer to null. The race condition would only happen for other formats (opb, lp, datalog). I have removed these sources of race conditions. But if the input you use is normal SMTLIB I don't see how it addresses the bug you see.

[pieter-bos]

That makes sense, I am using smt. I must admit I realized we're on an old version, and the newest z3 version does not exhibit this. Thank you for looking into it.

[NikolajBjorner]

the implementation of scoped timers changed when moving to C++ threads.
Could also be that we removed the nullptr assignments in the smtlib front-end when observing the same race condition you report. Closing as there is no support for downlevel.