z3 - How use forall in bit-vector -

i intend go vector, , different things on each bit.

what want know if i'm doing forall (in define-fun lt....)?

because results not match expected: s

code found in link: http://rise4fun.com/z3/xrfk

i'm not sure intended semantics of formula is, intuitively seems definition of is_in may culprit:

(define-fun is_in ((e (_ bitvec 9)) (s (_ bitvec 9))) bool     ;; true if e element of "set" s.     (= (bvand e s) e)) 

the constraint (= (bvand e s) e)) means function can return true when s equal e. going name of function, expect definition (not (= (bvand e s) empty)).