unknown
(
  (define-fun x () Pair
   (pair (store (as @a3 (Array Int S)) 0 s)
         (store (as @a3 (Array Int S)) 0 s)))
  (define-fun s () S (as @a2 S))
)