Flattening of ID_nondet_symbol for unbounded arrays

symbol_exprt and nondet_symbol_exprt are to be treated the same when in comes to
the back-end: they both introduce an uninterpreted, nullary function. Note the
difference at the level of symbolic execution/programs, where the value of
symbols may change (while the value of nondet_symbol_exprts cannot).

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -180,9 +180,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 ||
@@ -450,8 +451,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/strings/string_refinement.cpp

@@ -1127,7 +1127,7 @@ 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()));
@@ -1700,7 +1700,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)
@@ -2002,7 +2004,8 @@ exprt string_refinementt::get(const exprt &expr) const
     }
 
     INVARIANT(
-      array.is_nil() || array.id() == ID_symbol,
+      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()));