diff options
-rw-r--r-- | src/util/floatingpoint.cpp | 17 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue3619.smt2 | 7 |
3 files changed, 22 insertions, 3 deletions
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 1b1bfddc2..3bcf2b0de 100644 --- 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 5a59f2f54..fbf249e7f 100644 --- 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 index 000000000..9d6e0a36d --- /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) + |