Array-Logik (Beispiel QF_AX)

(set-logic QF_AX)
(declare-sort Index 0) 
(declare-sort Element 0) 
(declare-fun a () (Array Index Element)) 
(declare-fun i () Index) 
(declare-fun x () Element) 
(declare-fun y () Element) 
(assert (not (= (store (store a i x) i y)
                (store a i y))))
(check-sat)