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.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7d10cbadc0acae33dd6135bfa2a115030c4806cf..df236479057a84dfa626a1b1a4bab05a7be0d960 100644 (file)
--- 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
         {