From 758a6d98fb82cd9559a000a9c94b64d94800e296 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 12:35:48 +0000 Subject: [PATCH] FPA API clarification --- src/api/z3_fpa.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 70fafe6ea..e92b728d7 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -253,9 +253,9 @@ extern "C" { This is the operator named `fp' in the SMT FP theory definition. Note that \c sign is required to be a bit-vector of size 1. Significand and exponent - are required to be greater than 1 and 2 respectively. The FloatingPoint sort + are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes - of the arguments. + of the arguments. The exponent is assumed to be in IEEE-754 biased representation. \param c logical context \param sgn sign