z3 - Is it possible to cast a bitvector of one bit into a boolean variable in SMTLib2? -

i want have boolean variable test if, e.g., third bit of bit vector 0. theory of bitvector allows extract 1 bit bitvector, not boolean type. wonder if can cast. thank you.

=== update ===

i'm sorry if question not clear. answer of nikolaj bjorner how test bit of bit vector. while want assign value of first bit of bit vector variable. try modify example follows:

(declare-fun x () (_ bitvec 5)) (declare-fun bit0 () bool) (assert (= (= #b1 ((_ extract 0 0) x)) bit0 )) (check-sat) 

and z3 complains:

(error "line 2 column 25: invalid declaration, builtin symbol bit0") (error "line 3 column 44: invalid function application, sort mismatch on argument @ position 2") 

i need variable bit0 later use. please give me hint? thanks.

create equality between extraction of third bit , bit-vector value 1 (and 1 bit).

e.g,

(declare-const x (_ bitvec 5)) (assert (= #b1 ((_ extract 2 2) x))) (check-sat) (get-model) 

produces

sat (model   (define-fun x () (_ bitvec 5)     #b00100) )