(declare-fun a () (Array (_ BitVec 16) (_ BitVec 2)))
(assert (store a (_ bv0 16) (_ bv0 1)))