[SMT-LIB] Combine Boolean & BitVector?

[Jun Koi]

hi,

i want to do a simple logic on a variable, like this:

a = (b == 0? 1 : 0)

that is, a will be 1 if b is 0, or 0 if b is not 0.

i implemented the logic in below code. but Z3 complains "operator is
applied to arguments of the wrong sort" on line 4.
i guess this means it is not allowed to AND a Boolean value and a
Bitvector value.

but then how can i implement my idea?

thanks a lot,
Jun

-------
(set-logic QF_BV)
(declare-fun a () (_ BitVec 4))
(declare-fun b () (_ BitVec 4))
(assert (= a (bvand (= b #x0) #x1)))
(check-sat)