diff --git a/regression/cbmc/struct17/main.c b/regression/cbmc/struct17/main.c
new file mode 100644
index 00000000000..892cef000b9
--- /dev/null
+++ b/regression/cbmc/struct17/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct famt
+{
+  char x;
+  char vl[];
+};
+
+extern struct famt vls;
+struct famt vls = {'a', {1, 2, 3, 4}};
+
+int main()
+{
+  assert(vls.vl[3] == 4);
+  return 0;
+}
diff --git a/regression/cbmc/struct17/test.desc b/regression/cbmc/struct17/test.desc
new file mode 100644
index 00000000000..659a36aac28
--- /dev/null
+++ b/regression/cbmc/struct17/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index efc5cbd787f..a330416b2b5 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -262,6 +262,41 @@ void c_typecheck_baset::typecheck_redefinition_type(
   }
 }
 
+static bool is_instantiation_of_flexible_array(
+  const struct_typet &old_type,
+  const struct_typet &new_type)
+{
+  const struct_typet::componentst &old_components = old_type.components();
+  const struct_typet::componentst &new_components = new_type.components();
+
+  if(old_components.size() != new_components.size())
+    return false;
+
+  if(old_components.empty())
+    return false;
+
+  for(std::size_t i = 0; i < old_components.size() - 1; ++i)
+  {
+    if(old_components[i].type() != new_components[i].type())
+      return false;
+  }
+
+  if(
+    old_components.back().type().id() != ID_array ||
+    new_components.back().type().id() != ID_array)
+  {
+    return false;
+  }
+
+  const auto &old_array_type = to_array_type(old_components.back().type());
+  const auto &new_array_type = to_array_type(new_components.back().type());
+
+  return old_array_type.element_type() == new_array_type.element_type() &&
+         old_array_type.get_bool(ID_C_flexible_array_member) &&
+         new_array_type.get_bool(ID_C_flexible_array_member) &&
+         (old_array_type.size().is_nil() || old_array_type.size().is_zero());
+}
+
 void c_typecheck_baset::typecheck_redefinition_non_type(
   symbolt &old_symbol,
   symbolt &new_symbol)
@@ -446,6 +481,13 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
       // int (*f) (int)=0;
       // int (*f) ();
     }
+    else if(
+      final_old.id() == ID_struct && final_new.id() == ID_struct &&
+      is_instantiation_of_flexible_array(
+        to_struct_type(final_old), to_struct_type(final_new)))
+    {
+      old_symbol.type = new_symbol.type;
+    }
     else
     {
       error().source_location=new_symbol.location;
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index 6a8492275c0..d5dc9853f09 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/src/ansi-c/goto_check_c.cpp
@@ -1638,14 +1638,14 @@ void goto_check_ct::bounds_check_index(
     // that member, it behaves as if that member were replaced with the longest
     // array (with the same element type) that would not make the structure
     // larger than the object being accessed; [...]
-    const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
+    const auto type_size_opt =
+      pointer_offset_size(ode.root_object().type(), ns);
     CHECK_RETURN(type_size_opt.has_value());
 
     binary_relation_exprt inequality(
-      typecast_exprt::conditional_cast(
-        ode.offset(), type_size_opt.value().type()),
+      ode.offset(),
       ID_lt,
-      type_size_opt.value());
+      from_integer(type_size_opt.value(), ode.offset().type()));
 
     add_guarded_property(
       inequality,