结论性内容：
（1）如果是在程序中使用klee_make_symbolic，则可以使用下列脚本进行重现。
export LD_LIBRARY_PATH=/home/klee/xiaojiework/klee-xiaojie/build/debug/lib/:$LD_LIBRARY_PATH
gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test4.c -lkleeRuntest
KTEST_FILE=klee-last/test000015.ktest ./a.out
（2）如果是对命令行参数进行建模，即对klee进行符号执行的时候，使用 --posix-runtime选项，设定sym-args等参数，则重现只能用klee-replay，不能用（1）中的脚本。不需要链接到klee的运行库-lkleeRuntest，并且直接用gcc对代码进行编译成本地代码即可。
示例代码：
#include <stdio.h>//test.c #include <string.h> #include <stdlib.h> #include <assert.h> #include <klee/klee.h> int main(int argc, char* argv[]) { int result = argc > 1 ? atoi(argv[1]) : 0; if (result == 42) { klee_assert(0); } return result; }
脚本：
clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3
执行结果：
klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3
KLEE: NOTE: Using klee-uclibc : /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca
KLEE: NOTE: Using model: /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/kleeexperiment/modeltest/klee-out-31"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 71386000)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:22: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 11567
KLEE: done: completed paths = 73
KLEE: done: generated tests = 69
查看对应assertion错误的测试用例：
我们直接对程序输入+42，进行执行重现。
可以看到，即使是gcc test2.c -o test2（不是gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test2.c -lkleeRuntest），并且LD_LIBRARY_PATH是空的。为什么gcc能够在不链接到-lkleeRuntest的时候，对klee-assert进行解释呢？
这是因为在klee/klee.h中是这样定义的：
# define klee_assert(expr)
((expr)
? (void) (0)
: __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__))
所以压根不需要链接到kleeRuntest运行库。
下面改用--sym-arg选项，
clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --libc=uclibc --posix-runtime test2.bc --sym-arg 3
可以看到，和使用--sym-args生成了同样的测试用例。即+42，我们可以直接在命令行使用./test2 +42进行执行重现。
但是，在实际的实验进程中（由于反复试验，求解每次随机返回一个解），我还生成了另外内容的测试用例，同样覆盖assertion错误。内容如下：
对于这个测试用例，内容是x0b42，实际上就是三个字符，第一个是垂直制表符号，第二个是字符'4'，第三个是字符'2'。第一个无法直接通过命令行输入，所以我们使用klee的重现机制。
我们同时搜集的还有内容是‘42x00x00’的测试用例，连同之前的两个测试用例，三个测试用例都放在了generatedtests目录下：
使用脚本：
均没有任何assertion fail的反应。但是使用klee-repaly的时候，
三个测试输入依次是：
垂直字表符，42（垂直字表符，我们从键盘是敲不出来的）
42
+42
所以，对命令行建模的时候，需要用klee-replay的机制。
我们采取在程序中使用klee_make_symbolic的方式，再分析一下klee执行重现机制。
代码：
int main() { //test4.c int argc=2; int size=4; char argv[size]; klee_make_symbolic(argv, sizeof argv, "argv"); argv[3]=' '; int result = argc > 1 ? atoi(argv) : 0; if (result == 42) { klee_assert(0); //printf("yes"); } return result; }
由于不需要对命令行参数进行建模，我们使用如下脚本：
clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test4.c
klee --optimize --libc=uclibc test4.bc --sym-args 0 1 3
去除了--posix-runtime选项，因为不需要对命令行参数进行建模。需要保留--libc=uclibc选项，因为还要对atoi函数进行建模和处理。
下一步使用klee的重现机制。我们看到，可以使用KTEST_FILE的方式。
再试试klee-replay，结果显示：
由于test4.c中有klee_make_symbolic的语句，导致我们必须链接到lkleeRuntest才能执行重现。我们手动去掉这个语句，再编译成本地可执行代码，不链接到kleeRuntest运行库，即直接使用gcc -o test4 test4.c。结果仍然报错。
分析完毕！klee-replay和KTestFile指定文件各有应用场景，正如随笔一开始所给出的结论性内容。