Hi Marek :-) Have in mind that klee uses bit-vector arithmetics to interact with the SMT solver, and things can get a little bit weird when you do so.
if n is a '1' followed by 31 zeros (in binary), it is indeed a negative number, but when you divide by two (shift the one one position to the right), it magically becomes positive. You can see the counter-example generated by klee with "ktest-tool --write-ints klee-last/test000001.ktest" and the queries to the SMT-solver with "klee -use-query-log=all:smt2 file.bc" Regards. 2016-02-02 10:06 GMT+01:00 Marek Chalupa <[email protected]>: > 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
