Tolerate three cases of imprecision in value_set_fi

Fixes: #2653

Author: Daniel Kroening

src/pointer-analysis/value_set_fi.cpp

@@ -410,17 +410,18 @@ void value_set_fit::get_value_set_rec(
   {
     const typet &type = to_index_expr(expr).array().type();
 
-    DATA_INVARIANT(type.id()==ID_array ||
-                   type.id()=="#REF#",
-                   "operand 0 of index expression must be an array");
-
-    get_value_set_rec(
-      to_index_expr(expr).array(),
-      dest,
-      "[]" + suffix,
-      original_type,
-      ns,
-      recursion_set);
+    if(type.id() == ID_array)
+    {
+      get_value_set_rec(
+        to_index_expr(expr).array(),
+        dest,
+        "[]" + suffix,
+        original_type,
+        ns,
+        recursion_set);
+    }
+    else
+      insert(dest, exprt(ID_unknown, original_type));
 
     return;
   }
@@ -1192,12 +1193,15 @@ void value_set_fit::assign_rec(
   {
     const typet &type = to_index_expr(lhs).array().type();
 
-    DATA_INVARIANT(type.id()==ID_array ||
-                   type.id()=="#REF#",
-                   "operand 0 of index expression must be an array");
-
-    assign_rec(
-      to_index_expr(lhs).array(), values_rhs, "[]" + suffix, ns, recursion_set);
+    if(type.id() == ID_array)
+    {
+      assign_rec(
+        to_index_expr(lhs).array(),
+        values_rhs,
+        "[]" + suffix,
+        ns,
+        recursion_set);
+    }
   }
   else if(lhs.id()==ID_member)
   {
@@ -1239,9 +1243,9 @@ void value_set_fit::assign_rec(
 
     assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
   }
-  else if(lhs.id()=="zero_string" ||
-          lhs.id()=="is_zero_string" ||
-          lhs.id()=="zero_string_length")
+  else if(
+    lhs.id() == "zero_string" || lhs.id() == "is_zero_string" ||
+    lhs.id() == "zero_string_length" || lhs.id() == ID_address_of)
   {
     // ignore
   }