diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp
index 7f2c53dfe48..ecde976f4eb 100644
--- a/src/util/fresh_symbol.cpp
+++ b/src/util/fresh_symbol.cpp
@@ -17,7 +17,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include "symbol.h"
 #include "symbol_table_base.h"
 
-/// Installs a fresh-named symbol with the requested name pattern.
+/// Installs a fresh-named symbol with respect to the given namespace `ns` with
+/// the requested name pattern in the given symbol table
 /// \param type: The type of the new symbol.
 /// \param name_prefix: The new symbol will be named
 ///   `name_prefix::basename_prefix$num` unless name_prefix is empty, in which
@@ -25,6 +26,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// \param basename_prefix: See `name_prefix`.
 /// \param source_location: The source location for the new symbol.
 /// \param symbol_mode: The mode for the new symbol, e.g. ID_C, ID_java.
+/// \param ns: the new symbol has a different name than any symbols in `ns`
 /// \param symbol_table: The symbol table to add the new symbol to.
 /// \return The new symbol.
 symbolt &get_fresh_aux_symbol(
@@ -33,9 +35,9 @@ symbolt &get_fresh_aux_symbol(
   const std::string &basename_prefix,
   const source_locationt &source_location,
   const irep_idt &symbol_mode,
+  const namespacet &ns,
   symbol_table_baset &symbol_table)
 {
-  namespacet ns(symbol_table);
   irep_idt identifier = basename_prefix;
   std::size_t prefix_size = 0;
   if(!name_prefix.empty())
@@ -55,3 +57,32 @@ symbolt &get_fresh_aux_symbol(
 
   return res.first;
 }
+
+/// Installs a fresh-named symbol with the requested name pattern in the given
+/// symbol table
+/// \param type: The type of the new symbol.
+/// \param name_prefix: The new symbol will be named
+///   `name_prefix::basename_prefix$num` unless name_prefix is empty, in which
+///   case the :: prefix is omitted.
+/// \param basename_prefix: See `name_prefix`.
+/// \param source_location: The source location for the new symbol.
+/// \param symbol_mode: The mode for the new symbol, e.g. ID_C, ID_java.
+/// \param symbol_table: The symbol table to add the new symbol to.
+/// \return The new symbol.
+symbolt &get_fresh_aux_symbol(
+  const typet &type,
+  const std::string &name_prefix,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &symbol_mode,
+  symbol_table_baset &symbol_table)
+{
+  return get_fresh_aux_symbol(
+    type,
+    name_prefix,
+    basename_prefix,
+    source_location,
+    symbol_mode,
+    namespacet(symbol_table),
+    symbol_table);
+}
diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h
index 0d1601ad180..0bab21812be 100644
--- a/src/util/fresh_symbol.h
+++ b/src/util/fresh_symbol.h
@@ -16,6 +16,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include "irep.h"
 
+class namespacet;
 class source_locationt;
 class symbolt;
 class symbol_table_baset;
@@ -29,4 +30,13 @@ symbolt &get_fresh_aux_symbol(
   const irep_idt &symbol_mode,
   symbol_table_baset &symbol_table);
 
+symbolt &get_fresh_aux_symbol(
+  const typet &type,
+  const std::string &name_prefix,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &symbol_mode,
+  const namespacet &ns,
+  symbol_table_baset &symbol_table);
+
 #endif // CPROVER_UTIL_FRESH_SYMBOL_H