Running KLEE to Solve 8-Queens

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/