Merge pull request #3785 from tautschnig/deprecation-array_list_exprt

Construct array_list_exprt in a non-deprecated way

Author: Daniel Kroening

src/solvers/flattening/boolbv_get.cpp

@@ -361,7 +361,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
 
   if(size_mpint>100 || size.id()==ID_infinity)
   {
-    result = array_list_exprt(to_array_type(type));
+    result = array_list_exprt({}, to_array_type(type));
     result.type().set(ID_size, integer2string(size_mpint));
 
     result.operands().reserve(values.size()*2);

src/util/std_expr.h

@@ -1796,6 +1796,11 @@ class array_list_exprt : public multi_ary_exprt
     : multi_ary_exprt(ID_array_list, _type)
   {
   }
+
+  array_list_exprt(operandst &&_operands, const array_typet &_type)
+    : multi_ary_exprt(ID_array_list, std::move(_operands), _type)
+  {
+  }
 };
 
 template <>

unit/solvers/refinement/string_refinement/substitute_array_list.cpp

@@ -21,16 +21,16 @@ SCENARIO("substitute_array_list",
   const typet char_type=unsignedbv_typet(16);
   const typet int_type=signedbv_typet(32);
   const array_typet array_type(char_type, infinity_exprt(int_type));
-  array_list_exprt arr(array_type);
   const exprt index0=from_integer(0, int_type);
   const exprt charx=from_integer('x', char_type);
   const exprt index1=from_integer(1, int_type);
   const exprt chary=from_integer('y', char_type);
   const exprt index100=from_integer(100, int_type);
 
   // arr is `array-list [ 0 , 'x' , 1 , 'y' , 2 , 'z']`
-  arr.operands()=
-    { index0, charx, index1, chary, index100, from_integer('z', char_type) };
+  array_list_exprt arr(
+    {index0, charx, index1, chary, index100, from_integer('z', char_type)},
+    array_type);
 
   // Max length is 2, so index 2 should get ignored.
   const exprt subst=substitute_array_lists(arr, 2);