diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-19 18:54:17 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-19 11:54:17 -0500 |
| commit | 1c67e4cc188b4812cedb614e6e998ea944ddb320 (patch) | |
| tree | 0d423f7ff5abbc0ae94549a99d90440567522b99 /src/theory/sets | |
| parent | 41f1a9a0036f3d18ec21ef6005fb218cf704fe60 (diff) | |
Changes assertion (about maximum set cardinality) to an exception. (#4907)
Changes the assertion that checks for the maximum cardinality of set models to an exception, following #4374.
Also cleans up the code around it: previously, the Rational was checked against LONG_MAX, converted to std::uint32_t and then stored into an unsigned. Now we use std::uint32_t all the way.
Fixes #4374.
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/cardinality_extension.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 1c12c71e4..4aa866d27 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -997,9 +997,14 @@ void CardinalityExtension::mkModelValueElementsFor( Node v = val.getModelValue(it->second); Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl; - Assert(v.getConst<Rational>() <= LONG_MAX) - << "Exceeded LONG_MAX in sets model"; - unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt(); + if (v.getConst<Rational>() > UINT32_MAX) + { + std::stringstream ss; + ss << "The model for " << eqc << " was computed to have cardinality " + << v << ". We only allow sets up to cardinality " << UINT32_MAX; + throw LogicException(ss.str()); + } + std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt(); Assert(els.size() <= vu); NodeManager* nm = NodeManager::currentNM(); if (elementType.isInterpretedFinite()) |