diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index f772a0ea9b7..9b7d88d2bfb 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -43,8 +43,8 @@ static const symbolt &c_new_tmp_symbol(
   const bool static_lifetime,
   const std::string &prefix="tmp")
 {
-  symbolt &tmp_symbol=
-    get_fresh_aux_symbol(type, "", prefix, loc, ID_C, symbol_table);
+  symbolt &tmp_symbol = get_fresh_aux_symbol(
+    type, id2string(loc.get_function()), prefix, loc, ID_C, symbol_table);
   tmp_symbol.is_static_lifetime=static_lifetime;
 
   return tmp_symbol;
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index a33b0934349..5f40b8e35c5 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -250,7 +250,7 @@ const symbolt &code_contractst::new_tmp_symbol(
 {
   return get_fresh_aux_symbol(
     type,
-    "",
+    id2string(source_location.get_function()),
     "tmp_cc",
     source_location,
     irep_idt(),
diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp
index 56215c07cd1..30fdca79ddf 100644
--- a/src/goto-programs/convert_nondet.cpp
+++ b/src/goto-programs/convert_nondet.cpp
@@ -17,6 +17,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 #include <java_bytecode/java_object_factory.h> // gen_nondet_init
 
 #include <util/irep_ids.h>
+#include <util/fresh_symbol.h>
 
 #include <memory>
 
@@ -135,11 +136,13 @@ void convert_nondet(
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
+  object_factory_parameterst parameters = object_factory_parameters;
+  parameters.function_id = function.get_function_id();
   convert_nondet(
     function.get_goto_function().body,
     function.get_symbol_table(),
     message_handler,
-    object_factory_parameters);
+    parameters);
 
   function.compute_location_numbers();
 }
@@ -158,6 +161,8 @@ void convert_nondet(
 
     if(symbol.mode==ID_java)
     {
+      object_factory_parameterst parameters = object_factory_parameters;
+      parameters.function_id = f_it.first;
       convert_nondet(
         f_it.second.body,
         symbol_table,
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 4c5541a0108..e74833815c4 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -34,7 +34,6 @@ class goto_convertt:public messaget
     messaget(_message_handler),
     symbol_table(_symbol_table),
     ns(_symbol_table),
-    temporary_counter(0),
     tmp_symbol_prefix("goto_convertt")
   {
   }
@@ -46,7 +45,6 @@ class goto_convertt:public messaget
 protected:
   symbol_table_baset &symbol_table;
   namespacet ns;
-  unsigned temporary_counter;
   std::string tmp_symbol_prefix;
 
   void goto_convert_rec(const codet &code, goto_programt &dest);
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index f4edab30c47..6d6b2b7441e 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -147,8 +147,6 @@ void goto_convert_functionst::convert_function(
 
   // make tmp variables local to function
   tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
-  temporary_counter=0;
-  reset_temporary_counter();
 
   f.type=to_code_type(symbol.type);
 
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index d0cfa2c9b2f..bec761420ca 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -379,7 +379,7 @@ void goto_convertt::remove_function_call(
 
     new_base_name+='_';
     new_base_name+=id2string(symbol.base_name);
-    new_base_name+="$"+std::to_string(++temporary_counter);
+    new_base_name += "$0";
 
     new_symbol.base_name=new_base_name;
     new_symbol.mode=symbol.mode;
@@ -387,6 +387,7 @@ void goto_convertt::remove_function_call(
 
   new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
 
+  // ensure that the name is unique
   new_name(new_symbol);
 
   {
@@ -429,10 +430,11 @@ void goto_convertt::remove_cpp_new(
 
   auxiliary_symbolt new_symbol;
 
-  new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter);
+  new_symbol.base_name = "new_ptr$0";
   new_symbol.type=expr.type();
   new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
 
+  // ensure that the name is unique
   new_name(new_symbol);
 
   code_declt decl;
@@ -480,11 +482,12 @@ void goto_convertt::remove_malloc(
   {
     auxiliary_symbolt new_symbol;
 
-    new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter);
+    new_symbol.base_name = "malloc_value$0";
     new_symbol.type=expr.type();
     new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
     new_symbol.location=expr.source_location();
 
+    // ensure that the name is unique
     new_name(new_symbol);
 
     code_declt decl;
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 4c35d3b0667..854a706e5e7 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -233,14 +233,13 @@ void remove_function_pointerst::fix_return_type(
        code_type.return_type(), ns))
     return;
 
-  symbolt &tmp_symbol=
-    get_fresh_aux_symbol(
-      code_type.return_type(),
-      "remove_function_pointers",
-      "tmp_return_val",
-      function_call.source_location(),
-      irep_idt(),
-      symbol_table);
+  symbolt &tmp_symbol = get_fresh_aux_symbol(
+    code_type.return_type(),
+    id2string(function_call.source_location().get_function()),
+    "tmp_return_val",
+    function_call.source_location(),
+    irep_idt(),
+    symbol_table);
 
   symbol_exprt tmp_symbol_expr;
   tmp_symbol_expr.type()=tmp_symbol.type;
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index e859c8d9384..ad62322e90a 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -106,14 +106,13 @@ std::size_t remove_instanceoft::lower_instanceof(
   symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
   exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
 
-  symbolt &newsym=
-    get_fresh_aux_symbol(
-      object_clsid.type(),
-      "instanceof_tmp",
-      "instanceof_tmp",
-      source_locationt(),
-      ID_java,
-      symbol_table);
+  symbolt &newsym = get_fresh_aux_symbol(
+    object_clsid.type(),
+    id2string(this_inst->function),
+    "instanceof_tmp",
+    source_locationt(),
+    ID_java,
+    symbol_table);
 
   auto newinst=goto_program.insert_after(this_inst);
   newinst->make_assignment();
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index fb5561ae1c9..53d81c5b78e 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -203,19 +203,21 @@ exprt::operandst java_build_arguments(
     bool allow_null=
       !assume_init_pointers_not_null && !is_main && !is_this;
 
+    object_factory_parameterst parameters = object_factory_parameters;
+    parameters.function_id = function.name;
+
     // generate code to allocate and non-deterministicaly initialize the
     // argument
-    main_arguments[param_number]=
-      object_factory(
-        p.type(),
-        base_name,
-        init_code,
-        allow_null,
-        symbol_table,
-        object_factory_parameters,
-        allocation_typet::LOCAL,
-        function.location,
-        pointer_type_selector);
+    main_arguments[param_number] = object_factory(
+      p.type(),
+      base_name,
+      init_code,
+      allow_null,
+      symbol_table,
+      parameters,
+      allocation_typet::LOCAL,
+      function.location,
+      pointer_type_selector);
 
     // record as an input
     codet input(ID_input);
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 138033676b0..f05e6d13e90 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -35,21 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_root_class.h"
 #include "generic_parameter_specialization_map_keys.h"
 
-static symbolt &new_tmp_symbol(
-  symbol_table_baset &symbol_table,
-  const source_locationt &loc,
-  const typet &type,
-  const std::string &prefix = "tmp_object_factory")
-{
-  return get_fresh_aux_symbol(
-    type,
-    "",
-    prefix,
-    loc,
-    ID_java,
-    symbol_table);
-}
-
 class java_object_factoryt
 {
   /// Every new variable initialized by the code emitted by the methods of this
@@ -195,6 +180,7 @@ exprt allocate_dynamic_object(
   const typet &allocate_type,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &output_code,
   std::vector<const symbolt *> &symbols_created,
   bool cast_needed)
@@ -212,11 +198,13 @@ exprt allocate_dynamic_object(
     // create a symbol for the malloc expression so we can initialize
     // without having to do it potentially through a double-deref, which
     // breaks the to-SSA phase.
-    symbolt &malloc_sym=new_tmp_symbol(
-      symbol_table,
-      loc,
+    symbolt &malloc_sym = get_fresh_aux_symbol(
       pointer_type(allocate_type),
-      "malloc_site");
+      id2string(function_id),
+      "malloc_site",
+      loc,
+      ID_java,
+      symbol_table);
     symbols_created.push_back(&malloc_sym);
     code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
     assign.add_source_location()=loc;
@@ -253,6 +241,7 @@ exprt allocate_dynamic_object_with_decl(
   const exprt &target_expr,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &output_code)
 {
   std::vector<const symbolt *> symbols_created;
@@ -263,6 +252,7 @@ exprt allocate_dynamic_object_with_decl(
     allocate_type,
     symbol_table,
     loc,
+    function_id,
     tmp_block,
     symbols_created,
     false);
@@ -306,7 +296,13 @@ exprt java_object_factoryt::allocate_object(
     case allocation_typet::LOCAL:
     case allocation_typet::GLOBAL:
     {
-      symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type);
+      symbolt &aux_symbol = get_fresh_aux_symbol(
+        allocate_type,
+        id2string(object_factory_parameters.function_id),
+        "tmp_object_factory",
+        loc,
+        ID_java,
+        symbol_table);
       if(alloc_type==allocation_typet::GLOBAL)
         aux_symbol.is_static_lifetime=true;
       symbols_created.push_back(&aux_symbol);
@@ -327,6 +323,7 @@ exprt java_object_factoryt::allocate_object(
         allocate_type,
         symbol_table,
         loc,
+        object_factory_parameters.function_id,
         assignments,
         symbols_created,
         cast_needed);
@@ -569,6 +566,7 @@ codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   bool printable)
 {
@@ -608,8 +606,13 @@ codet initialize_nondet_string_struct(
   {
     /// \todo Refactor with make_nondet_string_expr
     // length_expr = nondet(int);
-    const symbolt length_sym =
-      new_tmp_symbol(symbol_table, loc, java_int_type());
+    const symbolt length_sym = get_fresh_aux_symbol(
+      java_int_type(),
+      id2string(function_id),
+      "tmp_object_factory",
+      loc,
+      ID_java,
+      symbol_table);
     const symbol_exprt length_expr = length_sym.symbol_expr();
     const side_effect_expr_nondett nondet_length(length_expr.type());
     code.add(code_declt(length_expr));
@@ -646,7 +649,7 @@ codet initialize_nondet_string_struct(
     // data_expr = nondet(char[INFINITY]) // we use infinity for variable size
     const dereference_exprt data_expr(data_pointer);
     const exprt nondet_array =
-      make_nondet_infinite_char_array(symbol_table, loc, code);
+      make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
     code.add(code_assignt(data_expr, nondet_array));
 
     struct_expr.copy_to_operands(length_expr);
@@ -692,6 +695,7 @@ static bool add_nondet_string_pointer_initialization(
   bool printable,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   const namespacet ns(symbol_table);
@@ -702,14 +706,15 @@ static bool add_nondet_string_pointer_initialization(
   if(!struct_type.has_component("data") || !struct_type.has_component("length"))
     return true;
 
-  const exprt malloc_site =
-    allocate_dynamic_object_with_decl(expr, symbol_table, loc, code);
+  const exprt malloc_site = allocate_dynamic_object_with_decl(
+    expr, symbol_table, loc, function_id, code);
 
   code.add(
     initialize_nondet_string_struct(
       dereference_exprt(malloc_site, struct_type),
       max_nondet_string_length,
       loc,
+      function_id,
       symbol_table,
       printable));
   return false;
@@ -862,6 +867,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
       object_factory_parameters.string_printable,
       symbol_table,
       loc,
+      object_factory_parameters.function_id,
       assignments);
   }
   else
@@ -967,7 +973,13 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   const pointer_typet &replacement_pointer,
   size_t depth)
 {
-  symbolt new_symbol=new_tmp_symbol(symbol_table, loc, replacement_pointer);
+  symbolt new_symbol = get_fresh_aux_symbol(
+    replacement_pointer,
+    id2string(object_factory_parameters.function_id),
+    "tmp_object_factory",
+    loc,
+    ID_java,
+    symbol_table);
 
   // Generate a new object into this new symbol
   gen_nondet_init(
@@ -1253,11 +1265,13 @@ void java_object_factoryt::allocate_nondet_length_array(
   const exprt &max_length_expr,
   const typet &element_type)
 {
-  symbolt &length_sym=new_tmp_symbol(
-    symbol_table,
-    loc,
+  symbolt &length_sym = get_fresh_aux_symbol(
     java_int_type(),
-    "nondet_array_length");
+    id2string(object_factory_parameters.function_id),
+    "nondet_array_length",
+    loc,
+    ID_java,
+    symbol_table);
   symbols_created.push_back(&length_sym);
   const auto &length_sym_expr=length_sym.symbol_expr();
 
@@ -1347,11 +1361,13 @@ void java_object_factoryt::gen_nondet_array_init(
 
   // Interpose a new symbol, as the goto-symex stage can't handle array indexing
   // via a cast.
-  symbolt &array_init_symbol=new_tmp_symbol(
-    symbol_table,
-    loc,
+  symbolt &array_init_symbol = get_fresh_aux_symbol(
     init_array_expr.type(),
-    "array_data_init");
+    id2string(object_factory_parameters.function_id),
+    "array_data_init",
+    loc,
+    ID_java,
+    symbol_table);
   symbols_created.push_back(&array_init_symbol);
   const auto &array_init_symexpr=array_init_symbol.symbol_expr();
   codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
@@ -1360,11 +1376,13 @@ void java_object_factoryt::gen_nondet_array_init(
 
   // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
   //                  ++array_init_iter) init(array[array_init_iter]);
-  symbolt &counter=new_tmp_symbol(
-    symbol_table,
-    loc,
+  symbolt &counter = get_fresh_aux_symbol(
     length_expr.type(),
-    "array_init_iter");
+    id2string(object_factory_parameters.function_id),
+    "array_init_iter",
+    loc,
+    ID_java,
+    symbol_table);
   symbols_created.push_back(&counter);
   exprt counter_expr=counter.symbol_expr();
 
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index 9a5da141344..a5ba9ea5500 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -142,6 +142,7 @@ exprt allocate_dynamic_object(
   const typet &allocate_type,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &output_code,
   std::vector<const symbolt *> &symbols_created,
   bool cast_needed = false);
@@ -150,12 +151,14 @@ exprt allocate_dynamic_object_with_decl(
   const exprt &target_expr,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &output_code);
 
 codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   bool printable);
 
diff --git a/src/java_bytecode/java_static_initializers.cpp b/src/java_bytecode/java_static_initializers.cpp
index b95dedbfea2..9cb9b054fea 100644
--- a/src/java_bytecode/java_static_initializers.cpp
+++ b/src/java_bytecode/java_static_initializers.cpp
@@ -369,6 +369,9 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
     class_globals.first != class_globals.second,
     "class with synthetic clinit should have at least one global to init");
 
+  object_factory_parameterst parameters = object_factory_parameters;
+  parameters.function_id = function_id;
+
   for(auto it = class_globals.first; it != class_globals.second; ++it)
   {
     const symbol_exprt new_global_symbol =
@@ -381,7 +384,7 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
       false,
       allocation_typet::DYNAMIC,
       !is_non_null_library_global(it->second),
-      object_factory_parameters,
+      parameters,
       pointer_type_selector,
       update_in_placet::NO_UPDATE_IN_PLACE);
   }
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 1f2ce3365d6..a05a285c18b 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -538,6 +538,7 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
 /// \return a new string_expr
 refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -548,7 +549,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   code.add(code_assignt(str.length(), nondet_length), loc);
 
   exprt nondet_array_expr =
-    make_nondet_infinite_char_array(symbol_table, loc, code);
+    make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
 
   address_of_exprt array_pointer(
     index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
@@ -573,11 +574,12 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
 exprt java_string_library_preprocesst::allocate_fresh_string(
   const typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   exprt str=fresh_string(type, loc, symbol_table);
-  allocate_dynamic_object_with_decl(str, symbol_table, loc, code);
+  allocate_dynamic_object_with_decl(str, symbol_table, loc, function_id, code);
   return str;
 }
 
@@ -590,12 +592,14 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
 exprt java_string_library_preprocesst::allocate_fresh_array(
   const typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_tablet &symbol_table,
   code_blockt &code)
 {
   exprt array=fresh_array(type, loc, symbol_table);
   code.add(code_declt(array), loc);
-  allocate_dynamic_object_with_decl(array, symbol_table, loc, code);
+  allocate_dynamic_object_with_decl(
+    array, symbol_table, loc, function_id, code);
   return array;
 }
 
@@ -647,6 +651,7 @@ codet java_string_library_preprocesst::code_return_function_application(
 exprt make_nondet_infinite_char_array(
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   const array_typet array_type(
@@ -799,7 +804,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   code.add(code_declt(return_code), loc);
 
   const refined_string_exprt string_expr =
-    make_nondet_string_expr(loc, symbol_table, code);
+    make_nondet_string_expr(loc, function_name, symbol_table, code);
 
   // args is { str.length, str.content, arguments... }
   exprt::operandst args;
@@ -942,6 +947,7 @@ java_string_library_preprocesst::string_literal_to_string_expr(
 codet java_string_library_preprocesst::make_equals_function_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   const typet &return_type = type.return_type();
@@ -991,6 +997,7 @@ codet java_string_library_preprocesst::make_equals_function_code(
 codet java_string_library_preprocesst::make_float_to_string_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   // Getting the argument
@@ -1002,7 +1009,8 @@ codet java_string_library_preprocesst::make_float_to_string_code(
   code_blockt code;
 
   // Declaring and allocating String * str
-  exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
+  exprt str = allocate_fresh_string(
+    type.return_type(), loc, function_id, symbol_table, code);
 
   // Expression representing 0.0
   ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
@@ -1373,6 +1381,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
   int index,
   const struct_typet &structured_type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -1388,13 +1397,14 @@ exprt java_string_library_preprocesst::make_argument_for_format(
     if(name!="string_expr")
     {
       std::string tmp_name="tmp_"+id2string(name);
-      symbolt field_symbol=get_fresh_aux_symbol(
-        type, tmp_name, tmp_name, loc, ID_java, symbol_table);
+      symbolt field_symbol = get_fresh_aux_symbol(
+        type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
       field_expr=field_symbol.symbol_expr();
       code.add(code_declt(field_expr), loc);
     }
     else
-      field_expr = make_nondet_string_expr(loc, symbol_table, code);
+      field_expr =
+        make_nondet_string_expr(loc, function_id, symbol_table, code);
 
     field_exprs.push_back(field_expr);
     arg_i_struct.copy_to_operands(field_expr);
@@ -1402,10 +1412,16 @@ exprt java_string_library_preprocesst::make_argument_for_format(
 
   // arg_i = argv[index]
   exprt obj=get_object_at_index(argv, index);
-  symbolt object_symbol=get_fresh_aux_symbol(
-    obj.type(), "tmp_format_obj", "tmp_format_obj", loc, ID_java, symbol_table);
+  symbolt object_symbol = get_fresh_aux_symbol(
+    obj.type(),
+    id2string(function_id),
+    "tmp_format_obj",
+    loc,
+    ID_java,
+    symbol_table);
   symbol_exprt arg_i=object_symbol.symbol_expr();
-  allocate_dynamic_object_with_decl(arg_i, symbol_table, loc, code);
+  allocate_dynamic_object_with_decl(
+    arg_i, symbol_table, loc, function_id, code);
   code.add(code_assignt(arg_i, obj), loc);
   code.add(
     code_assumet(
@@ -1468,6 +1484,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
 codet java_string_library_preprocesst::make_string_format_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   PRECONDITION(type.parameters().size()==2);
@@ -1495,13 +1512,14 @@ codet java_string_library_preprocesst::make_string_format_code(
   std::vector<exprt> processed_args;
   processed_args.push_back(args[0]);
   for(std::size_t i=0; i<MAX_FORMAT_ARGS; ++i)
-    processed_args.push_back(make_argument_for_format(
-      args[1], i, structured_type, loc, symbol_table, code));
+    processed_args.push_back(
+      make_argument_for_format(
+        args[1], i, structured_type, loc, function_id, symbol_table, code));
 
   refined_string_exprt string_expr = string_expr_of_function(
     ID_cprover_string_format_func, processed_args, loc, symbol_table, code);
-  exprt java_string=allocate_fresh_string(
-    type.return_type(), loc, symbol_table, code);
+  exprt java_string = allocate_fresh_string(
+    type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
       java_string, string_expr, symbol_table),
@@ -1525,6 +1543,7 @@ codet java_string_library_preprocesst::make_string_format_code(
 codet java_string_library_preprocesst::make_object_get_class_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   code_typet::parameterst params=type.parameters();
@@ -1568,7 +1587,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
   // string1 = (String*) string_expr
   pointer_typet string_ptr_type=java_reference_type(
     symbol_table.lookup_ref("java::java.lang.String").type);
-  exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code);
+  exprt string1 = allocate_fresh_string(
+    string_ptr_type, loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(string1, string_expr1, symbol_table),
     loc);
@@ -1647,7 +1667,8 @@ codet java_string_library_preprocesst::make_string_returning_function_from_call(
     string_expr_of_function(function_name, arguments, loc, symbol_table, code);
 
   // Assign to string
-  exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
+  exprt str = allocate_fresh_string(
+    type.return_type(), loc, function_name, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
     loc);
@@ -1673,6 +1694,7 @@ codet java_string_library_preprocesst::make_string_returning_function_from_call(
 codet java_string_library_preprocesst::make_copy_string_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   // Code for the output
@@ -1688,7 +1710,8 @@ codet java_string_library_preprocesst::make_copy_string_code(
     string_expr, arg0, loc, symbol_table, code);
 
   // Allocate and assign the string
-  exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
+  exprt str = allocate_fresh_string(
+    type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
     loc);
@@ -1712,6 +1735,7 @@ codet java_string_library_preprocesst::make_copy_string_code(
 codet java_string_library_preprocesst::make_copy_constructor_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   // Code for the output
@@ -1746,6 +1770,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
 codet java_string_library_preprocesst::make_init_from_array_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   // Code for the output
@@ -1793,6 +1818,7 @@ codet java_string_library_preprocesst::make_init_from_array_code(
 codet java_string_library_preprocesst::make_string_length_code(
   const code_typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   code_typet::parameterst params=type.parameters();
@@ -1876,7 +1902,7 @@ exprt java_string_library_preprocesst::code_for_function(
 
   auto it=conversion_table.find(function_id);
   if(it!=conversion_table.end())
-    return it->second(type, loc, symbol_table);
+    return it->second(type, loc, function_id, symbol_table);
 
   return nil_exprt();
 }
@@ -1911,28 +1937,29 @@ void java_string_library_preprocesst::initialize_conversion_table()
   // provided for them in the class-path.
 
   // String library
+  conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
+    std::bind(
+      &java_string_library_preprocesst::make_copy_constructor_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   conversion_table
-    ["java::java.lang.String.<init>:(Ljava/lang/String;)V"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_constructor_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
-  conversion_table
-    ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_constructor_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
+      &java_string_library_preprocesst::make_copy_constructor_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
     &java_string_library_preprocesst::make_init_from_array_code,
     this,
     std::placeholders::_1,
     std::placeholders::_2,
-    std::placeholders::_3);
+    std::placeholders::_3,
+    std::placeholders::_4);
   cprover_equivalent_to_java_constructor
     ["java::java.lang.String.<init>:()V"]=
       ID_cprover_string_empty_string_func;
@@ -1970,25 +1997,27 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
       ID_cprover_string_endswith_func;
 
-  conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]=
+  conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"] =
     std::bind(
       &java_string_library_preprocesst::make_equals_function_code,
       this,
       std::placeholders::_1,
       std::placeholders::_2,
-      std::placeholders::_3);
+      std::placeholders::_3,
+      std::placeholders::_4);
   cprover_equivalent_to_java_function
     ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
       ID_cprover_string_equals_ignore_case_func;
   conversion_table
     ["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)"
-      "Ljava/lang/String;"]=
+     "Ljava/lang/String;"] =
       std::bind(
         &java_string_library_preprocesst::make_string_format_code,
         this,
         std::placeholders::_1,
         std::placeholders::_2,
-        std::placeholders::_3);
+        std::placeholders::_3,
+        std::placeholders::_4);
   cprover_equivalent_to_java_function
     ["java::java.lang.String.hashCode:()I"]=
       ID_cprover_string_hash_code_func;
@@ -2022,14 +2051,13 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_function
     ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
       ID_cprover_string_last_index_of_func;
-  conversion_table
-    ["java::java.lang.String.length:()I"]=
-      std::bind(
-        &java_string_library_preprocesst::make_string_length_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+  conversion_table["java::java.lang.String.length:()I"] = std::bind(
+    &java_string_library_preprocesst::make_string_length_code,
+    this,
+    std::placeholders::_1,
+    std::placeholders::_2,
+    std::placeholders::_3,
+    std::placeholders::_4);
   cprover_equivalent_to_java_function
     ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
      "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
@@ -2061,14 +2089,14 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
       ID_cprover_string_to_lower_case_func;
-  conversion_table
-    ["java::java.lang.String.toString:()Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+  conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] =
+    std::bind(
+      &java_string_library_preprocesst::make_copy_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
       ID_cprover_string_to_upper_case_func;
@@ -2081,22 +2109,22 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
       ID_cprover_string_of_char_func;
-  conversion_table
-    ["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_float_to_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
-  conversion_table
-    ["java::java.lang.String.valueOf:(F)Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_float_to_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+  conversion_table["java::java.lang.String.valueOf:(D)Ljava/lang/String;"] =
+    std::bind(
+      &java_string_library_preprocesst::make_float_to_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
+  conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] =
+    std::bind(
+      &java_string_library_preprocesst::make_float_to_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
       ID_cprover_string_of_int_func;
@@ -2106,13 +2134,13 @@ void java_string_library_preprocesst::initialize_conversion_table()
 
   // StringBuilder library
   conversion_table
-    ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_constructor_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
+      &java_string_library_preprocesst::make_copy_constructor_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   cprover_equivalent_to_java_constructor
     ["java::java.lang.StringBuilder.<init>:()V"]=
       ID_cprover_string_empty_string_func;
@@ -2182,14 +2210,13 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
      "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
-  conversion_table
-    ["java::java.lang.StringBuilder.length:()I"]=
-      std::bind(
-        &java_string_library_preprocesst::make_string_length_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+  conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
+    &java_string_library_preprocesst::make_string_length_code,
+    this,
+    std::placeholders::_1,
+    std::placeholders::_2,
+    std::placeholders::_3,
+    std::placeholders::_4);
   cprover_equivalent_to_java_assign_function
     ["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
       ID_cprover_string_char_set_func;
@@ -2203,23 +2230,23 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   conversion_table
-    ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
+      &java_string_library_preprocesst::make_copy_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
 
   // StringBuffer library
   conversion_table
-    ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_constructor_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
+      &java_string_library_preprocesst::make_copy_constructor_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   cprover_equivalent_to_java_constructor
     ["java::java.lang.StringBuffer.<init>:()V"]=
       ID_cprover_string_empty_string_func;
@@ -2303,39 +2330,39 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::org.cprover.CProverString.substring:(Ljava/Lang/"
      "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
   conversion_table
-    ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
+      &java_string_library_preprocesst::make_copy_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
 
   // CharSequence library
   cprover_equivalent_to_java_function
     ["java::java.lang.CharSequence.charAt:(I)C"]=
       ID_cprover_string_char_at_func;
   conversion_table
-    ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_copy_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
+      &java_string_library_preprocesst::make_copy_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   conversion_table
     ["java::java.lang.CharSequence.length:()I"]=
       conversion_table["java::java.lang.String.length:()I"];
 
   // Other libraries
-  conversion_table
-    ["java::java.lang.Float.toString:(F)Ljava/lang/String;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_float_to_string_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+  conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] =
+    std::bind(
+      &java_string_library_preprocesst::make_float_to_string_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
   cprover_equivalent_to_java_function
     ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
       ID_cprover_string_parse_int_func;
@@ -2363,12 +2390,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
       ID_cprover_string_of_int_func;
-  conversion_table
-    ["java::java.lang.Object.getClass:()Ljava/lang/Class;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_object_get_class_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+  conversion_table["java::java.lang.Object.getClass:()Ljava/lang/Class;"] =
+    std::bind(
+      &java_string_library_preprocesst::make_object_get_class_code,
+      this,
+      std::placeholders::_1,
+      std::placeholders::_2,
+      std::placeholders::_3,
+      std::placeholders::_4);
 }
diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h
index c3bedd13734..d481047dc20 100644
--- a/src/java_bytecode/java_string_library_preprocess.h
+++ b/src/java_bytecode/java_string_library_preprocess.h
@@ -100,8 +100,11 @@ class java_string_library_preprocesst:public messaget
   const typet index_type;
   const refined_string_typet refined_string_type;
 
-  typedef std::function<
-    codet(const code_typet &, const source_locationt &, symbol_table_baset &)>
+  typedef std::function<codet(
+    const code_typet &,
+    const source_locationt &,
+    const irep_idt &,
+    symbol_table_baset &)>
     conversion_functiont;
 
   typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> id_mapt;
@@ -148,41 +151,49 @@ class java_string_library_preprocesst:public messaget
   codet make_equals_function_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_float_to_string_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_string_to_char_array_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table);
 
   codet make_string_format_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_copy_string_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_copy_constructor_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_string_length_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_object_get_class_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   // Helper functions
@@ -241,18 +252,21 @@ class java_string_library_preprocesst:public messaget
 
   refined_string_exprt make_nondet_string_expr(
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
   exprt allocate_fresh_string(
     const typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
   exprt allocate_fresh_array(
     const typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table,
     code_blockt &code);
 
@@ -329,6 +343,7 @@ class java_string_library_preprocesst:public messaget
     int index,
     const struct_typet &structured_type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
@@ -344,12 +359,14 @@ class java_string_library_preprocesst:public messaget
   codet make_init_from_array_code(
     const code_typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 };
 
 exprt make_nondet_infinite_char_array(
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 void add_pointer_to_array_association(
diff --git a/src/java_bytecode/object_factory_parameters.h b/src/java_bytecode/object_factory_parameters.h
index dfc498c9661..5e0785bf7a7 100644
--- a/src/java_bytecode/object_factory_parameters.h
+++ b/src/java_bytecode/object_factory_parameters.h
@@ -34,6 +34,9 @@ struct object_factory_parameterst final
 
   /// Force string content to be ASCII printable characters when set to true.
   bool string_printable = false;
+
+  /// Function id, used as a prefix for identifiers of temporaries
+  irep_idt function_id;
 };
 
 #endif
diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp
index 34cef89a30f..0f7c3a9daf2 100644
--- a/src/util/fresh_symbol.cpp
+++ b/src/util/fresh_symbol.cpp
@@ -11,16 +11,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include "fresh_symbol.h"
 
-// This needs to be outside get_fresh_aux_symbol
-// to make it available for both reset_temporary_counter
-// and get_fresh_aux_symbol
-static size_t temporary_counter=0;
-
-// This is useful with loading multiple GOTO models
-void reset_temporary_counter()
-{
-  temporary_counter=0;
-}
+#include "namespace.h"
+#include "rename.h"
 
 /// Installs a fresh-named symbol with the requested name pattern
 /// \par parameters: `type`: type of new symbol
@@ -38,19 +30,23 @@ symbolt &get_fresh_aux_symbol(
   const irep_idt &symbol_mode,
   symbol_table_baset &symbol_table)
 {
-  // Loop until find a name that doesn't clash with a non-auxilliary symbol
-  while(true)
+  namespacet ns(symbol_table);
+  irep_idt identifier = basename_prefix;
+  std::size_t prefix_size = 0;
+  if(!name_prefix.empty())
   {
-    auxiliary_symbolt new_symbol(
-      // Distinguish local variables with the same name
-      basename_prefix + "$" + std::to_string(++temporary_counter),
-      type);
-    if(!name_prefix.empty())
-      new_symbol.name=name_prefix+"::"+id2string(new_symbol.base_name);
-    new_symbol.location=source_location;
-    new_symbol.mode=symbol_mode;
-    std::pair<symbolt &, bool> res=symbol_table.insert(std::move(new_symbol));
-    if(res.second)
-      return res.first;
+    identifier = name_prefix + "::" + basename_prefix;
+    prefix_size = name_prefix.size() + 2;
   }
+  get_new_name(identifier, ns, '$');
+  std::string basename = id2string(identifier).substr(prefix_size);
+
+  auxiliary_symbolt new_symbol(basename, type);
+  new_symbol.name = identifier;
+  new_symbol.location = source_location;
+  new_symbol.mode = symbol_mode;
+  std::pair<symbolt &, bool> res = symbol_table.insert(std::move(new_symbol));
+  CHECK_RETURN(res.second);
+
+  return res.first;
 }
diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h
index 18d91164248..8cdedc56977 100644
--- a/src/util/fresh_symbol.h
+++ b/src/util/fresh_symbol.h
@@ -19,8 +19,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include <util/symbol_table.h>
 #include <util/type.h>
 
-void reset_temporary_counter();
-
 symbolt &get_fresh_aux_symbol(
   const typet &type,
   const std::string &name_prefix,
diff --git a/src/util/rename.cpp b/src/util/rename.cpp
index b0fdf8d3219..17645508ebf 100644
--- a/src/util/rename.cpp
+++ b/src/util/rename.cpp
@@ -24,13 +24,13 @@ void get_new_name(symbolt &symbol, const namespacet &ns)
 /// automated variable renaming
 /// \par parameters: symbol to be renamed, namespace
 /// \return new symbol
-void get_new_name(irep_idt &new_name, const namespacet &ns)
+void get_new_name(irep_idt &new_name, const namespacet &ns, char delimiter)
 {
   const symbolt *symbol;
   if(ns.lookup(new_name, symbol))
-    return;
+    return; // name not taken yet
 
-  std::string prefix=id2string(new_name)+"_";
+  std::string prefix = id2string(new_name) + delimiter;
 
   new_name=prefix+std::to_string(ns.get_max(prefix)+1);
 }
diff --git a/src/util/rename.h b/src/util/rename.h
index 8e9269e02be..3456bfc3827 100644
--- a/src/util/rename.h
+++ b/src/util/rename.h
@@ -23,7 +23,9 @@ class symbolt;
 void get_new_name(symbolt &symbol,
                   const namespacet &ns);
 
-void get_new_name(irep_idt &new_name,
-                  const namespacet &ns);
+void get_new_name(
+  irep_idt &new_name,
+  const namespacet &ns,
+  char delimiter = '_');
 
 #endif // CPROVER_UTIL_RENAME_H
diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
index f038a4e7642..efba76b4fe0 100644
--- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
+++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
@@ -48,8 +48,8 @@ SCENARIO(
 
     WHEN("Initialisation code for a string is generated")
     {
-      const codet code =
-        initialize_nondet_string_struct(expr, 20, loc, symbol_table, false);
+      const codet code = initialize_nondet_string_struct(
+        expr, 20, loc, "test", symbol_table, false);
 
       THEN("Code is produced")
       {
diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
index c24a94b1f50..e9eca838d9c 100644
--- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
+++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -32,8 +32,6 @@ TEST_CASE("Convert exprt to string exprt")
 {
   GIVEN("A location, a string expression, and a symbol table")
   {
-    reset_temporary_counter();
-
     source_locationt loc;
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);