Flattening of ID_nondet_symbol for unbounded arrays

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -182,9 +182,10 @@ void arrayst::collect_arrays(const exprt &a)
   else if(a.id()==ID_member)
   {
     DATA_INVARIANT(
-      to_member_expr(a).struct_op().id()==ID_symbol,
-      ("unexpected array expression: member with `"+
-       a.op0().id_string()+"'").c_str());
+      to_member_expr(a).struct_op().id() == ID_symbol ||
+        to_member_expr(a).struct_op().id() == ID_nondet_symbol,
+      ("unexpected array expression: member with `" + a.op0().id_string() + "'")
+        .c_str());
   }
   else if(a.id()==ID_constant ||
           a.id()==ID_array ||
@@ -458,8 +459,10 @@ void arrayst::add_array_constraints(
           expr.id()==ID_string_constant)
   {
   }
-  else if(expr.id()==ID_member &&
-          to_member_expr(expr).struct_op().id()==ID_symbol)
+  else if(
+    expr.id() == ID_member &&
+    (to_member_expr(expr).struct_op().id() == ID_symbol ||
+     to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
   {
   }
   else if(expr.id()==ID_byte_update_little_endian ||

src/solvers/flattening/boolbv_index.cpp

@@ -51,9 +51,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       // record type if array is a symbol
 
-      if(array.id()==ID_symbol)
-        map.get_map_entry(
-          to_symbol_expr(array).get_identifier(), array_type);
+      if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
+        map.get_map_entry(array.get(ID_identifier), array_type);
 
       // make sure we have the index in the cache
       convert_bv(index);

src/solvers/refinement/string_refinement.cpp

@@ -1120,10 +1120,10 @@ static exprt substitute_array_access(
       *if_expr, index_expr.index(), symbol_generator, left_propagate);
 
   INVARIANT(
-    array.is_nil() || array.id() == ID_symbol,
+    array.is_nil() || array.id() == ID_symbol || array.id() == ID_nondet_symbol,
     std::string(
-      "in case the array is unknown, it should be a symbol or nil, id: ")
-    + id2string(array.id()));
+      "in case the array is unknown, it should be a symbol or nil, id: ") +
+      id2string(array.id()));
   return index_expr;
 }
 
@@ -1693,7 +1693,9 @@ static void initial_index_set(
   const exprt &s,
   const exprt &i)
 {
-  PRECONDITION(s.id() == ID_symbol || s.id() == ID_array || s.id() == ID_if);
+  PRECONDITION(
+    s.id() == ID_symbol || s.id() == ID_nondet_symbol || s.id() == ID_array ||
+    s.id() == ID_if);
   if(s.id() == ID_array)
   {
     for(std::size_t j = 0; j < s.operands().size(); ++j)
@@ -1995,11 +1997,11 @@ exprt string_refinementt::get(const exprt &expr) const
     }
 
     INVARIANT(
-      array.is_nil() || array.id() == ID_symbol,
-      std::string(
-        "apart from symbols, array valuations can be interpreted as "
-        "sparse arrays, id: ") +
-      id2string(array.id()));
+      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()));
     return index_exprt(array, index);
   }