(declare-fun an_array () (Array (_ BitVec 1) (_ BitVec 1)))
(assert (not  (store an_array true false))