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