\myheading{School-level equation: KLEE}

Let's revisit school-level system of equations from (\ref{eq2_SMT}).

We will force KLEE to find a path, where all the constraints are satisfied:

\lstinputlisting[style=customc]{equations/KLEE_eq/klee_eq1.c}

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

...

% time klee --libc=uclibc --optimize --use-query-log=solver:smt2 klee_eq1.bc
KLEE: done: total instructions = 11794
KLEE: done: completed paths = 2
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 3
\end{lstlisting}

Let's find out, where \TT{klee\_assert()} has been triggered:

\begin{lstlisting}
% ls klee-last/*err
klee-last/test000001.external.err

% ktest-tool klee-last/test000001.ktest | grep uint
object 0: uint: 5
object 1: uint: 2
object 2: uint: 1
\end{lstlisting}

This is indeed correct solution to the system of equations.

But 3 tests generated. What are others? Others are \emph{partial} solutions,
which leads to one of \emph{return} statements.
See explanation: \ref{KLEE_zebra}.

\myhrule{}

KLEE has \emph{intrinsic} \TT{klee\_assume()} which tells KLEE to cut path if some constraint is not satisfied.
So we can rewrite our example in such cleaner way:

\lstinputlisting[style=customc]{equations/KLEE_eq/klee_eq2.c}

Interestingly, we can dump SMT-LIB 2 file here and see its contents:

\begin{lstlisting}
% time klee --libc=uclibc --optimize --use-query-log=solver:smt2 klee_eq2.bc

KLEE: done: total instructions = 11652
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1
\end{lstlisting}

\lstinputlisting[style=customc]{equations/KLEE_eq/eq2_solver-queries.smt2}

There are 3 queries, each for each path.
I can try them all separately.

\lstinputlisting[caption=First query]{equations/KLEE_eq/1.txt}

\lstinputlisting[caption=Second query]{equations/KLEE_eq/2.txt}

\lstinputlisting[caption=Third query]{equations/KLEE_eq/3.txt}

Aha, here the solution in surfacing gradually.
First, KLEE determines the correct value for 'circle', then for 'square', then for 'triangle'.
Each 32-bit variable of \emph{integer} type is represented by 4-bytes tuple.
Maybe there is some reason for this.