(set-logic QF_BV)
(set-option :time-limit-per 200)
(set-option :rewrite-level 0)
(set-option :preprocess false)
(declare-const a (_ BitVec 16))
(declare-const b (_ BitVec 16))
(declare-const c (_ BitVec 16))
(push 1)
(assert (distinct (bvmul a b c) (bvmul b c a)))
(check-sat)
(pop 1)
(check-sat)