sat
(
; cardinality of t is 2
; rep: (as @a0 t)
; rep: (as @a1 t)
(define-fun x () t (as @a0 t))
(define-fun y () t (as @a1 t))
(define-fun a () (Array t t) (store ((as const (Array t t)) (as @a0 t)) (as @a1 t) (as @a1 t)))
)