% clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ TGIF_KLEE1.c % time klee --libc=uclibc --optimize --use-query-log=solver:smt2 TGIF_KLEE1.bc ... KLEE: ERROR: TGIF_KLEE1.c:20: failed external call: klee_assert KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 11734 KLEE: done: completed paths = 1 KLEE: done: partially completed paths = 1 KLEE: done: generated tests = 2 ... % ls klee-last/* klee-last/assembly.ll klee-last/run.stats klee-last/test000001.ktest klee-last/info klee-last/solver-queries.smt2 klee-last/test000002.ktest klee-last/messages.txt klee-last/test000001.external.err klee-last/warnings.txt klee-last/run.istats klee-last/test000001.kquery % ktest-tool klee-last/test000001.ktest | grep uint object 0: uint: 86400 % ktest-tool klee-last/test000002.ktest | grep uint object 0: uint: 0