Calvin-L
commented
4 years ago Looks like the error actually happens while calling the (no-op) Z3 error callback:
In the screenshot, the highlighted line is the next instruction to execute after api::context::context::set_error_code(...) (which is being called) returns. That procedure tail-calls api::context::invoke_error_handler(...) which tail-calls the m_error_handler function pointer which I suppose happens to be a libffi call. That makes sense since in the Z3 Python code:
def z3_error_handler(c, e):
# Do nothing error handler, just avoid exit(0)
# The wrappers in z3core.py will raise a Z3Exception if an error is detected
return
class Context:
# ...
def __init__(self, *args, **kws):
# ...
self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
# ...
Some of the recent Travis build failures indicate failed synthesis jobs with no further explanation. It appears that the synthesis jobs are segfaulting on Linux. In a Fedora 32 virtual machine,
cozy examples/lsort.dsexhibits the segfault consistently. Fromdmesg:The
dmesgoutput indicates that this is a null pointer dereference (segfault at 0). More info about segfault error codes.After a great deal of work, I was able to obtain a stacktrace:
It looks like Z3 is the culprit (
Z3_model_get_func_interp), but experience has shown me that it is much more likely to be Cozy's fault somehow.Notes: