Motivation

(Kroening/Strichman: Kapitel 10)

• Lineare Arithmetik + mathend000# uninterpretierte Funktionen:

  (x₂≥x₁)∧(x₁ - x₃≥x₂)∧(x₃≥0)∧f (f (x₁) - f (x₂))≠f (x₃) mathend000#

• Bitfolgen + mathend000# uninterpretierte Funktionen:

  f (a[32], b[1]) = f (b[32], a[1])∧a[32] = b[32] mathend000#

• Arrays + mathend000# lineare Arithmetik

  x = select(store(v, i, e), j)∧y = select(v, j)∧x > e∧x > y mathend000#