Handle nil case in string_refinementt::get

If the underlying solver does not know about the existence of an array,
it can return nil, which shouldn't be returned inside an
index_expression as in particular the type will be broken.

Author: romainbrenguier

src/solvers/strings/string_refinement.cpp

@@ -2060,6 +2060,12 @@ exprt string_refinementt::get(const exprt &expr) const
     }
     const auto array = supert::get(current.get());
     const auto index = get(index_expr->index());
+
+    // If the underlying solver does not know about the existence of an array,
+    // it can return nil, which cannot be used in the expression returned here.
+    if(array.is_nil())
+      return index_exprt(current, index);
+
     const exprt unknown =
       from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type());
     if(
@@ -2070,12 +2076,9 @@ exprt string_refinementt::get(const exprt &expr) const
       return sparse_array->to_if_expression(index);
     }
 
-    INVARIANT(
-      array.is_nil() || array.id() == ID_symbol ||
-        array.id() == ID_nondet_symbol,
-      std::string("apart from symbols, array valuations can be interpreted as "
-                  "sparse arrays, id: ") +
-        id2string(array.id()));
+    INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
+              "Apart from symbols, array valuations can be interpreted as "
+              "sparse arrays. Array model : " + array.pretty());
     return index_exprt(array, index);
   }