From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 4 Dec 2019 00:20:13 +0000 (-0800)
Subject: Fix corner case in model construction of strings (#3524)
X-Git-Tag: cvc5-1.0.0~3803
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f3d40cc254026805259c511dd706d87a130c807e;p=cvc5.git

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 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
         {