diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 81bef8e9ac415a838d5eae427005b8dbc7308de6..cb836f48af6787f6e94ff6593d3490a5a4013155 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -125,11 +125,15 @@ our theory ``ACASXU_P1``.
 
 We will need to write down some numerical values. As of now, CAISAR allows
 writing values using floating-point arithmetic only. Why3 defines a float type
-and the relevant arithmetic operations according to the IEEE floating-point
+and the relevant arithmetic operations according to the IEEE 754 floating-point
 standard in a theory, astutely called ``ieee_float``. Specifically, we will
 import the ``Float64`` sub-theory, that defines everything we need for 64-bit
 precision floating-point numbers. We thus import it in our theory using the
 ``use`` keyword.
+This currently requires to write exact IEEE 754 floating
+point values in the specification file, which is
+understandably a setback in terms of usability, but have the
+advantage of being unambiguous on the specification.
 
 Our file looks like this so far: