[SMT-LIB] "typecast" for bitvec?

[Jun Koi]

hi,

how can we "typecast" when we assert 2 bitvec vars of different size?
the below code reports "sort mismatch" with Z3.

naturally, a dirty hack is to set a32 to 64 bit, but i dont want that.

many thanks,
J

;;;;;;;;
(set-logic QF_BV)
(declare-fun a64 () (_ BitVec 64))
(declare-fun a32 () (_ BitVec 32))
(assert (= a64 a32))
(check-sat)