diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 9d51bca80e8..6a3f6daf9fa 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -456,6 +456,23 @@ void c_typecastt::implicit_typecast(
   implicit_typecast_followed(expr, src_type, type_qual, dest_type);
 }
 
+static bool is_array_element_alias(const namespacet& ns, const symbolt* const orig_symbol, const typet &src_type, const typet &dest_type)
+{
+  if(orig_symbol==nullptr)
+    return false;
+  const symbolt* aliased_symbol;
+  if(ns.lookup(orig_symbol->name, aliased_symbol))
+    return false;
+  if(!aliased_symbol->is_macro)
+    return false;
+  if(src_type.id()!=ID_array)
+    return false;
+  const typet &src_subtype=ns.follow(src_type.subtype());
+  if(src_subtype!=dest_type)
+    return false;
+  return true;
+}
+
 void c_typecastt::implicit_typecast_followed(
   exprt &expr,
   const typet &src_type,
@@ -569,7 +586,7 @@ void c_typecastt::implicit_typecast_followed(
     }
   }
 
-  if(check_c_implicit_typecast(src_type, dest_type))
+  if(check_c_implicit_typecast(src_type, dest_type) && !is_array_element_alias(ns, get_current_symbol(), src_type, dest_type))
     errors.push_back("implicit conversion not permitted");
   else if(src_type!=dest_type)
     do_typecast(expr, orig_dest_type);
diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h
index 11e379f3935..75db13ece88 100644
--- a/src/ansi-c/c_typecast.h
+++ b/src/ansi-c/c_typecast.h
@@ -41,7 +41,7 @@ bool c_implicit_typecast_arithmetic(
 class c_typecastt
 {
 public:
-  explicit c_typecastt(const namespacet &_ns):ns(_ns)
+  explicit c_typecastt(const namespacet &_ns):ns(_ns), current_symbol(nullptr)
   {
   }
 
@@ -63,6 +63,9 @@ class c_typecastt
   std::list<std::string> errors;
   std::list<std::string> warnings;
 
+  void set_current_symbol(const symbolt * const symbol) { current_symbol=symbol; }
+  const symbolt *get_current_symbol() const { return current_symbol; }
+
 protected:
   const namespacet &ns;
 
@@ -100,6 +103,9 @@ class c_typecastt
   void do_typecast(exprt &dest, const typet &type);
 
   c_typet minimum_promotion(const typet &type) const;
+
+private:
+  const symbolt *current_symbol;
 };
 
 #endif // CPROVER_ANSI_C_C_TYPECAST_H
diff --git a/src/ansi-c/c_typecheck_typecast.cpp b/src/ansi-c/c_typecheck_typecast.cpp
index 2ce03d83f18..0672d1019d2 100644
--- a/src/ansi-c/c_typecheck_typecast.cpp
+++ b/src/ansi-c/c_typecheck_typecast.cpp
@@ -15,6 +15,7 @@ void c_typecheck_baset::implicit_typecast(
   const typet &dest_type)
 {
   c_typecastt c_typecast(*this);
+  c_typecast.set_current_symbol(&current_symbol);
 
   typet src_type=expr.type();