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 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,31 @@ static void update_index_set(
 static optionalt<exprt>
 find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 {
+  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;
+  };
+
   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;
-    });
+    expr.depth_begin(), expr.depth_end(), index_str_containing_qvar);
+  if(it == expr.depth_end())
+    return {};
+
+  // Check that there are no two such indexes
+  auto next_it = it;
+  next_it.next_sibling_or_parent();
+  bool has_second_index =
+    std::find_if(next_it, expr.depth_end(), index_str_containing_qvar)
+    != expr.depth_end();
+  INVARIANT(
+    !has_second_index, "string should only be indexed once in a given formula");
 
-  if(it != expr.depth_end())
-    return to_index_expr(*it).index();
-  return {};
+  return to_index_expr(*it).index();
 }
 
 /// Instantiates a string constraint by substituting the quantifiers.