Incorrect bug report

[XujieSi]

I played a little bit with LinearArbitrary-SeaHorn. The following code seems correct to me, but the tool complains it is buggy.

#include "seahorn/seahorn.h"
int main() {
  // variable declarations
  int n;
  int x;
  // pre-conditions
  (x = n);
  // loop body
  while ((x > 1)) {
    {
    (x  = (x - 1));
    }

  }
  // post-condition
  if ( (n > 0) )
    sassert( (x == 1) );

}

Just want to make sure I didn't do something silly. Could you please run your built of LinearArbitrary-SeaHorn on it?

[rowangithub]

The tool is weak in handling uninitialized variables. Please modify the code to "int n = unknown()". Then, the result should be as expected.

[XujieSi]

Cool, thanks!