diff options
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) { |