diff --git a/regression/goto-cc-file-local/base-name-1/file1.c b/regression/goto-cc-file-local/base-name-1/file1.c
new file mode 100644
index 00000000000..3cdccb87301
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-1/file1.c
@@ -0,0 +1,7 @@
+int __CPROVER_file_local_file2_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_file2_c_foo(1);
+  __CPROVER_assert(x == 2, "x == 2");
+}
diff --git a/regression/goto-cc-file-local/base-name-1/file2.c b/regression/goto-cc-file-local/base-name-1/file2.c
new file mode 100644
index 00000000000..d8031af5eba
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-1/file2.c
@@ -0,0 +1,9 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}
diff --git a/regression/goto-cc-file-local/base-name-1/test.desc b/regression/goto-cc-file-local/base-name-1/test.desc
new file mode 100644
index 00000000000..2b4d4092811
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-1/test.desc
@@ -0,0 +1,13 @@
+CORE
+file1.c
+final-link show-symbol-table assertion-check
+^Base name\.\.\.: __CPROVER_file_local_.*_foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: foo$
+--
+The linking order must not affect the base name of the mangled symbol. See
+base-name-2 for a test that will yield a different linking order (while still
+producing the same base name).
diff --git a/regression/goto-cc-file-local/base-name-2/file1.c b/regression/goto-cc-file-local/base-name-2/file1.c
new file mode 100644
index 00000000000..d8031af5eba
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-2/file1.c
@@ -0,0 +1,9 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}
diff --git a/regression/goto-cc-file-local/base-name-2/file2.c b/regression/goto-cc-file-local/base-name-2/file2.c
new file mode 100644
index 00000000000..81b647d5f83
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-2/file2.c
@@ -0,0 +1,7 @@
+int __CPROVER_file_local_file1_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_file1_c_foo(1);
+  __CPROVER_assert(x == 2, "x == 2");
+}
diff --git a/regression/goto-cc-file-local/base-name-2/test.desc b/regression/goto-cc-file-local/base-name-2/test.desc
new file mode 100644
index 00000000000..e2e8684025b
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-2/test.desc
@@ -0,0 +1,13 @@
+CORE
+file1.c
+final-link show-symbol-table assertion-check
+^Base name\.\.\.: __CPROVER_file_local_.*_foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: foo$
+--
+The linking order must not affect the base name of the mangled symbol. See
+base-name-1 for a test that will yield a different linking order (while still
+producing the same base name).
diff --git a/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
index bf698744a96..b856adf9f18 100644
--- a/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
+++ b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
@@ -1,11 +1,10 @@
 CORE
 test.c
 --reachable-functions
-^.* foo 1 4$
+^.* __CPROVER_file_local_project_c_foo 1 4$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^.* [a-zA-Z0-9_]+foo \d+ \d+$
 --
 This test checks that after building the goto binary (see test.sh) with
 --export-file-local-symbols function "foo" is still reported as reachable. Note,
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h
index ab6382a834d..df206bfbb63 100644
--- a/src/goto-programs/name_mangler.h
+++ b/src/goto-programs/name_mangler.h
@@ -70,6 +70,9 @@ class function_name_manglert
       symbolt new_sym;
       new_sym = sym;
       new_sym.name = mangled;
+      new_sym.base_name = mangled;
+      if(new_sym.pretty_name.empty())
+        new_sym.pretty_name = sym.base_name;
       new_sym.is_file_local = false;
 
       new_syms.push_back(new_sym);