\myheading{KLEE}
\label{KLEE_zebra}

\renewcommand{\CURPATH}{puzzles/zebra/KLEE}

We just define all variables and add constraints:

\lstinputlisting[style=customc]{\CURPATH/klee_zebra1.c}

I force KLEE to find distinct values for colors, nationalities, cigarettes, etc, 
in the same way as I did for Sudoku earlier 
(\ref{sudoku_SMT}).

Let's run it:

\begin{lstlisting}
% clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ klee_zebra1.c
...

% time klee --libc=uclibc --optimize klee_zebra1.bc
KLEE: done: total instructions = 15399
KLEE: done: completed paths = 42
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 43
\end{lstlisting}

It works for $\approx 7$ seconds on my Intel Core i3-3110M 2.4GHz notebook.
Let's find out path, where \TT{klee\_assert()} has been executed:

% FIXME:
\begin{lstlisting}
% ls klee-last/*err
klee-last/test000037.external.err

% ktest-tool klee-last/test000037.ktest
ktest file : 'klee-last/test000037.ktest'
args       : ['klee_zebra1.bc']
num objects: 25
object  0: name: 'Yellow'
object  0: size: 4
object  0: data: b'\x01\x00\x00\x00'
object  0: hex : 0x01000000
object  0: int : 1
object  0: uint: 1
object  0: text: ....
object  1: name: 'Blue'
object  1: size: 4
object  1: data: b'\x02\x00\x00\x00'
object  1: hex : 0x02000000
object  1: int : 2
object  1: uint: 2
object  1: text: ....
object  2: name: 'Red'
object  2: size: 4
object  2: data: b'\x03\x00\x00\x00'
object  2: hex : 0x03000000
object  2: int : 3
object  2: uint: 3
object  2: text: ....

...

object 23: name: 'Dog'
object 23: size: 4
object 23: data: b'\x04\x00\x00\x00'
object 23: hex : 0x04000000
object 23: int : 4
object 23: uint: 4
object 23: text: ....
object 24: name: 'Zebra'
object 24: size: 4
object 24: data: b'\x05\x00\x00\x00'
object 24: hex : 0x05000000
object 24: int : 5
object 24: uint: 5
object 24: text: ....
\end{lstlisting}

This is indeed the correct solution.

How many tests are there?

\begin{lstlisting}
% ls -la klee-last/*.ktest | wc -l
43
\end{lstlisting}

This is because KLEE found a test for each path, till each \emph{return}.

How many \emph{return} statement our program has, after all?
Almost 43:

\begin{lstlisting}
 % cat klee_zebra1.c| grep return | wc -l
45
\end{lstlisting}

\myhrule{}

\TT{klee\_assume()} also can be used:

\lstinputlisting[style=customc]{\CURPATH/klee_zebra2.c}

\begin{lstlisting}
% time klee --libc=uclibc --optimize klee_zebra2.bc
...
KLEE: done: total instructions = 12304
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1

% ls klee-last/
assembly.ll  messages.txt  run.stats            test000001.external.err  test000001.ktest
info         run.istats    solver-queries.smt2  test000001.kquery        warnings.txt
\end{lstlisting}

\dots and this version works slightly faster ($\approx 5$ seconds).
Faster, because KLEE has to find only one path, till the end of the function.
Hence, here is only one test generated.