\begin{slide}{Motivation}

(Kroening/Strichman: Kapitel 10)

\begin{itemize}
\item 
  Lineare Arithmetik $+$ uninterpretierte Funktionen:

$(x_2\ge x_1) \wedge (x_1-x_3\ge x_2) \wedge
(x_3\ge 0) \wedge f(f(x_1)-f(x_2)) \neq f(x_3)$
\item
  Bitfolgen $+$ uninterpretierte Funktionen:

$f(a[32],b[1])=f(b[32],a[1])\wedge a[32]=b[32]$
\item
  Arrays $+$ lineare Arithmetik

$x=v\{i:=e\}[j] \wedge y=v[j]\wedge x>e\wegde x>y$
\end{itemize}


\end{slide}
