diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-27 08:14:19 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-27 08:14:19 -0700 |
| commit | 8f8d2193277d75c7b3631af235b0a23de7f04926 (patch) | |
| tree | 24f7b6b2c1e28b988f4ddd61f9761777caebf487 /src/theory/strings/theory_strings.cpp | |
| parent | 0b82388e10cbb2ae7fc2f2c81ee643c5dd6f2605 (diff) | |
| parent | 9f9f8d29c9428289492e421fc1c464a51a06977e (diff) | |
Merge branch 'master' into rmCoverityrmCoverity
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ce0100686..72e82edca 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -103,7 +103,6 @@ TheoryStrings::TheoryStrings(context::Context* c, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), - RMAXINT(LONG_MAX), d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), d_conflict(c, false), @@ -536,7 +535,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl; if( lts[i].isConst() ) { lts_values.push_back( lts[i] ); - Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -545,7 +545,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Node v = d_valuation.getModelValue(lts[i]); Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; lts_values.push_back( v ); - Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(v.getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -621,7 +622,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << std::endl; //use type enumerator - Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); for (const Node& eqc : pure_eq) { |