(define a::(bitvector 4))
(define b::(bitvector 4))
(define c::(bitvector 4))
(define d::(bitvector 4))

(assert (= b a))
(assert (bv-lt c 0b0010))
(assert (= d b))
(assert (and (= c b) (= d 0b0100)))

(check)