From c172b5826832046db5aa8ee92ff9525771d60cd8 Mon Sep 17 00:00:00 2001
From: Daniel Tang <danielzgtg.opensource@gmail.com>
Date: Sat, 14 Feb 2026 01:37:58 -0500
Subject: [PATCH] Alias ArithRef.__abs__ to Abs

This integrates with the `abs(Int('x'))` Python builtin.
---
 src/api/python/z3/z3.py | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 132edecde..aec92b466 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2804,6 +2804,17 @@ class ArithRef(ExprRef):
         a, b = _coerce_exprs(self, other)
         return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
 
+    def __abs__(self):
+        """Return an expression representing `abs(self)`.
+
+        >>> x = Int('x')
+        >>> abs(x)
+        If(x > 0, x, -x)
+        >>> eq(abs(x), Abs(x))
+        True
+        """
+        return Abs(self)
+
 
 def is_arith(a):
     """Return `True` if `a` is an arithmetical expression.