Hi Marek,
I think you have indeed hit a bug in KLEE. The bug seems to be in the
way we optimise divides by a constant, so to avoid it, you should pass
-solver-optimize-divides=false.
Can you please report this on GitHub, including your program? I (or
others) will try to fix this soon.
Cristian
On 02/02/2016 09:06, Marek Chalupa wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
