\begin{slide}{Nelson-Oppen, Beispiel}

(Kroening/Strichman, Ex. 10.8)

NO-Verfahren anwenden auf:

$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) $

\bigskip

Diese Beispiel als Constraint-Problem
in der geeigneten SMT-LIB-Teilsprache 
formulieren und mit Z3 Erfüllbarkeit bestimmen.


\end{slide}
