RealVal("1/2") fails to parse fraction strings

[kiranandcode]

Reproducer

from lean_py.z3 import RealVal

val = RealVal("1/2")
# ValueError: invalid literal for int() with base 10: '1/2'

z3py accepts fraction strings like "1/2" in RealVal() and constructs the corresponding rational value. lean.py's RealVal hits int("1/2") because the parsing branch in core.py:1136 only checks for "." and "e" before falling through to int(n).

RatVal(1, 2) works as a workaround.