parameters: (self, other)
return_statement: return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
docstring: Create the Z3 expression `other%self`.
  
          >>> x = Int('x')
          >>> y = Int('y')
          >>> x % y
          x%y
          >>> simplify(IntVal(10) % IntVal(3))
          1
docstring_summary: Create the Z3 expression `other%self`.
docstring_tokens: Create the Z3 expression other%self .
function: def __mod__(self, other):
          """Create the Z3 expression `other%self`.
  
          >>> x = Int('x')
          >>> y = Int('y')
          >>> x % y
          x%y
          >>> simplify(IntVal(10) % IntVal(3))
          1
          """
          a, b = _coerce_exprs(self, other)
          if z3_debug():
              _z3_assert(a.is_int(), "Z3 integer expression expected")
          return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
function_tokens: def __mod__ ( self , other ) : a , b = _coerce_exprs ( self , other ) if z3_debug ( ) : _z3_assert ( a . is_int ( ) , "Z3 integer expression expected" ) return ArithRef ( Z3_mk_mod ( self . ctx_ref ( ) , a . as_ast ( ) , b . as_ast ( ) ) , self . ctx )