Worthwhile reports Z3 timeout although Z3 is still running

[tbormer]

Steps to reproduce:

1. Set Z3 timeout for the WW-project to 60s
2. Try to prove the following program correct:

Integer x
Integer y
Integer z := 0
Integer oldX := x
Integer oldY := y

while (y != 0) 
  _invariant y >= 0 && oldX * oldY = x * y + z
{
      if (y / 2 * 2 != y) {
          z := x + z
          y := y / 2
          x := 2 * x
      }

      if (y / 2 * 2 = y) {
          y := y / 2
          x := 2 * x
      }
}
_assert z = oldX * oldY

WW immediately reports that Z3 has reached the timeout but Z3 is still running in the background.

[jspam]

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.

[leonhandreke]

I have no idea what to do there and I consider it minor enough to not work on for now.

[bafain]

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 killing it is "not work for now".