[SMT-LIB] "typecast" for bitvec?

Jun Koi junkoi2004 at gmail.com
Wed Sep 7 21:58:25 EDT 2011


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)


More information about the SMT-LIB mailing list