diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 | ||||
| -rw-r--r-- | src/util/bitvector.h | 17 |
2 files changed, 11 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 62afbf987..e4b9023d5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2603,8 +2603,9 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) { case kind::CONST_RATIONAL: { Rational constant = current.getConst<Rational>(); AlwaysAssert(constant.isIntegral()); + AlwaysAssert(constant >= 0); BitVector bv(size, constant.getNumerator()); - if (bv.getValue() != constant.getNumerator()) { + if (bv.toSignedInt() != constant.getNumerator()) { throw TypeCheckingException(current.toExpr(), string("Not enough bits for constant in intToBV: ") + current.toString()); } result = nm->mkConst(bv); diff --git a/src/util/bitvector.h b/src/util/bitvector.h index a04cbb58f..4a74c1c53 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -338,6 +338,15 @@ public: return d_value; } + Integer toSignedInt() const { + // returns Integer corresponding to two's complement interpretation of bv + unsigned size = d_size; + Integer sign_bit = d_value.extractBitRange(1,size-1); + Integer val = d_value.extractBitRange(size-1, 0); + Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; + return res; + } + /** Returns k is the integer is equal to 2^{k-1} and zero otherwise @@ -356,14 +365,6 @@ private: unsigned d_size; Integer d_value; - Integer toSignedInt() const { - // returns Integer corresponding to two's complement interpretation of bv - unsigned size = d_size; - Integer sign_bit = d_value.extractBitRange(1,size-1); - Integer val = d_value.extractBitRange(size-1, 0); - Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; - return res; - } };/* class BitVector */ |