(declare-fun a () (Array (_ BitVec 1) (_ BitVec 2)))
(assert (ite true a (_ bv1 1)))