Rename size to L2 in field_sensitivity::apply

This is to allow constant propagation to take place and know whether the
size is actually constant, which can allow field sensitivity to apply.

Author: romainbrenguier

src/goto-symex/field_sensitivity.cpp

@@ -97,21 +97,21 @@ exprt field_sensitivityt::apply(
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
       bool was_l2 = !tmp.get_level_2().empty();
-
-      exprt array_size_expr = to_array_type(l2_array.get().type()).size();
-      if(array_size_expr.is_nil() && index.array().id() == ID_symbol)
+      exprt l2_size =
+        state.rename(to_array_type(index.array().type()).size(), ns).get();
+      if(l2_size.is_nil() && index.array().id() == ID_symbol)
       {
         // In case the array type was incomplete, attempt to retrieve it from
         // the symbol table.
         const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
           to_symbol_expr(index.array()).get_identifier());
         if(array_from_symbol_table != nullptr)
-          array_size_expr = to_array_type(array_from_symbol_table->type).size();
+          l2_size = to_array_type(array_from_symbol_table->type).size();
       }
 
       if(
-        array_size_expr.id() == ID_constant &&
-        numeric_cast_v<mp_integer>(to_constant_expr(array_size_expr)) <=
+        l2_size.id() == ID_constant &&
+        numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
           max_field_sensitive_array_size &&
         index.id() == ID_constant)
       {