(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1) ))
(assert (not a))