(self, other: ArithRef | int | float)
| 475 | return self._binop(op, other) |
| 476 | |
| 477 | def __mod__(self, other: ArithRef | int | float) -> ArithRef: |
| 478 | # Int uses Euclidean mod (SMT-LIB), Real uses normal mod |
| 479 | op = BinOp.EMOD if isinstance(self._sort._ast_sort, IntASTSort) else BinOp.MOD |
| 480 | return self._binop(op, other) |
| 481 | |
| 482 | def __rtruediv__(self, other: int | float) -> ArithRef: |
| 483 | op = BinOp.EDIV if isinstance(self._sort._ast_sort, IntASTSort) else BinOp.DIV |