fixup! Correct find_index function for if-expressions

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -2097,6 +2097,7 @@ static void update_index_set(
 /// Finds an index on `str` used in `expr` that contains `qvar`, for instance
 /// with arguments ``(str[k]=='a')``, `str`, and `k`, the function should
 /// return `k`.
+/// If two different such indexes exist, an invariant will fail.
 /// \param [in] expr: the expression to search
 /// \param [in] str: the string which must be indexed
 /// \param [in] qvar: the universal variable that must be in the index
@@ -2105,21 +2106,38 @@ static void update_index_set(
 static optionalt<exprt>
 find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 {
-  const auto it = std::find_if(
-    expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
-      if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
-      {
-        const auto &arr = index_expr->array();
-        const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
-        return str_it != arr.depth_end() &&
-               find_qvar(index_expr->index(), qvar);
-      }
-      return false;
-    });
+  auto index_str_containing_qvar = [&](const exprt &e) { // NOLINT
+    if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
+    {
+      const auto &arr = index_expr->array();
+      const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
+      return str_it != arr.depth_end() && find_qvar(index_expr->index(), qvar);
+    }
+    return false;
+  };
+
+  auto it = std::find_if(
+    expr.depth_begin(), expr.depth_end(), index_str_containing_qvar);
+  if(it == expr.depth_end())
+    return {};
+  const exprt &index = to_index_expr(*it).index();
+
+  // Check that there are no two such indexes
+  it.next_sibling_or_parent();
+  while(it != expr.depth_end())
+  {
+    if(index_str_containing_qvar(*it))
+    {
+      INVARIANT(
+        to_index_expr(*it).index() == index,
+        "string should always be indexed by same value in a given formula");
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
 
-  if(it != expr.depth_end())
-    return to_index_expr(*it).index();
-  return {};
+  return index;
 }
 
 /// Instantiates a string constraint by substituting the quantifiers.