Fix an incorrect limit in conversion from real to float (#4418)

This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 1b1bfddc21f297a7be55d4ef750d63218d961e53..3bcf2b0de9b8a81b69d0a8bb64234db7417cd978 100644 (file)
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -19,6 +19,7 @@
 #include "util/integer.h"
 
 #include <math.h>
+#include <limits>
 
 #ifdef CVC4_USE_SYMFPU
 #include "symfpu/core/add.h"
@@ -920,15 +921,25 @@ static FloatingPointLiteral constructorHelperBitVector(
       Integer significand(0);
 #endif
       Integer signedSignificand(sign * significand);
-      
-      // Only have pow(uint32_t) so we should check this.
-      Assert(this->t.significand() <= 32);
+
+      // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
+      // As we convert Integer -> unsigned int -> uint32_t we need that
+      // unsigned int is not smaller than uint32_t
+      static_assert(sizeof(unsigned int) >= sizeof(uint32_t));
+#ifdef CVC4_ASSERTIONS
+      // Note that multipling by 2^n requires n bits of space (worst case)
+      // so, in effect, these tests limit us to cases where the resultant
+      // number requires up to 2^32 bits = 512 megabyte to represent.
+      Integer shiftLimit(std::numeric_limits<uint32_t>::max());
+#endif
 
       if (!(exp.strictlyNegative())) {
+       Assert(exp <= shiftLimit);
        Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
        return PartialRational(Rational(r), true);
       } else {
        Integer one(1U);
+       Assert((-exp) <= shiftLimit);
        Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
        Rational r(signedSignificand, q);
        return PartialRational(r, true);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5a59f2f54d9f3f532d16aeb831b8003a90df46dd..fbf249e7fbd5535251475a9ec8785b79df244a5c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -503,6 +503,7 @@ set(regress_0_tests
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/issue3536.smt2
+  regress0/fp/issue3619.smt2
   regress0/fp/issue4277-assign-func.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/rti_3_5_bug_report.smt2

diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2
new file mode 100644 (file)
index 0000000..9d6e0a3
--- /dev/null
+++ b/test/regress/regress0/fp/issue3619.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: symfpu
+(set-logic QF_FPLRA)
+(set-info :status sat)
+(declare-fun a () (_ FloatingPoint 11 53))
+(assert (= (fp.to_real a) 0.0))
+(check-sat)
+