From f3d40cc254026805259c511dd706d87a130c807e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 3 Dec 2019 16:20:13 -0800 Subject: 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. --- src/theory/strings/theory_strings.cpp | 9 +++------ 1 file 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::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 { -- cgit v1.2.3