(set-logic QF_ABV) (set-info :status sat) (declare-const a0 (Array (_ BitVec 1) (_ BitVec 1) )) (declare-const v0 (_ BitVec 1)) (assert (= #b1 (select a0 v0))) (check-sat)