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)