Soundness issue

[debugfe]

Hello everyone,
I think I found now also a "soundness" bug in AProVE:

int max_int = 2147483647;
int min_int = -2147483647; 

int __safe_div(int dividend, int divisor) {
  if (divisor == 0)
    return 0;
  else if (dividend <= min_int && divisor == -1)
    return max_int;
  else
    return dividend / divisor;
}

int __safe_mul(int x, int y) {
  int sqrt_max_int = 46340;
  int sqrt_min_int = -46340;
  if (x > sqrt_max_int || x < sqrt_min_int || y > sqrt_max_int || y < sqrt_min_int)
    return 0;
  else
    return x * y;
}

extern int __VERIFIER_nondet_int(void);

int main() {
  int b = __VERIFIER_nondet_int();
  int a = b;
  while (__safe_mul(__safe_mul(__safe_div(b, __safe_mul(-31, -96)), b), b) <= 0)
    ;
}

Here AProVE returns YES but choosing e.g. a b outside of [sqrt_min_int,sqrt_max_int] = [-46340,46340], makes __safe_mul return 0 and therefore the loop condition would evaluate to true. I could also reproduce this using your web interface.

[J-C-Kassing]

Thanks for the bug report!

We're currently working on a fix for this issue and expect it to be included in the upcoming release for this year's termination competition later this month.