Проверка того, является ли действительное число целым числом в alt-ergo

Question

Я хочу проверить, является ли реальное значение целым числом. Кажется, не существует функции Floor или аналогичной, поэтому я пытаюсь использовать функцию real_of_int из учебника следующим образом:

      function real_of_int(n:int):real = n **. 1
predicate is_int_r(a:real) = exists v:int . a = real_of_int(v)

goal g1: real_of_int(0) = 0.0
goal g2: exists v:int . real_of_int(v) = 0.0
goal g3: is_int_r(0.0)


File "test2.ae", line 4, characters 10-30: Valid (0.0000) (3 steps) (goal g1)
File "test2.ae", line 5, characters 10-45: I don't know (0.0000) (9 steps) (goal g2)
File "test2.ae", line 6, characters 10-23: I don't know (0.0013) (11 steps) (goal g3)

Таким образом, действительное число int 0 равно 0,0 (g1 допустимо), но существует в g2 не может его найти, и, следовательно, g3 тоже не работает (alt-ergo 2.4.3).

Есть лучший способ сделать это?

Поскольку g1 действителен, я ожидал, что g2 найдет v=0. Но это не так.