Incorrect result of reduce_inequalities involving pi and abs

[vitrun]

sympy v1.12:

In [1]: from sympy import *
   ...: m = symbols('m')

In [2]: reduce_inequalities(3 < abs(m))
Out[2]: ((-oo < m) & (m < -3)) | ((3 < m) & (m < oo))

In [3]: reduce_inequalities(pi < abs(m))
Out[3]: False

[vitrun]

After conducting a detailed analysis of the source code, I found differing behaviors in the two inequalities at /solvers/inequalities.py#L260:

            if not (domain.is_ZZ or domain.is_QQ):
                expr = numer/denom
                expr = Relational(expr, 0, rel)
                solution &= solve_univariate_inequality(expr, gen, relational=False)
            else:
                _eqs.append(((numer, denom), rel))

In the case of 3 < abs(m), the else branch correctly produces the desired result. However, it's important to note that the domain variable in the code is set to ZZ[pi], and ZZ[pi].is_ZZ evaluates to False. This led me to create issue25736 initially, but it appears that my understanding was incorrect. As clarified by @oscarbenjamin, the domain of pi is indeed ZZ[pi].

[smichr]

If you print out the _exprs being solved you see:

>>> reduce_inequalities(pi < abs(m))
[[_m - pi > 0, _m >= 0], [-_m - pi > 0, _m < 0]]

The intersections of the sublist solutions are the arguments for the union of the whole solution.