z3 process kept alive for longer than necessary

[keyboardDrummer]

Verify Foo in the following program:

method Foo() {
  assert Ack(4, 3) == 1;
}

function Ack(m: nat, n: nat): nat
{
  if m == 0 then
    n + 1
  else if n == 0 then
    Ack(m - 1, 1)
  else
    Ack(m - 1, Ack(m, n - 1))
}

After verification times out, there is still a z3 process running, until you make an edit to the program. It would be better if the z3 process was terminated immediately after verification finished.