我无法重现本文图 7 中的结果：
http://www.stanford.edu/~engler/klee-osdi-2008.pdf
具体来说，我尝试测试核心 util 的“tac”命令：
klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./tac.bc -r -sym-files 20 1
但是，我没有看到 KLEE 报告的任何错误消息，尽管该论文声称应该存在错误。
另一方面，如果我像这样测试核心 util 的“md5sum”命令：
klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./md5sum.bc -c -sym-files 1 10
KLEE 报以下错误：
: /root/coreutils-6.10/obj-llvm/src/../../src/md5sum.c:212: memory error: out of bound pointer
有人可以指出正确的方向来发现“tac”或“pr”命令中的错误吗？如果这些都需要文件“t2.txt”和“t3.txt”，它们分别在论文中定义为“\b\b\b\b\b\b\b\t”和“\n”。
将不胜感激所有/任何建议。