from z3 import *
#求解变量
v46=BitVec('v46',8)
#求解器
solver = Solver()
#约束条件
solver.add(  v4  == 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52)
#求解
solver.check()
#结果模型
mz = solver.model()
#格式化结果
ans = ''
ans += chr(int("%s" % (mz[v46])))

https://ericpony.github.io/z3py-tutorial/guide-examples.htm