#5361

src/api/z3_fpa.h

@@ -961,7 +961,8 @@ extern "C" {
 
         \param c logical context
         \param t a floating-point numeral
-        \param sgn sign
+        \param sgn the retrieved sign
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for
         NaN, which is an invalid argument.
@@ -975,6 +976,7 @@ extern "C" {
 
         \param c logical context
         \param t a floating-point numeral
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long
         enough to represent the real significand precisely.
@@ -1004,6 +1006,7 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
         \param biased flag to indicate whether the result is in biased representation
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: This function extracts the exponent in `t`, without normalization.
         NaN is an invalid argument.
@@ -1019,6 +1022,7 @@ extern "C" {
         \param t a floating-point numeral
         \param n exponent
         \param biased flag to indicate whether the result is in biased representation
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: This function extracts the exponent in `t`, without normalization.
         NaN is an invalid argument.