diff options
Diffstat (limited to 'src/theory/strings')
| -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 { |