user@host:~/queens$ clang -emit-llvm -c queens.c -I ../include -I ../klee/include queens.c:32:3: warning: implicit declaration of function '__assert_fail' is invalid in C99 [-Wimplicit-function-declaration] klee_assert(attack()); ^ ../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:~/queens$ time klee --libc=uclibc --posix-runtime queens.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/queens/klee-out-1" KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 62278464) KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: ERROR: (location information missing) ASSERTION FAIL: attack() KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 7307 KLEE: done: completed paths = 57 KLEE: done: generated tests = 57 real 0m4.042s user 0m3.811s sys 0m0.226s user@host:~/queens$ ls klee-last/*.err klee-last/test000057.assert.err user@host:~/queens$ ktest-tool klee-last/test000057.ktest ktest file : 'klee-last/test000057.ktest' args : ['queens.bc'] num objects: 2 object 0: name: 'model_version' object 0: size: 4 object 0: data: '\x01\x00\x00\x00' object 1: name: 'queens' object 1: size: 8 object 1: data: '\x04\x06\x03\x00\x02\x07\x05\x01' Note that the coordinates are 0-based and check it: http://spaz.ca/aaron/SCS/queens/