(set-logic QF_BV)
(set-option :produce-models true)
(declare-fun |val1| ()  (_ BitVec 16))
(declare-fun |val2| ()  (_ BitVec 16))
(declare-fun |gen_mul| ()  (_ BitVec 16))
(assert (= |val1| #xb621))
(assert (= |val2| #xd620))
(assert (= |gen_mul| (bvmul val1 val2)))
(check-sat)
(get-value (|val1|))
(get-value (|val2|))
(get-value (|gen_mul|))
(exit)