Hi,
On Thu, 29 Nov 2018 15:32:33 +0800 changze cui <[email protected]> wrote: > For now, I am thinking there may be some other random number generator > related to state selection which may influence instruction execution > sequence. But I haven't found it yet. there are quite a few other sources for non-determinism, e.g.: - environment variables - number of files in your directory - name of the executable - other external concrete data (time stamps, ...) - allocation scheme - ... If your traces diverge in the uclibc setup phase, this is most likely the cause. It might help to use -environ, -run-in, -allocate-determ, ... Good luck, Frank _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
