From 127e8c3824f48b81e7a2a450627fd993691186bd Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 11 Aug 2026 19:42:11 -0500 Subject: [PATCH] Fix RealVal for floats requiring scientific notation `RealVal` passed `str(val)` to `mkReal`, but `str` switches to scientific notation for small and large magnitudes (`str(1e-5) == '1e-05'`), which `mkReal` rejects. Convert floats via `format(Decimal(repr(val)), "f")` instead. `repr` yields the shortest decimal that round-trips to the float, and formatting the `Decimal` with `"f"` expands it without an exponent, so the resulting rational is exactly the value Python would print, for every finite float. Co-Authored-By: Claude Opus 5 (1M context) --- cvc5_pythonic_api/cvc5_pythonic.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 44c0d3b..92d5466 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -3505,8 +3505,20 @@ def RealVal(val, ctx=None): 3/5 >>> RealVal("1.5") 3/2 + >>> RealVal(1.5) + 3/2 + >>> RealVal(1e-5) + 1/100000 + >>> RealVal(1e-11).eq(RatVal(1, 10**11)) + True """ ctx = _get_ctx(ctx) + if isinstance(val, float): + # `str` may use scientific notation (e.g. `str(1e-5) == '1e-05'`), + # which `mkReal` does not accept. `repr` gives the shortest decimal + # that round-trips to `val`, and formatting the resulting `Decimal` + # with `'f'` expands it without an exponent and without rounding. + return RatNumRef(ctx.tm.mkReal(format(Decimal(repr(val)), "f")), ctx) return RatNumRef(ctx.tm.mkReal(str(val)), ctx)