parameters: (self, other)
return_statement: return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
docstring: Create the Z3 expression (signed) division `other / self`.
  
          Use the function UDiv() for unsigned division.
  
          >>> x = BitVec('x', 32)
          >>> 10 / x
          10/x
          >>> (10 / x).sexpr()
          '(bvsdiv #x0000000a x)'
          >>> UDiv(10, x).sexpr()
          '(bvudiv #x0000000a x)'
docstring_summary: Create the Z3 expression (signed) division `other / self`.
docstring_tokens: Create the Z3 expression ( signed ) division other / self .
function: def __rdiv__(self, other):
          """Create the Z3 expression (signed) division `other / self`.
  
          Use the function UDiv() for unsigned division.
  
          >>> x = BitVec('x', 32)
          >>> 10 / x
          10/x
          >>> (10 / x).sexpr()
          '(bvsdiv #x0000000a x)'
          >>> UDiv(10, x).sexpr()
          '(bvudiv #x0000000a x)'
          """
          a, b = _coerce_exprs(self, other)
          return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
function_tokens: def __rdiv__ ( self , other ) : a , b = _coerce_exprs ( self , other ) return BitVecRef ( Z3_mk_bvsdiv ( self . ctx_ref ( ) , b . as_ast ( ) , a . as_ast ( ) ) , self . ctx )