diff options
Diffstat (limited to 'src/theory/strings/strings_entail.cpp')
| -rw-r--r-- | src/theory/strings/strings_entail.cpp | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 3b90338fc..6e4ba25a5 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -123,7 +123,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1, Assert(dir == 1 || dir == -1); Assert(nr.empty()); NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConst(cvc5::Rational(0)); + Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0)); bool ret = false; bool success = true; unsigned sindex = 0; @@ -145,7 +145,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1, Assert(d_arithEntail.check(curr, true)); Node s = n1[sindex_use]; size_t slen = Word::getLength(s); - Node ncl = nm->mkConst(cvc5::Rational(slen)); + Node ncl = nm->mkConst(CONST_RATIONAL, cvc5::Rational(slen)); Node next_s = nm->mkNode(MINUS, lowerBound, ncl); next_s = d_rr->rewrite(next_s); Assert(next_s.isConst()); @@ -459,8 +459,10 @@ bool StringsEntail::componentContainsBase( } if (dir != -1) { - n1rb = nm->mkNode( - STRING_SUBSTR, n2[0], nm->mkConst(Rational(0)), start_pos); + n1rb = nm->mkNode(STRING_SUBSTR, + n2[0], + nm->mkConst(CONST_RATIONAL, Rational(0)), + start_pos); } if (dir != 1) { @@ -712,7 +714,7 @@ bool StringsEntail::checkNonEmpty(Node a) bool StringsEntail::checkLengthOne(Node s, bool strict) { NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(Rational(1)); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); Node len = nm->mkNode(STRING_LENGTH, s); len = d_rr->rewrite(len); return d_arithEntail.check(one, len) |