[klee-dev] bug in klee/stp

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev