(define x::(bitvector 20))
(define y::(bitvector 20))
(assert (= x y))
(assert (/= (bv-neg x)(bv-neg y)))
(check)