AProVE returning false alarm for program with unsigned int

[debugfe]

Hello everyone,
I noticed that AProVE returns "non-terminating" for

int main(void) {
  unsigned int input = (unsigned int) -1; // should be 4294967295
  while(input != 0)
    input--;
  return 0;
}

This is especially surprising as this, more general, program is found terminating:

extern unsigned int __VERIFIER_nondet_uint();

int main(void) {
  unsigned int input = __VERIFIER_nondet_uint();
  while(input != 0)
    input--;
  return 0;
}

Inspecting the generated .koat files I think there is something wrong with the translation as the rewrite system in the koat files seems indeed non-terminating.
I am using the version from last SV-Comp and the corresponding command: ./AProVE.sh --bit-width 64 test.c
Thanks in advance!

[nilslommen]

Thanks for spotting this bug. There appears to be an issue with the handling of unsigned variables. We are trying to fix it soon.

[J-C-Kassing]

After some refactoring, we have now published an open-source version of AProVE at aprove-open-source.

I checked this issue again and can confirm that the bug still seems to be present. Since future development and maintenance will happen in the new repository, could you please open a corresponding issue there?

Looking at the nontermination proof for the first example, it appears that AProVE currently ignores the cast to unsigned int during the translation and effectively treats the input variable as having the value -1 in the generated LLVM representation. This would explain why the generated KoAT system becomes non-terminating. We will investigate why this cast is not handled correctly during translation.