diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-26 00:22:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-26 00:22:57 -0500 |
commit | 28867b06a05fc13d0257093fcd28caa5907317b6 (patch) | |
tree | d6e0db315a168c112aadec5fe3c8d34c0e59deb5 /src/theory/strings/regexp_operation.cpp | |
parent | b70ccff4de0a23bdf11c70002d10a2cc0795a91c (diff) |
Fix unsigned integer type issues in strings (#2380)
* Fix unsigned integer types in strings.
* Format
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) { |