\myheading{KLEE} (All timings are when KLEE 3.0 running on AMD Ryzen 5 3600.) I've also rewritten Sudoku example (\ref{sudoku_SMT}) for KLEE: \lstinputlisting[numbers=left]{puzzles/sudoku/KLEE/klee_sudoku_or1.c} Let's run it: \begin{lstlisting} % clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ klee_sudoku_or1.c ... % time klee --libc=uclibc --optimize klee_sudoku_or1.bc ... KLEE: ERROR: klee_sudoku_or1.c:96: ASSERTION FAIL: 0 KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 23675 KLEE: done: completed paths = 102 KLEE: done: partially completed paths = 1 KLEE: done: generated tests = 103 real 6m4.584s user 6m3.999s \end{lstlisting} Now this is really slower (on AMD Ryzen 5 3600) in comparison to Z3Py solution (\ref{sudoku_SMT}). But the answer is correct: \begin{lstlisting} % ls klee-last/*err klee-last/test000103.external.err % ktest-tool klee-last/test000103.ktest ktest file : 'klee-last/test000103.ktest' args : ['klee_sudoku_or1.bc'] num objects: 1 object 0: name: 'cells' object 0: size: 81 object 0: data: b'\x01\x04\x05\x03\x02\x07\x06\t\x08\x08\x03\t\x06\x05\x04\x01\x02\x07\x06\x07\x02\t\x01\x08\x05\x04\x03\x04\t\x06\x01\x08\x05\x03\x07\x02\x02\x01\x08\x04\x07\x03\t\x05\x06\x07\x05\x03\x02\t\x06\x04\x08\x01\x03\x06\x07\x05\x04\x02\x08\x01\t\t\x08\x04\x07\x06\x01\x02\x03\x05\x05\x02\x01\x08\x03\t\x07\x06\x04' object 0: hex : 0x010405030207060908080309060504010207060702090108050403040906010805030702020108040703090506070503020906040801030607050402080109090804070601020305050201080309070604 object 0: text: ................................................................................. \end{lstlisting} Character \TT{\textbackslash{}t} has code of 9 in C/C++, and KLEE prints byte array as a C/C++ string, so it shows some values in such way. We can just keep in mind that there is 9 at the each place where we see \TT{\textbackslash{}t}. The solution, while not properly formatted, correct indeed. By the way, at lines 45 and 46 you may see how we tell to KLEE that all array elements must be within some limits. If we comment these lines out, we've got this: \begin{lstlisting} ... KLEE: ERROR: klee_sudoku_or1.c:54: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:55: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:58: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:59: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:60: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:61: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:62: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:56: overshift error KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_sudoku_or1.c:57: overshift error KLEE: NOTE: now ignoring this error at this location ... \end{lstlisting} KLEE warns us that shift value at lines 54...62 is too big. Indeed, KLEE may try all byte values up to 255 (0xFF), which are pointless to use there, and may be a symptom of error or bug, so KLEE warns about it. % FIXME chk spelling Now let's use \verb|klee_assume()| again: \lstinputlisting{puzzles/sudoku/KLEE/klee_sudoku_or2.c} \begin{lstlisting} ... KLEE: ERROR: klee_sudoku_or2.c:96: ASSERTION FAIL: 0 KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 16739 KLEE: done: completed paths = 0 KLEE: done: partially completed paths = 1 KLEE: done: generated tests = 1 real 0m18.663s user 0m18.409s ... \end{lstlisting} That works much faster: because only one path to explore. And, as we see, the only one path has been found (one we actually interesting in it) instead of 161. It's still much slower than Z3Py solution, though.