code: def limitReal(x, max_denominator=1000000):
      
      f = Fraction(x).limit_denominator(max_denominator)
      return Real((f.numerator, f.denominator))
docs: Creates an pysmt Real constant from x.
  
      Args:
          x (number): A number to be cast to a pysmt constant.
          max_denominator (int, optional): The maximum size of the denominator.
              Default 1000000.
  
      Returns:
          A Real constant with the given value and the denominator limited.