Termination analysis: Bug

[pwnchaser]

Hello again,
I believe I have another "soundness" bug and I think it is independent from #472 as it also occurs in the respective side branch.

int one() { return 1; }

int mul(int x, int y) {
    return x * y;
}

int div_by_32(int dividend, int divisor) {
  if (divisor == 0)
    return 0;
  else
    return dividend / 32;
}

int main(void) {
  int x = -33;
  int v1 = one();
  while (v1 || div_by_32(1, mul(x, x / 32)))
    ;

  while (1)
    x++;
  
  return 0;
}

Here Theta returns Safe but should have returned Unsafe:

$ "./theta/theta-start.sh" "test.c" "--svcomp" "--backend" "IMC"  "--property" "termination.prp" "--architecture" "LP64" "--memlimit" "1000000000"
...
(SafetyResult Safe)