diff --git a/regression/cbmc/constructor1/main.c b/regression/cbmc/constructor1/main.c
index 8936ecd76d0..305bc104cab 100644
--- a/regression/cbmc/constructor1/main.c
+++ b/regression/cbmc/constructor1/main.c
@@ -1,11 +1,12 @@
 #include <assert.h>
 
 #ifdef __GNUC__
-int x, y;
+int x, y, z;
 
 // forward declaration with and without attribute is ok
 static __attribute__((constructor)) void format_init(void);
 static void other_init(void);
+static __attribute__((constructor)) void more_init(void);
 
 static __attribute__((constructor))
 void format_init(void)
@@ -18,6 +19,11 @@ static __attribute__((constructor)) void other_init(void)
 {
   y = 42;
 }
+
+static void more_init(void)
+{
+  z = 42;
+}
 #endif
 
 int main()
@@ -25,6 +31,7 @@ int main()
 #ifdef __GNUC__
   assert(x==42);
   assert(y == 42);
+  assert(z == 42);
 #endif
   return 0;
 }
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 93a581747e5..0b7bcb42b69 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -379,12 +379,21 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
       new_ct.return_type().id() != ID_constructor &&
       new_ct.return_type().id() != ID_destructor)
     {
-      throw invalid_source_file_exceptiont{
-        "function symbol '" + id2string(new_symbol.display_name()) +
-          "' redefined with a different type:\n" +
-          "Original: " + to_string(old_symbol.type) + "\n" +
-          "     New: " + to_string(new_symbol.type),
-        new_symbol.location};
+      if(
+        old_ct.return_type().id() == ID_constructor ||
+        old_ct.return_type().id() == ID_destructor)
+      {
+        new_ct = old_ct;
+      }
+      else
+      {
+        throw invalid_source_file_exceptiont{
+          "function symbol '" + id2string(new_symbol.display_name()) +
+            "' redefined with a different type:\n" +
+            "Original: " + to_string(old_symbol.type) + "\n" +
+            "     New: " + to_string(new_symbol.type),
+          new_symbol.location};
+      }
     }
     const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();