Spezialfälle

durch beschriebene Transformation kann man Array-Logik reduzieren auf Kombination von

• Index-Logik (z. B. lineare Arithmetik)
• Element-Logik
• uninterpretierte Funktionen.

Lösen mit Nelson-Oppen möglich.

Ähnliche Rechnungen finden (seit vielen Jahrzehnten!) im Schleifen-Optimiere von gcc statt (Beispiel).

Mit Array-Logik kann man beweisen, daß der Optimierer recht hat.