Nelson-Oppen, Beispiel

(Kroening/Strichman, Ex. 10.8)

NO-Verfahren anwenden auf:

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

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