parameters: (self, other)
return_statement: return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
docstring: Create the Z3 expression `self + other`.
  
          >>> x = Int('x')
          >>> y = Int('y')
          >>> x + y
          x + y
          >>> (x + y).sort()
          Int
docstring_summary: Create the Z3 expression `self + other`.
docstring_tokens: Create the Z3 expression self + other .
function: def __add__(self, other):
          """Create the Z3 expression `self + other`.
  
          >>> x = Int('x')
          >>> y = Int('y')
          >>> x + y
          x + y
          >>> (x + y).sort()
          Int
          """
          a, b = _coerce_exprs(self, other)
          return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
function_tokens: def __add__ ( self , other ) : a , b = _coerce_exprs ( self , other ) return ArithRef ( _mk_bin ( Z3_mk_add , a , b ) , self . ctx )