(define x::(bitvector 20))
(define y::(bitvector 20))
(define z::(bitvector 20))
(define w::(bitvector 20))

(assert (and (= x y)(= z w)))
(assert (/= (bv-mul x z)(bv-mul w y)))

;;(dump-context)
(check)