Support for AUFBV?

Question

Will Z3 be supporting AUFBV?

For the following script:

(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))

The online Z3 demo seems to be happy with the set-logic call, but then it complains about the sorts BitVec and Array. (Incidentally, the online demo seems to be happy with the set-logic call regardless of the logic name, even with bogus names such as (set-logic blarg).)

The SMT-Lib web-site does not mention neither UFBV nor AUFBV, but given their quantifier-free counterparts (QF_UFBV and QF_AUFBV), I was hoping Z3 would support AUFBV as well.

Needless to say, arrays play a very important role in practice. I think the AUFBV logic should remain decidable given the finiteness argument. It'd be really nice to see Z3 support it.

Thanks!