diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-03 16:20:13 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-03 16:20:13 -0800 |
commit | f3d40cc254026805259c511dd706d87a130c807e (patch) | |
tree | 5207abb94e80a577a213dd7455e80c56948c9be5 /src/theory | |
parent | 48ba9401dd647e737b79f1605dc68c44119e5baf (diff) |
Fix corner case in model construction of strings (#3524)
This commit fixes a corner case in the model construction of strings:
For a given length, we were assuming that for each equivalence class, we
could always find an initial guess for a constant to assign to it. This
was not always true, however, because a preceding equivalence class
could use up all constants and get assigned the last remaining one, so
we wouldn't have a constant remaining for the current class. This
resulted in an assertion failure (in debug) or a crash (in production).
This commit fixes the issue by checking whether we've run out of
constants before assigning an initial constant for an equivalence class.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7d10cbadc..df2364790 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -645,11 +645,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) std::map<Node, Node>::iterator itp = pure_eq_assign.find(eqc); if (itp == pure_eq_assign.end()) { - Assert(!sel.isFinished()); - c = *sel; - while (m->hasTerm(c)) + do { - ++sel; if (sel.isFinished()) { // We are in a case where model construction is impossible due to @@ -687,8 +684,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) return false; } c = *sel; - } - ++sel; + ++sel; + } while (m->hasTerm(c)); } else { |