(set-logic QF_BV)
(set-info :status sat)
(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)