projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 41f1a9a) | patch
Changes assertion (about maximum set cardinality) to an exception. (#4907)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 19 Aug 2020 16:54:17 +0000 (18:54 +0200)
committerGitHub <noreply@github.com>
Wed, 19 Aug 2020 16:54:17 +0000 (11:54 -0500)
commit1c67e4cc188b4812cedb614e6e998ea944ddb320
tree0d423f7ff5abbc0ae94549a99d90440567522b99tree
parent41f1a9a0036f3d18ec21ef6005fb218cf704fe60commit | 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.
src/theory/sets/cardinality_extension.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
test/regress/regress0/strings/large-model.smt2 diff | blob | history