user@host:~/magic$ clang -emit-llvm -g -c magicsquare.c -I ../include -I../klee/include magicsquare.c:85:2: warning: implicit declaration of function '__assert_fail' is invalid in C99 [-Wimplicit-function-declaration] klee_assert(!magic()); ^ ../klee/include/klee/klee.h:96:6: note: expanded from macro 'klee_assert' : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \ ^ 1 warning generated. user@host:~/magic$ time klee --libc=uclibc --posix-runtime magicsquare.bc KLEE: NOTE: Using klee-uclibc : /home/user/klee/Release+Asserts/lib/klee-uclibc.bca KLEE: NOTE: Using model: /home/user/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/user/magic/klee-out-4" KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 38035904) KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: ERROR: /home/user/magic/magicsquare.c:85: ASSERTION FAIL: !magic() KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 16605 KLEE: done: completed paths = 172 KLEE: done: generated tests = 172 real 0m52.896s user 0m51.102s sys 0m1.729s user@host:~/magic$ ls klee-last/*.err klee-last/test000153.assert.err user@host:~/magic$ ktest-tool klee-last/test000153.ktest ktest file : 'klee-last/test000153.ktest' args : ['magicsquare.bc'] num objects: 2 object 0: name: 'model_version' object 0: size: 4 object 0: data: '\x01\x00\x00\x00' object 1: name: 'square' object 1: size: 9 object 1: data: '\x04\x03\x08\t\x05\x01\x02\x07\x06' ... and, since \t == 9, that would be: 4 3 8 9 5 1 2 7 6