Motivation

(Kroening/Strichman: Kapitel 10)

• Lineare Arithmetik + uninterpretierte Funktionen:

  (x₂$\ge$x₁) $\wedge$ (x₁ - x₃$\ge$x₂) $\wedge$ (x₃$\ge$0) $\wedge$ f (f (x₁) - f (x₂)) $\neq$ f (x₃)

• Bitfolgen + uninterpretierte Funktionen:

  f (a[32], b[1]) = f (b[32], a[1]) $\wedge$ a[32] = b[32]

• Arrays + lineare Arithmetik

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