(declare-fun a () (Array (_ BitVec 128) (_ BitVec 1)))
(declare-fun b () (Array (_ BitVec 128) (_ BitVec 8)))
(assert (= a b))