Open tbormer opened 12 years ago
This does not work when calling Z3 via a shell script. I have the following shell script called z3
(to be able to simulate timeouts):
#!/bin/bash
# sleep 10
./z3bin $*
When a timeout occurs, the Z3 binary is not killed. It works when running z3 directly without the shell script in between.
I have no idea what to do there and I consider it minor enough to not work on for now.
Since z3bin
is executed as the shell's child and destroy()
does not ask, that is send some signal like SIGINT
instead of SIGKILL
that could be handled, the Process
to exit the shell cannot terminate its child process and z3bin
is still running after Worthwhile has called destroy()
on the shell's Process
object.
I agree with @leonhandreke that doing things like deciding which operating system Worthwhile is running on (for how to do the following), getting the shell's pid
and kill
ing it is "not work for now".
Steps to reproduce:
WW immediately reports that Z3 has reached the timeout but Z3 is still running in the background.