I'm working with different sizes of Z3 bitvecs and I was working on a way to ease the workload. I'm going to get the info from an object before z3 expression was created so it's not actually a vital problem but I wondered why z3 bitvecs doesn't carry runtime size information.
You can surely query the sort of every z3 AST term, and then get the size for bvs; so, yes, they do carry size information along with pretty much everything you need to know.
The relevant calls are:
The API documentation has myriad other calls for scrutinizing different parts of terms, see here.