Array-Logik (Beispiel QF_AUFLIA)

(set-logic QF_AUFLIA)
(declare-fun a () (Array Int Int)) 
(declare-fun b () (Array Int Int)) 
(declare-fun i () Int) 
(declare-fun j () Int) 
(declare-fun k () Int) 
(assert (< i j))
(assert (< (select a i) (select a j)))
(assert (= b (store a k 0)))
(assert (> i k))
(assert (> (select b i) (select b j)))
(check-sat)