Greetings, I found another problem in the Klee runtime code that manifests on 64bit architectures. It can be a serious source of dropped states when testing utilities which use the file system model, and it was also one of the sources of failed replays that I mentioned in previous messages.
In brief, the Klee runtime API (specified in include/klee/klee.h) contains function declarations that take 32 bit parameters, while they are sometime used in the file system model code with 64bit arguments. This results into value truncations, which further lead to invalid assumptions and dropped states. More details about this problem can be found here: http://llvm.org/bugs/show_bug.cgi?id=6690 I have also submitted a patch which solves the problem in my case, and which may be useful for you, as well. Note that it was tested only on Linux 64bit, so it needs additional testing for other architectures. In particular, I expect it not to work on Windows machines, because of different interpretation of the "unsigned long" type. Best regards, Stefan Bucur
