Greetings, I recently posted on Bugzilla a bug report [1] concerning the crash of Klee 64-bit during symbolic memory allocation, for a certain number of coreutils. In the mean time I investigated the issue and discovered that the crash was caused by a size mismatch between a 64-bit value and a 32-bit one, when they were used together in a comparison expression. The latter was 32-bit because its type was hard-coded instead of being determined dynamically (as it was the case for the former value).
Therefore, I proposed a patch to fix this issue, which can be found as well on the bug report page. If you encountered this problem, too, I encourage you to apply the fix and check that everything works all right. Cheers, Stefan [1] http://llvm.org/bugs/show_bug.cgi?id=6211
