diff options
Diffstat (limited to 'src/theory/bv/theory_bv_utils.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index adb067045..fd300fe41 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -467,7 +467,7 @@ Node eliminateBv2Nat(TNode node) { const unsigned size = utils::getSize(node[0]); NodeManager* const nm = NodeManager::currentNM(); - const Node z = nm->mkConst(CONST_RATIONAL, Rational(0)); + const Node z = nm->mkConstInt(Rational(0)); const Node bvone = utils::mkOne(1); Integer i = 1; @@ -478,8 +478,8 @@ Node eliminateBv2Nat(TNode node) nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone); - children.push_back(nm->mkNode( - kind::ITE, cond, nm->mkConst(CONST_RATIONAL, Rational(i)), z)); + children.push_back( + nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z)); } // avoid plus with one child return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children); @@ -496,11 +496,11 @@ Node eliminateInt2Bv(TNode node) Integer i = 2; while (v.size() < size) { - Node cond = nm->mkNode(kind::GEQ, - nm->mkNode(kind::INTS_MODULUS_TOTAL, - node[0], - nm->mkConst(CONST_RATIONAL, Rational(i))), - nm->mkConst(CONST_RATIONAL, Rational(i, 2))); + Node cond = nm->mkNode( + kind::GEQ, + nm->mkNode( + kind::INTS_MODULUS_TOTAL, node[0], nm->mkConstInt(Rational(i))), + nm->mkConstInt(Rational(i, 2))); v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); i *= 2; } |