(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1)))
(assert (ite true (_ bv0 16) a)