unknown
(
  (define-fun x () Int 0)
  (define-fun y () Int 0)
  (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
  (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
)