[klee-dev] bug in klee/stp

[Marek Chalupa]

Hi list,

I have this small trivial program:


#include <assert.h>

int main(void)
{
   int n;
   klee_make_symbolic(&n, sizeof n, "n");
   klee_assume(n < 0);

   if (n/2 > 0)
     assert(0);

   return 0;
}


KLEE (on master from git) says that the assertion is violated, although 
since n is negative, then n/2 should not be greater than 0 and the 
assert() should be never called. I suppose it is a bug, or did I 
overlook something?

P.S. If the condition is just (n > 0), then everything is fine. The 
assumption can be even (n < -1) or (n < -1 && n > -10) (in which case I 
get that the assumption is provably false, which is weird also)

Thanks,
Marek