diff --git a/regression/goto-cc-file-local/child-symbols-mangled/file1.c b/regression/goto-cc-file-local/child-symbols-mangled/file1.c
new file mode 100644
index 00000000000..fe5a1e24198
--- /dev/null
+++ b/regression/goto-cc-file-local/child-symbols-mangled/file1.c
@@ -0,0 +1,5 @@
+#include "lib.h"
+int caller1(int a)
+{
+  return helper(a);
+}
diff --git a/regression/goto-cc-file-local/child-symbols-mangled/file2.c b/regression/goto-cc-file-local/child-symbols-mangled/file2.c
new file mode 100644
index 00000000000..c12cc894eb8
--- /dev/null
+++ b/regression/goto-cc-file-local/child-symbols-mangled/file2.c
@@ -0,0 +1,5 @@
+#include "lib.h"
+int caller2(int b)
+{
+  return helper(b);
+}
diff --git a/regression/goto-cc-file-local/child-symbols-mangled/lib.h b/regression/goto-cc-file-local/child-symbols-mangled/lib.h
new file mode 100644
index 00000000000..15a7783dec7
--- /dev/null
+++ b/regression/goto-cc-file-local/child-symbols-mangled/lib.h
@@ -0,0 +1,9 @@
+// A file-local function defined in a shared header: when two translation
+// units include it and are compiled with --export-file-local-symbols, both
+// mangle `helper` to the same __CPROVER_file_local_lib_h_helper name.  Its
+// parameter symbol (helper::x) must be mangled in lockstep, otherwise the
+// two TUs carry identically-named parameter symbols that clash at link time.
+static int helper(int x)
+{
+  return x + 1;
+}
diff --git a/regression/goto-cc-file-local/child-symbols-mangled/test.desc b/regression/goto-cc-file-local/child-symbols-mangled/test.desc
new file mode 100644
index 00000000000..a042a967247
--- /dev/null
+++ b/regression/goto-cc-file-local/child-symbols-mangled/test.desc
@@ -0,0 +1,8 @@
+CORE
+file1.c
+final-link show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+__CPROVER_file_local_lib_h_helper::x
+--
+^warning: ignoring
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h
index ebcdab0f62d..0c9d9971ce3 100644
--- a/src/goto-programs/name_mangler.h
+++ b/src/goto-programs/name_mangler.h
@@ -83,10 +83,71 @@ class function_name_manglert
       log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom;
     }
 
+    // Second pass: rename scoped child symbols of renamed
+    // functions.  Parameter symbols and function-local
+    // variables are stored in the symbol table under names of
+    // the form `<function_name>::<base_name>` (and longer
+    // scope chains for nested locals).  Without renaming
+    // these, two translation units that include the same
+    // kernel header end up with identically-named parameter
+    // symbols (e.g. `security_netlink_send::sk` from both
+    // TUs); the linker then either accepts them with a
+    // `$link1` suffix on one (unifying the function symbol
+    // under its external name) or rejects them as
+    // 'conflicting function declarations' depending on
+    // whether the parameter types match exactly.  The fix is
+    // to rename child symbols in lockstep with the parent
+    // function so the per-TU mangling is complete.
+    std::vector<symbolt> new_child_syms;
+    std::vector<symbol_tablet::symbolst::const_iterator> old_child_syms;
+    for(auto sym_it = model.symbol_table.symbols.begin();
+        sym_it != model.symbol_table.symbols.end();
+        ++sym_it)
+    {
+      const std::string sym_name = id2string(sym_it->first);
+      // Skip the function symbols themselves; they were
+      // handled above and any name match here would already be
+      // in `renamed_funs`.
+      if(renamed_funs.find(sym_it->first) != renamed_funs.end())
+        continue;
+
+      for(const auto &pair : renamed_funs)
+      {
+        const std::string old_prefix = id2string(pair.first) + "::";
+        if(sym_name.compare(0, old_prefix.size(), old_prefix) != 0)
+          continue;
+
+        const irep_idt new_name =
+          id2string(pair.second) + "::" + sym_name.substr(old_prefix.size());
+        symbolt new_child = sym_it->second;
+        new_child.name = new_name;
+        // Clear file_local on the child symbols too: the parent
+        // function has just transitioned from file-local to
+        // globally-mangled and unifiable, and the linker's
+        // file-local renaming rule (RENAME_NEW for any
+        // file_local symbol it sees on the new side of a link)
+        // would otherwise force `$link1` suffixes on each
+        // duplicate child symbol — defeating the unification we
+        // just set up.  The new mangled name is unique across
+        // TUs that share the header but should unify cleanly
+        // when two TUs include the SAME header (because both
+        // ends of the link produce identical mangled names).
+        new_child.is_file_local = false;
+        new_child_syms.push_back(new_child);
+        old_child_syms.push_back(sym_it);
+        rename.insert(sym_it->second.symbol_expr(), new_child.symbol_expr());
+        break;
+      }
+    }
+
     for(const auto &sym : new_syms)
       model.symbol_table.insert(sym);
     for(const auto &sym : old_syms)
       model.symbol_table.erase(sym);
+    for(const auto &sym : new_child_syms)
+      model.symbol_table.insert(sym);
+    for(const auto &sym : old_child_syms)
+      model.symbol_table.erase(sym);
 
     for(auto it = model.symbol_table.begin(); it != model.symbol_table.end();
         ++it)