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

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

;;(dump-context)
(check)