diff options
Diffstat (limited to 'src/theory/strings/regexp_entail.cpp')
| -rw-r--r-- | src/theory/strings/regexp_entail.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 530f34455..c9d890358 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -574,7 +574,7 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, } else { - Node num2 = nm->mkConst(cvc5::Rational(u - 1)); + Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(u - 1)); Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2); if (testConstStringInRegExp(s, index_start + len, r2)) { @@ -606,7 +606,7 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, cvc5::String t = s.substr(index_start, len); if (testConstStringInRegExp(t, 0, r[0])) { - Node num2 = nm->mkConst(cvc5::Rational(l - 1)); + Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(l - 1)); Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2); if (testConstStringInRegExp(s, index_start + len, r2)) { @@ -657,7 +657,7 @@ Node RegExpEntail::getFixedLengthForRegexp(Node n) } else if (n.getKind() == REGEXP_ALLCHAR || n.getKind() == REGEXP_RANGE) { - return nm->mkConst(Rational(1)); + return nm->mkConst(CONST_RATIONAL, Rational(1)); } else if (n.getKind() == REGEXP_UNION || n.getKind() == REGEXP_INTER) { |