diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 477e99b9b..3faa63df5 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -34,7 +34,7 @@ RegExpOpr::RegExpOpr() std::vector<Node>{})), d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), - RMAXINT(LONG_MAX), + d_rMaxInt(UINT32_MAX), d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, std::vector<Node>{})), d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) @@ -1137,7 +1137,8 @@ bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) { bool RegExpOpr::containC2(unsigned cnt, Node n) { if(n.getKind() == kind::REGEXP_RV) { - Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); + Assert(n[0].getConst<Rational>() <= d_rMaxInt, + "Exceeded UINT32_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); return cnt == y; } else if(n.getKind() == kind::REGEXP_CONCAT) { @@ -1178,7 +1179,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { r1 = d_emptySingleton; r2 = d_emptySingleton; } else if(n.getKind() == kind::REGEXP_RV) { - Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::convert2"); + Assert(n[0].getConst<Rational>() <= d_rMaxInt, + "Exceeded UINT32_MAX in RegExpOpr::convert2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); r1 = d_emptySingleton; if(cnt == y) { |