diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-26 12:41:05 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-26 12:41:05 -0700 |
commit | 77d8df881ec006f9c99a089befcd981af4104a21 (patch) | |
tree | a17250961a770b23e57813e45d0615db96b358ea /src/smt | |
parent | 7f079d6d88fc6e7e5c73eb4bfa9cb42e6930c224 (diff) |
Updated script, fixed bug in QF_NIA conversion.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 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); |