From 13b24dee44c23124a6bed652a5be51f24b1773d0 Mon Sep 17 00:00:00 2001
From: Ernesto Casablanca <65033249+TendTo@users.noreply.github.com>
Date: Tue, 2 Jun 2026 20:17:17 +0100
Subject: [PATCH] fix: support smaller floats

This solves the issue with RealVal where some smaller values (in absolute terms) would cause an issue when converted to string, since they use the scientific notation.
---
 cvc5_pythonic_api/cvc5_pythonic.py | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 44c0d3b..74233e7 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -3507,6 +3507,12 @@ def RealVal(val, ctx=None):
     3/2
     """
     ctx = _get_ctx(ctx)
+    if isinstance(val, float):
+        if abs(val) > 1e-10:
+            return RatNumRef(ctx.tm.mkReal(f"{val:.10f}"), ctx)
+        else:
+            num, den = val.as_integer_ratio()
+            return RatVal(num, den, ctx)
     return RatNumRef(ctx.tm.mkReal(str(val)), ctx)