parameters: (self, other)
return_statement: return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
docstring: Create the Z3 expression (signed) mod `other % self`.
  
          Use the function URem() for unsigned remainder, and SRem() for signed remainder.
  
          >>> x = BitVec('x', 32)
          >>> 10 % x
          10%x
          >>> (10 % x).sexpr()
          '(bvsmod #x0000000a x)'
          >>> URem(10, x).sexpr()
          '(bvurem #x0000000a x)'
          >>> SRem(10, x).sexpr()
          '(bvsrem #x0000000a x)'
docstring_summary: Create the Z3 expression (signed) mod `other % self`.
docstring_tokens: Create the Z3 expression ( signed ) mod other % self .
function: def __rmod__(self, other):
          """Create the Z3 expression (signed) mod `other % self`.
  
          Use the function URem() for unsigned remainder, and SRem() for signed remainder.
  
          >>> x = BitVec('x', 32)
          >>> 10 % x
          10%x
          >>> (10 % x).sexpr()
          '(bvsmod #x0000000a x)'
          >>> URem(10, x).sexpr()
          '(bvurem #x0000000a x)'
          >>> SRem(10, x).sexpr()
          '(bvsrem #x0000000a x)'
          """
          a, b = _coerce_exprs(self, other)
          return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
function_tokens: def __rmod__ ( self , other ) : a , b = _coerce_exprs ( self , other ) return BitVecRef ( Z3_mk_bvsmod ( self . ctx_ref ( ) , b . as_ast ( ) , a . as_ast ( ) ) , self . ctx )