parameters: (self, other)
return_statement: return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
docstring: Create the Z3 expression `other * self`.
  
          >>> x = BitVec('x', 32)
          >>> 10 * x
          10*x
docstring_summary: Create the Z3 expression `other * self`.
docstring_tokens: Create the Z3 expression other * self .
function: def __rmul__(self, other):
          """Create the Z3 expression `other * self`.
  
          >>> x = BitVec('x', 32)
          >>> 10 * x
          10*x
          """
          a, b = _coerce_exprs(self, other)
          return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
function_tokens: def __rmul__ ( self , other ) : a , b = _coerce_exprs ( self , other ) return BitVecRef ( Z3_mk_bvmul ( self . ctx_ref ( ) , b . as_ast ( ) , a . as_ast ( ) ) , self . ctx )