diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp
index 427122e1992..a5d4b8fa19f 100644
--- a/jbmc/src/java_bytecode/convert_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp
@@ -15,12 +15,12 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include <util/fresh_symbol.h>
 #include <util/irep_ids.h>
 
 #include <memory>
 
 #include "java_object_factory.h" // gen_nondet_init
+#include "java_utils.h"
 
 /// Returns true if `expr` is a nondet pointer that isn't a function pointer or
 /// a void* pointer as these can be meaningfully non-det initialized.
@@ -116,13 +116,8 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
     //   target2: instruction containing op, with op replaced by aux_symbol
     //            dead aux_symbol
 
-    symbolt &aux_symbol = get_fresh_aux_symbol(
-      op.type(),
-      id2string(function_identifier),
-      "nondet_tmp",
-      source_loc,
-      ID_java,
-      symbol_table);
+    symbolt &aux_symbol = fresh_java_symbol(
+      op.type(), "nondet_tmp", source_loc, function_identifier, symbol_table);
 
     const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
     op = aux_symbol_expr;
diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index eb1a43696f8..76417570344 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -9,12 +9,12 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
 #include "java_bytecode_concurrency_instrumentation.h"
 #include "expr2java.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 #include <util/expr_iterator.h>
 #include <util/namespace.h>
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
-#include <util/fresh_symbol.h>
 #include <util/arith_tools.h>
 
 // Disable linter to allow an std::string constant.
@@ -229,12 +229,11 @@ static void instrument_synchronized_code(
   code_pop_catcht catch_pop;
 
   // Create the finally block with the same label targeted in the catch-push
-  const symbolt &tmp_symbol = get_fresh_aux_symbol(
+  const symbolt &tmp_symbol = fresh_java_symbol(
     java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
-    id2string(symbol.name),
     "caught-synchronized-exception",
     code.source_location(),
-    ID_java,
+    id2string(symbol.name),
     symbol_table);
   symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
   catch_var.set(ID_C_base_name, tmp_symbol.base_name);
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
index 3b11e293fdf..4ae7ae42741 100644
--- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -11,7 +11,6 @@ Date:   June 2017
 #include "java_bytecode_instrument.h"
 
 #include <util/arith_tools.h>
-#include <util/fresh_symbol.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/c_types.h>
@@ -112,14 +111,8 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception(
 
   // Allocate and throw an instance of the exception class:
 
-  symbolt &new_symbol=
-    get_fresh_aux_symbol(
-      exc_ptr_type,
-      "new_exception",
-      "new_exception",
-      original_loc,
-      ID_java,
-      symbol_table);
+  symbolt &new_symbol = fresh_java_symbol(
+    exc_ptr_type, "new_exception", original_loc, "new_exception", symbol_table);
 
   side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
   code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 39a834cc3da..30284035635 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -375,12 +375,11 @@ exprt::operandst java_build_arguments(
       // method(..., param, ...)
       //
 
-      const symbolt result_symbol = get_fresh_aux_symbol(
+      const symbolt result_symbol = fresh_java_symbol(
         p.type(),
-        id2string(function.name),
         "nondet_parameter_" + std::to_string(param_number),
         function.location,
-        ID_java,
+        function.name,
         symbol_table);
       main_arguments[param_number] = result_symbol.symbol_expr();
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 9f9a52efec7..a8d7e204ec5 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_object_factory.h"
 
 #include <util/expr_initializer.h>
-#include <util/fresh_symbol.h>
 #include <util/nondet_bool.h>
 #include <util/nondet.h>
 #include <util/pointer_offset_size.h>
@@ -20,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
 #include "java_string_literals.h"
+#include "java_utils.h"
 
 class java_object_factoryt
 {
@@ -442,13 +442,8 @@ void initialize_nondet_string_fields(
 
   /// \todo Refactor with make_nondet_string_expr
   // length_expr = nondet(int);
-  const symbolt length_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    id2string(function_id),
-    "tmp_object_factory",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt length_sym = fresh_java_symbol(
+    java_int_type(), "tmp_object_factory", loc, function_id, symbol_table);
   const symbol_exprt length_expr = length_sym.symbol_expr();
   const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
   code.add(code_declt(length_expr));
@@ -476,10 +471,10 @@ void initialize_nondet_string_fields(
     index_exprt(data_expr, from_integer(0, java_int_type())));
 
   add_pointer_to_array_association(
-    array_pointer, data_expr, symbol_table, loc, code);
+    array_pointer, data_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
-    data_expr, length_expr, symbol_table, loc, code);
+    data_expr, length_expr, symbol_table, loc, function_id, code);
 
   struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
 
@@ -487,7 +482,7 @@ void initialize_nondet_string_fields(
   if(printable)
   {
     add_character_set_constraint(
-      array_pointer, length_expr, " -~", symbol_table, loc, code);
+      array_pointer, length_expr, " -~", symbol_table, loc, function_id, code);
   }
 }
 
@@ -745,12 +740,11 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   size_t depth,
   const source_locationt &location)
 {
-  symbolt new_symbol = get_fresh_aux_symbol(
+  symbolt new_symbol = fresh_java_symbol(
     replacement_pointer,
-    id2string(object_factory_parameters.function_id),
     "tmp_object_factory",
-    loc,
-    ID_java,
+    location,
+    object_factory_parameters.function_id,
     symbol_table);
 
   // Generate a new object into this new symbol
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 9cd208b9860..edf38dd76b0 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -241,30 +241,10 @@ void java_string_library_preprocesst::add_string_type(
   string_symbol->mode = ID_java;
 }
 
-/// add a symbol in the table with static lifetime and name containing
-/// `cprover_string_array` and given type
-/// \param type: an array type
-/// \param location: a location in the program
-/// \param symbol_table: symbol table
-symbol_exprt java_string_library_preprocesst::fresh_array(
-  const typet &type,
-  const source_locationt &location,
-  symbol_tablet &symbol_table)
-{
-  symbolt array_symbol=get_fresh_aux_symbol(
-    type,
-    "cprover_string_array",
-    "cprover_string_array",
-    location,
-    ID_java,
-    symbol_table);
-  array_symbol.is_static_lifetime=true;
-  return array_symbol.symbol_expr();
-}
-
 /// calls string_refine_preprocesst::process_operands with a list of parameters.
 /// \param params: a list of function parameters
 /// \param loc: location in the source
+/// \param function_id: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
@@ -272,16 +252,14 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
 exprt::operandst java_string_library_preprocesst::process_parameters(
   const java_method_typet::parameterst &params,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   exprt::operandst ops;
   for(const auto &p : params)
-  {
-    symbol_exprt sym(p.get_identifier(), p.type());
-    ops.push_back(sym);
-  }
-  return process_operands(ops, loc, symbol_table, init_code);
+    ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
+  return process_operands(ops, loc, function_id, symbol_table, init_code);
 }
 
 /// Creates a string_exprt from the input exprt representing a char sequence
@@ -289,6 +267,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
 ///   sequence
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
+/// \param function_id: name of the function in which the code will be added
 /// \param init_code: code block, in which declaration will be added:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// char *cprover_string_content;
@@ -303,11 +282,12 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
   const exprt &expr_to_process,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
+  const irep_idt &function_id,
   code_blockt &init_code)
 {
   PRECONDITION(implements_java_char_sequence_pointer(expr_to_process.type()));
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, init_code);
+    decl_string_expr(loc, function_id, symbol_table, init_code);
   code_assign_java_string_to_string_expr(
     string_expr, expr_to_process, loc, symbol_table, init_code);
   return string_expr;
@@ -320,6 +300,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 /// for char array references.
 /// \param operands: a list of expressions
 /// \param loc: location in the source
+/// \param function_id: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
@@ -327,6 +308,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 exprt::operandst java_string_library_preprocesst::process_operands(
   const exprt::operandst &operands,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
@@ -334,50 +316,17 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   for(const auto &p : operands)
   {
     if(implements_java_char_sequence_pointer(p.type()))
-      ops.push_back(
-        convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
+      ops.push_back(convert_exprt_to_string_exprt(
+        p, loc, symbol_table, function_id, init_code));
     else if(is_java_char_array_pointer_type(p.type()))
-      ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
+      ops.push_back(
+        replace_char_array(p, loc, function_id, symbol_table, init_code));
     else
       ops.push_back(p);
   }
   return ops;
 }
 
-/// Converts the operands of the equals function to string expressions and
-/// outputs these conversions. As a side effect of the conversions it adds some
-/// code to init_code.
-/// \param operands: a list of expressions
-/// \param loc: location in the source
-/// \param symbol_table: symbol table
-/// \param init_code: code block, in which declaration of some arguments may be
-///   added
-/// \return a list of expressions
-exprt::operandst
-java_string_library_preprocesst::process_equals_function_operands(
-  const exprt::operandst &operands,
-  const source_locationt &loc,
-  symbol_table_baset &symbol_table,
-  code_blockt &init_code)
-{
-  PRECONDITION(operands.size()==2);
-  exprt::operandst ops;
-  const exprt &op0=operands[0];
-  const exprt &op1 = operands[1];
-  PRECONDITION(implements_java_char_sequence_pointer(op0.type()));
-
-  ops.push_back(
-    convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
-
-  // TODO: Manage the case where we have a non-String Object (this should
-  // probably be handled upstream. At any rate, the following code should be
-  // protected with assertions on the type of op1.
-  typecast_exprt tcast(op1, to_pointer_type(op0.type()));
-  ops.push_back(
-    convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
-  return ops;
-}
-
 /// Finds the type of the data component
 /// \param type: a type containing a "data" component
 /// \param symbol_table: symbol table
@@ -441,35 +390,37 @@ static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
 /// array.
 /// \param array_pointer: an expression of type char array pointer
 /// \param loc: location in the source
+/// \param function_id: name of the function in which the string is defined
 /// \param symbol_table: symbol table
 /// \param code: code block, in which some assignments will be added
 /// \return a string expression
 refined_string_exprt java_string_library_preprocesst::replace_char_array(
   const exprt &array_pointer,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   // array is *array_pointer
-  dereference_exprt array=
+  const dereference_exprt array =
     checked_dereference(array_pointer, array_pointer.type().subtype());
   // array_data is array_pointer-> data
   const exprt array_data = get_data(array, symbol_table);
-  symbolt sym_char_array = get_fresh_aux_symbol(
-    array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
-  symbol_exprt char_array=sym_char_array.symbol_expr();
+  const symbolt &sym_char_array = fresh_java_symbol(
+    array_data.type(), "char_array", loc, function_id, symbol_table);
+  const symbol_exprt char_array = sym_char_array.symbol_expr();
   // char_array = array_pointer->data
   code.add(code_assignt(char_array, array_data), loc);
 
   // string_expr is `{ rhs->length; string_array }`
-  refined_string_exprt string_expr(
+  const refined_string_exprt string_expr(
     get_length(array, symbol_table), char_array, refined_string_type);
 
-  dereference_exprt inf_array(
+  const dereference_exprt inf_array(
     char_array, array_typet(java_char_type(), infinity_exprt(java_int_type())));
 
   add_pointer_to_array_association(
-    string_expr.content(), inf_array, symbol_table, loc, code);
+    string_expr.content(), inf_array, symbol_table, loc, function_id, code);
 
   return string_expr;
 }
@@ -478,15 +429,17 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
 /// given type
 /// \param type: a type for refined strings
 /// \param loc: a location in the program
+/// \param function_id: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \return a new symbol
 symbol_exprt java_string_library_preprocesst::fresh_string(
   const typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
-  symbolt string_symbol=get_fresh_aux_symbol(
-    type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
+  symbolt string_symbol =
+    fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
   string_symbol.is_static_lifetime=true;
   return string_symbol.symbol_expr();
 }
@@ -494,33 +447,26 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
 /// Add declaration of a refined string expr whose content and length are
 /// fresh symbols.
 /// \param loc: source location
+/// \param function_id: name of the function in which the string is defined
 /// \param symbol_table: the symbol table
 /// \param [out] code: code block to which the declaration is added
 /// \return refined string expr with fresh content and length symbols
 refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  symbolt sym_length = get_fresh_aux_symbol(
-    index_type,
-    "cprover_string_length",
-    "cprover_string_length",
-    loc,
-    ID_java,
-    symbol_table);
-  symbol_exprt length_field=sym_length.symbol_expr();
-  pointer_typet array_type = pointer_type(java_char_type());
-  symbolt sym_content = get_fresh_aux_symbol(
-    array_type,
-    "cprover_string_content",
-    "cprover_string_content",
-    loc,
-    ID_java,
-    symbol_table);
-  symbol_exprt content_field = sym_content.symbol_expr();
+  const symbolt &sym_length = fresh_java_symbol(
+    index_type, "cprover_string_length", loc, function_id, symbol_table);
+  const symbol_exprt length_field = sym_length.symbol_expr();
+  const pointer_typet array_type = pointer_type(java_char_type());
+  const symbolt &sym_content = fresh_java_symbol(
+    array_type, "cprover_string_content", loc, function_id, symbol_table);
+  const symbol_exprt content_field = sym_content.symbol_expr();
   code.add(code_declt(content_field), loc);
-  refined_string_exprt str(length_field, content_field, refined_string_type);
+  const refined_string_exprt str{
+    length_field, content_field, refined_string_type};
   code.add(code_declt(length_field), loc);
   return str;
 }
@@ -539,22 +485,23 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   code_blockt &code)
 {
   /// \todo refactor with initialize_nonddet_string_struct
-  const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt str =
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
 
-  exprt nondet_array_expr =
+  const exprt nondet_array_expr =
     make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
 
-  address_of_exprt array_pointer(
+  const address_of_exprt array_pointer(
     index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
 
   add_pointer_to_array_association(
-    array_pointer, nondet_array_expr, symbol_table, loc, code);
+    array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
-    nondet_array_expr, str.length(), symbol_table, loc, code);
+    nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
 
   code.add(code_assignt(str.content(), array_pointer), loc);
 
@@ -575,7 +522,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  exprt str=fresh_string(type, loc, symbol_table);
+  const exprt str = fresh_string(type, loc, function_id, symbol_table);
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
@@ -589,42 +536,42 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
 
 /// assign the result of a function call
 /// \param lhs: an expression
-/// \param function_name: the name of the function
+/// \param function_id: the name of the function
 /// \param arguments: a list of arguments
 /// \param symbol_table: a symbol table
 /// \return the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// lhs = <function_name>(arguments)
+/// lhs = <function_id>(arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 static codet code_assign_function_application(
   const exprt &lhs,
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const exprt::operandst &arguments,
   symbol_table_baset &symbol_table)
 {
-  exprt fun_app=make_function_application(
-    function_name, arguments, lhs.type(), symbol_table);
-  return code_assignt(lhs, fun_app);
+  return code_assignt(
+    lhs,
+    make_function_application(
+      function_id, arguments, lhs.type(), symbol_table));
 }
 
 /// return the result of a function call
-/// \param function_name: the name of the function
+/// \param function_id: the name of the function
 /// \param arguments: a list of arguments
 /// \param type: the return type
 /// \param symbol_table: a symbol table
 /// \return the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// return <function_name>(arguments)
+/// return <function_id>(arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::code_return_function_application(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const exprt::operandst &arguments,
   const typet &type,
   symbol_table_baset &symbol_table)
 {
-  exprt fun_app=make_function_application(
-    function_name, arguments, type, symbol_table);
-  return code_returnt(fun_app);
+  return code_returnt(
+    make_function_application(function_id, arguments, type, symbol_table));
 }
 
 /// Declare a fresh symbol of type array of character with infinite size.
@@ -641,12 +588,11 @@ exprt make_nondet_infinite_char_array(
 {
   const array_typet array_type(
     java_char_type(), infinity_exprt(java_int_type()));
-  const symbolt data_sym = get_fresh_aux_symbol(
+  const symbolt data_sym = fresh_java_symbol(
     pointer_type(array_type),
-    id2string(function_id),
     "nondet_infinite_array_pointer",
     loc,
-    ID_java,
+    function_id,
     symbol_table);
 
   const symbol_exprt data_pointer = data_sym.symbol_expr();
@@ -664,24 +610,21 @@ exprt make_nondet_infinite_char_array(
 /// \param array: a character array expression
 /// \param symbol_table: the symbol table
 /// \param loc: source location
+/// \param function_id: name of the function in which the code will be added
 /// \param [out] code: code block to which declaration and calls get added
 void add_pointer_to_array_association(
   const exprt &pointer,
   const exprt &array,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   PRECONDITION(array.type().id() == ID_array);
   PRECONDITION(pointer.type().id() == ID_pointer);
-  symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    "return_array",
-    "return_array",
-    loc,
-    ID_java,
-    symbol_table);
-  auto return_expr = return_sym.symbol_expr();
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "return_array", loc, function_id, symbol_table);
+  const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
     code_assign_function_application(
@@ -698,21 +641,18 @@ void add_pointer_to_array_association(
 /// \param length: integer expression
 /// \param symbol_table: the symbol table
 /// \param loc: source location
+/// \param function_id: name of the function in which the code will be added
 /// \param [out] code: code block to which declaration and calls get added
 void add_array_to_length_association(
   const exprt &array,
   const exprt &length,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
-  symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    "return_array",
-    "return_array",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "return_array", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -733,6 +673,7 @@ void add_array_to_length_association(
 ///   lower case ascii letters.
 /// \param symbol_table: the symbol table
 /// \param loc: source location
+/// \param function_id: the name of the function
 /// \param [out] code: code block to which declaration and calls get added
 void add_character_set_constraint(
   const exprt &pointer,
@@ -740,11 +681,12 @@ void add_character_set_constraint(
   const irep_idt &char_set,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   PRECONDITION(pointer.type().id() == ID_pointer);
-  symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "cnstr_added", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   const constant_exprt char_set_expr(char_set, string_typet());
@@ -758,10 +700,10 @@ void add_character_set_constraint(
 }
 
 /// Create a refined_string_exprt `str` whose content and length are fresh
-/// symbols, calls the string primitive with name `function_name`.
+/// symbols, calls the string primitive with name `function_id`.
 /// In the arguments of the primitive `str` takes the place of the result and
 /// the following arguments are given by parameter `arguments.
-/// \param function_name: the name of the function
+/// \param function_id: the name of the function
 /// \param arguments: arguments of the function
 /// \param loc: source location
 /// \param symbol_table: symbol table
@@ -770,29 +712,28 @@ void add_character_set_constraint(
 /// int return_code;
 /// int str.length;
 /// char str.data[str.length]
-/// return_code = <function_name>(str.length, str.data, arguments)
+/// return_code = <function_id>(str.length, str.data, arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// \return refined string expression `str`
 refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const exprt::operandst &arguments,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   // int return_code;
-  symbolt return_code_sym = get_fresh_aux_symbol(
+  const symbolt return_code_sym = fresh_java_symbol(
     java_int_type(),
-    std::string("return_code_") + function_name.c_str(),
-    std::string("return_code_") + function_name.c_str(),
+    std::string("return_code_") + function_id.c_str(),
     loc,
-    ID_java,
+    function_id,
     symbol_table);
   const auto return_code = return_code_sym.symbol_expr();
   code.add(code_declt(return_code), loc);
 
   const refined_string_exprt string_expr =
-    make_nondet_string_expr(loc, function_name, symbol_table, code);
+    make_nondet_string_expr(loc, function_id, symbol_table, code);
 
   // args is { str.length, str.content, arguments... }
   exprt::operandst args;
@@ -800,10 +741,10 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   args.push_back(string_expr.content());
   args.insert(args.end(), arguments.begin(), arguments.end());
 
-  // return_code = <function_name>_data(args)
+  // return_code = <function_id>_data(args)
   code.add(
     code_assign_function_application(
-      return_code, function_name, args, symbol_table),
+      return_code, function_id, args, symbol_table),
     loc);
 
   return string_expr;
@@ -961,14 +902,14 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   code_blockt code;
 
   // Declaring and allocating String * str
-  exprt str = allocate_fresh_string(
+  const 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()));
+  const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
   ieee_floatt zero_float(float_spec);
   zero_float.from_float(0.0);
-  constant_exprt zero=zero_float.to_expr();
+  const constant_exprt zero = zero_float.to_expr();
 
   // For each possible case with have a condition and a string_exprt
   std::vector<exprt> condition_list;
@@ -976,7 +917,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Case of computerized scientific notation
   condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
-  refined_string_exprt sci_notation = string_expr_of_function(
+  const refined_string_exprt sci_notation = string_expr_of_function(
     ID_cprover_string_of_float_scientific_notation_func,
     {arg},
     loc,
@@ -986,9 +927,9 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Subcase of negative scientific notation
   condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
-  refined_string_exprt minus_sign =
+  const refined_string_exprt minus_sign =
     string_literal_to_string_expr("-", loc, symbol_table, code);
-  refined_string_exprt neg_sci_notation = string_expr_of_function(
+  const refined_string_exprt neg_sci_notation = string_expr_of_function(
     ID_cprover_string_concat_func,
     {minus_sign, sci_notation},
     loc,
@@ -998,20 +939,20 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Case of NaN
   condition_list.push_back(isnan_exprt(arg));
-  refined_string_exprt nan =
+  const refined_string_exprt nan =
     string_literal_to_string_expr("NaN", loc, symbol_table, code);
   string_expr_list.push_back(nan);
 
   // Case of Infinity
   extractbit_exprt is_neg(arg, float_spec.width()-1);
   condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
-  refined_string_exprt infinity =
+  const refined_string_exprt infinity =
     string_literal_to_string_expr("Infinity", loc, symbol_table, code);
   string_expr_list.push_back(infinity);
 
   // Case -Infinity
   condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
-  refined_string_exprt minus_infinity =
+  const refined_string_exprt minus_infinity =
     string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
   string_expr_list.push_back(minus_infinity);
 
@@ -1022,25 +963,24 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   bound_sup_float.from_float(1e7f);
   bound_inf_float.change_spec(float_spec);
   bound_sup_float.change_spec(float_spec);
-  constant_exprt bound_inf=bound_inf_float.to_expr();
-  constant_exprt bound_sup=bound_sup_float.to_expr();
+  const constant_exprt bound_inf = bound_inf_float.to_expr();
+  const constant_exprt bound_sup = bound_sup_float.to_expr();
 
-  and_exprt is_simple_float(
-    binary_relation_exprt(arg, ID_ge, bound_inf),
-    binary_relation_exprt(arg, ID_lt, bound_sup));
+  const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
+                                  binary_relation_exprt(arg, ID_lt, bound_sup)};
   condition_list.push_back(is_simple_float);
 
-  refined_string_exprt simple_notation = string_expr_of_function(
+  const refined_string_exprt simple_notation = string_expr_of_function(
     ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
   string_expr_list.push_back(simple_notation);
 
   // Case of a negative number in simple notation
-  and_exprt is_neg_simple_float(
+  const and_exprt is_neg_simple_float{
     binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
-    binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup)));
+    binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
   condition_list.push_back(is_neg_simple_float);
 
-  refined_string_exprt neg_simple_notation = string_expr_of_function(
+  const refined_string_exprt neg_simple_notation = string_expr_of_function(
     ID_cprover_string_concat_func,
     {minus_sign, simple_notation},
     loc,
@@ -1073,7 +1013,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 }
 
 /// Generate the goto code for string initialization.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: the type of the function call
 /// \param loc: location in program
 /// \param symbol_table: the symbol table to populate
@@ -1088,7 +1028,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 ///     cprover_string = {.=cprover_string_length, .=cprover_string_array};
 ///
 code_blockt java_string_library_preprocesst::make_init_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
@@ -1107,11 +1047,12 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
   code_blockt code;
 
   // Processing parameters
-  exprt::operandst args=process_parameters(params, loc, symbol_table, code);
+  const exprt::operandst args =
+    process_parameters(params, loc, function_id, symbol_table, code);
 
   // string_expr <- function(arg1)
-  refined_string_exprt string_expr =
-    string_expr_of_function(function_name, args, loc, symbol_table, code);
+  const refined_string_exprt string_expr =
+    string_expr_of_function(function_id, args, loc, symbol_table, code);
 
   // arg_this <- string_expr
   code.add(
@@ -1124,40 +1065,39 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
 
 /// Call a cprover internal function, assign the result to object `this` and
 /// return it.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: the type of the function call
 /// \param loc: location in program
 /// \param symbol_table: the symbol table to populate
 /// \return Code calling function with the given function name.
 code_blockt
 java_string_library_preprocesst::make_assign_and_return_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
   // This is similar to assign functions except we return a pointer to `this`
-  java_method_typet::parameterst params = type.parameters();
+  const java_method_typet::parameterst &params = type.parameters();
   PRECONDITION(!params.empty());
   PRECONDITION(!params[0].get_identifier().empty());
   code_blockt code;
   code.add(
-    make_assign_function_from_call(function_name, type, loc, symbol_table),
-    loc);
+    make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
   const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
   code.add(code_returnt(arg_this), loc);
   return code;
 }
 
 /// Call a cprover internal function and assign the result to object `this`.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: the type of the function call
 /// \param loc: location in program
 /// \param symbol_table: the symbol table to populate
 /// \return Code assigning result of a call to the function with given function
 ///   name.
 code_blockt java_string_library_preprocesst::make_assign_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
@@ -1165,7 +1105,7 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
   // This is similar to initialization function except we do not ignore
   // the first argument
   return make_init_function_from_call(
-    function_name, type, loc, symbol_table, false);
+    function_id, type, loc, symbol_table, false);
 }
 
 /// Adds to the code an assignment of the form
@@ -1182,6 +1122,7 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
 ///   one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int,
 ///   ID_long, ID_float, ID_double, ID_void
 /// \param loc: a location in the source
+/// \param function_id: the name of the function
 /// \param symbol_table: the symbol table
 /// \param code: code block to which we are adding some assignments
 /// \return An expression containing a symbol `tmp_type_name` where `type_name`
@@ -1192,6 +1133,7 @@ java_string_library_preprocesst::get_primitive_value_of_object(
   const exprt &object,
   irep_idt type_name,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -1246,10 +1188,10 @@ java_string_library_preprocesst::get_primitive_value_of_object(
   DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
 
   // declare tmp_type_name to hold the value
-  std::string aux_name="tmp_"+id2string(type_name);
-  symbolt symbol=get_fresh_aux_symbol(
-    value_type, aux_name, aux_name, loc, ID_java, symbol_table);
-  auto value = symbol.symbol_expr();
+  const std::string aux_name = "tmp_" + id2string(type_name);
+  const symbolt &symbol =
+    fresh_java_symbol(value_type, aux_name, loc, function_id, symbol_table);
+  const auto value = symbol.symbol_expr();
 
   // Check that the type of the object is in the symbol table,
   // otherwise there is no safe way of finding its value.
@@ -1263,10 +1205,11 @@ java_string_library_preprocesst::get_primitive_value_of_object(
       struct_type.get_component("value");
     if(!value_comp.is_nil())
     {
-      pointer_typet pointer_type=::pointer_type(struct_type);
-      dereference_exprt deref(
-        typecast_exprt(object, pointer_type), pointer_type.subtype());
-      member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
+      const pointer_typet struct_pointer_type = pointer_type(struct_type);
+      dereference_exprt deref{typecast_exprt(object, struct_pointer_type),
+                              struct_pointer_type.subtype()};
+      const member_exprt deref_value{
+        std::move(deref), value_comp.get_name(), value_comp.type()};
       code.add(code_assignt(value, deref_value), loc);
       return value;
     }
@@ -1290,14 +1233,14 @@ dereference_exprt java_string_library_preprocesst::get_object_at_index(
   const exprt &argv,
   std::size_t index)
 {
-  dereference_exprt deref_objs(argv, argv.type().subtype());
-  pointer_typet empty_pointer = pointer_type(java_void_type());
-  pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
-  member_exprt data_member(deref_objs, "data", pointer_of_pointer);
-  plus_exprt data_pointer_plus_index(
-    data_member, from_integer(index, java_int_type()), data_member.type());
-  return dereference_exprt(
-    data_pointer_plus_index, data_pointer_plus_index.type().subtype());
+  const dereference_exprt deref_objs{argv, argv.type().subtype()};
+  const pointer_typet empty_pointer = pointer_type(java_void_type());
+  const pointer_typet pointer_of_pointer = pointer_type(empty_pointer);
+  const member_exprt data_member{deref_objs, "data", pointer_of_pointer};
+  const plus_exprt data_pointer_plus_index{
+    data_member, from_integer(index, java_int_type()), data_member.type()};
+  return dereference_exprt{data_pointer_plus_index,
+                           data_pointer_plus_index.type().subtype()};
 }
 
 /// Helper for format function. Adds code:
@@ -1352,8 +1295,8 @@ struct_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, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
+      const symbolt &field_symbol =
+        fresh_java_symbol(type, tmp_name, loc, function_id, symbol_table);
       auto field_symbol_expr = field_symbol.symbol_expr();
       field_expr = field_symbol_expr;
       code.add(code_declt(field_symbol_expr), loc);
@@ -1367,15 +1310,10 @@ struct_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(),
-    id2string(function_id),
-    "tmp_format_obj",
-    loc,
-    ID_java,
-    symbol_table);
-  symbol_exprt arg_i=object_symbol.symbol_expr();
+  const exprt obj = get_object_at_index(argv, index);
+  const symbolt &object_symbol = fresh_java_symbol(
+    obj.type(), "tmp_format_obj", loc, function_id, symbol_table);
+  const symbol_exprt arg_i = object_symbol.symbol_expr();
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
@@ -1402,9 +1340,9 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
 
     if(name=="string_expr")
     {
-      pointer_typet string_pointer =
+      const pointer_typet string_pointer =
         java_reference_type(struct_tag_typet("java::java.lang.String"));
-      typecast_exprt arg_i_as_string(arg_i, string_pointer);
+      const typecast_exprt arg_i_as_string{arg_i, string_pointer};
       code_assign_java_string_to_string_expr(
         to_string_expr(field_expr),
         arg_i_as_string,
@@ -1415,7 +1353,7 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
     else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
     {
       const auto value = get_primitive_value_of_object(
-        arg_i, name, loc, symbol_table, code_not_null);
+        arg_i, name, loc, function_id, symbol_table, code_not_null);
       if(value.has_value())
         code_not_null.add(code_assignt(field_expr, *value), loc);
       else
@@ -1450,8 +1388,8 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
 {
   PRECONDITION(type.parameters().size()==2);
   code_blockt code;
-  exprt::operandst args=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  exprt::operandst args =
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
   INVARIANT(args.size()==2, "String.format should have two arguments");
 
   // The argument can be:
@@ -1477,9 +1415,9 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
       make_argument_for_format(
         args[1], i, structured_type, loc, function_id, symbol_table, code));
 
-  refined_string_exprt string_expr = string_expr_of_function(
+  const 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(
+  const exprt java_string = allocate_fresh_string(
     type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1517,22 +1455,21 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
   code_blockt code;
 
   // > Class class1;
-  pointer_typet class_type=
-    java_reference_type(
-      symbol_table.lookup_ref("java::java.lang.Class").type);
-  symbolt class1_sym=get_fresh_aux_symbol(
-    class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
-  symbol_exprt class1=class1_sym.symbol_expr();
+  const pointer_typet class_type =
+    java_reference_type(symbol_table.lookup_ref("java::java.lang.Class").type);
+  const symbolt &class1_sym = fresh_java_symbol(
+    class_type, "class_symbol", loc, function_id, symbol_table);
+  const symbol_exprt class1 = class1_sym.symbol_expr();
   code.add(code_declt(class1), loc);
 
   // class_identifier is this->@class_identifier
-  member_exprt class_identifier(
+  const member_exprt class_identifier(
     checked_dereference(this_obj, this_obj.type().subtype()),
     "@class_identifier",
     string_typet());
 
   // string_expr = cprover_string_literal(this->@class_identifier)
-  refined_string_exprt string_expr = string_expr_of_function(
+  const refined_string_exprt string_expr = string_expr_of_function(
     ID_cprover_string_literal_func,
     {class_identifier},
     loc,
@@ -1541,7 +1478,7 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
 
   // string_expr1 = substr(string_expr, 6)
   // We do this to remove the "java::" prefix
-  refined_string_exprt string_expr1 = string_expr_of_function(
+  const refined_string_exprt string_expr1 = string_expr_of_function(
     ID_cprover_string_substring_func,
     {string_expr, from_integer(6, java_int_type())},
     loc,
@@ -1549,9 +1486,9 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
     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(
+  const pointer_typet string_ptr_type =
+    java_reference_type(symbol_table.lookup_ref("java::java.lang.String").type);
+  const exprt string1 = allocate_fresh_string(
     string_ptr_type, loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1576,46 +1513,46 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
 
 /// Provide code for a function that calls a function from the solver and simply
 /// returns it.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: type of the function
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// return function_name(args)
+/// return function_id(args)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~
 code_blockt java_string_library_preprocesst::make_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
   code_blockt code;
-  exprt::operandst args=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  const exprt::operandst args =
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
   code.add(
     code_return_function_application(
-      function_name, args, type.return_type(), symbol_table),
+      function_id, args, type.return_type(), symbol_table),
     loc);
   return code;
 }
 
 /// Provide code for a function that calls a function from the solver and return
 /// the string_expr result as a Java string.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: type of the function
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// string_expr = function_name(args)
+/// string_expr = function_id(args)
 /// string = new String
 /// string = string_expr_to_string(string)
 /// return string
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 code_blockt
 java_string_library_preprocesst::make_string_returning_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
@@ -1624,16 +1561,16 @@ java_string_library_preprocesst::make_string_returning_function_from_call(
   code_blockt code;
 
   // Calling the function
-  exprt::operandst arguments=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  const exprt::operandst arguments =
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
 
   // String expression that will hold the result
-  refined_string_exprt string_expr =
-    string_expr_of_function(function_name, arguments, loc, symbol_table, code);
+  const refined_string_exprt string_expr =
+    string_expr_of_function(function_id, arguments, loc, symbol_table, code);
 
   // Assign to string
-  exprt str = allocate_fresh_string(
-    type.return_type(), loc, function_name, symbol_table, code);
+  const 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, true),
@@ -1668,17 +1605,18 @@ code_blockt java_string_library_preprocesst::make_copy_string_code(
   code_blockt code;
 
   // String expression that will hold the result
-  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt string_expr =
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   // Assign the argument to string_expr
-  java_method_typet::parametert op = type.parameters()[0];
+  const java_method_typet::parametert &op = type.parameters()[0];
   PRECONDITION(!op.get_identifier().empty());
-  symbol_exprt arg0(op.get_identifier(), op.type());
+  const symbol_exprt arg0{op.get_identifier(), op.type()};
   code_assign_java_string_to_string_expr(
     string_expr, arg0, loc, symbol_table, code);
 
   // Allocate and assign the string
-  exprt str = allocate_fresh_string(
+  const exprt str = allocate_fresh_string(
     type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1714,18 +1652,19 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code(
   code_blockt code;
 
   // String expression that will hold the result
-  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt string_expr =
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   // Assign argument to a string_expr
-  java_method_typet::parameterst params = type.parameters();
+  const java_method_typet::parameterst &params = type.parameters();
   PRECONDITION(!params[0].get_identifier().empty());
   PRECONDITION(!params[1].get_identifier().empty());
-  symbol_exprt arg1(params[1].get_identifier(), params[1].type());
+  const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
   code_assign_java_string_to_string_expr(
     string_expr, arg1, loc, symbol_table, code);
 
   // Assign string_expr to `this` object
-  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
+  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
   code.add(
     code_assign_string_expr_to_java_string(
       arg_this, string_expr, symbol_table, true),
@@ -1753,10 +1692,10 @@ code_returnt java_string_library_preprocesst::make_string_length_code(
 {
   (void)function_id;
 
-  java_method_typet::parameterst params = type.parameters();
+  const java_method_typet::parameterst &params = type.parameters();
   PRECONDITION(!params[0].get_identifier().empty());
-  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
-  dereference_exprt deref =
+  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
+  const dereference_exprt deref =
     checked_dereference(arg_this, arg_this.type().subtype());
 
   code_returnt ret(get_length(deref, symbol_table));
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index a825f2129f1..12d4a4f8774 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -185,6 +185,7 @@ class java_string_library_preprocesst:public messaget
   exprt::operandst process_parameters(
     const java_method_typet::parameterst &params,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
@@ -193,6 +194,7 @@ class java_string_library_preprocesst:public messaget
     java_string_library_preprocesst &preprocess,
     const exprt &deref,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table,
     code_blockt &init_code);
 
@@ -200,38 +202,32 @@ class java_string_library_preprocesst:public messaget
     const exprt &deref,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
+    const irep_idt &function_name,
     code_blockt &init_code);
 
   exprt::operandst process_operands(
     const exprt::operandst &operands,
     const source_locationt &loc,
-    symbol_table_baset &symbol_table,
-    code_blockt &init_code);
-
-  exprt::operandst process_equals_function_operands(
-    const exprt::operandst &operands,
-    const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
   refined_string_exprt replace_char_array(
     const exprt &array_pointer,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
   symbol_exprt fresh_string(
     const typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
-  symbol_exprt fresh_array(
-    const typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table);
-
   refined_string_exprt decl_string_expr(
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
@@ -249,13 +245,13 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   codet code_return_function_application(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const exprt::operandst &arguments,
     const typet &type,
     symbol_table_baset &symbol_table);
 
   refined_string_exprt string_expr_of_function(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const exprt::operandst &arguments,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
@@ -288,32 +284,32 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   code_blockt make_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_init_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
     bool is_constructor = true);
 
   code_blockt make_assign_and_return_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_assign_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_string_returning_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
@@ -331,6 +327,7 @@ class java_string_library_preprocesst:public messaget
     const exprt &object,
     irep_idt type_name,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
@@ -348,6 +345,7 @@ void add_pointer_to_array_association(
   const exprt &array,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 void add_array_to_length_association(
@@ -355,6 +353,7 @@ void add_array_to_length_association(
   const exprt &length,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 void add_character_set_constraint(
@@ -363,6 +362,7 @@ void add_character_set_constraint(
   const irep_idt &char_set,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
index 86b8d1043bd..234c136d3fd 100644
--- a/jbmc/src/java_bytecode/java_utils.cpp
+++ b/jbmc/src/java_bytecode/java_utils.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_root_class.h"
 
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/message.h>
@@ -433,3 +434,23 @@ const std::unordered_set<std::string> cprover_methods_to_ignore
   "endThread",
   "getCurrentThreadID"
 };
+
+/// \param type: type of new symbol
+/// \param basename_prefix: new symbol will be named
+///   function_name::basename_prefix$num
+/// \param source_location: new symbol source loc
+/// \param function_name: name of the function in which the symbol is defined
+/// \param symbol_table: table to add the new symbol to
+/// \return fresh-named symbol with the requested name pattern
+symbolt &fresh_java_symbol(
+  const typet &type,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &function_name,
+  symbol_table_baset &symbol_table)
+{
+  PRECONDITION(!function_name.empty());
+  const std::string name_prefix = id2string(function_name);
+  return get_fresh_aux_symbol(
+    type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
+}
diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h
index 128d6268671..70d1b30d504 100644
--- a/jbmc/src/java_bytecode/java_utils.h
+++ b/jbmc/src/java_bytecode/java_utils.h
@@ -109,4 +109,11 @@ bool is_non_null_library_global(const irep_idt &);
 
 extern const std::unordered_set<std::string> cprover_methods_to_ignore;
 
+symbolt &fresh_java_symbol(
+  const typet &type,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &function_name,
+  symbol_table_baset &symbol_table);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp
index 24a0260953a..cfcb04fed7d 100644
--- a/jbmc/src/java_bytecode/remove_instanceof.cpp
+++ b/jbmc/src/java_bytecode/remove_instanceof.cpp
@@ -10,12 +10,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// Remove Instance-of Operators
 
 #include "remove_instanceof.h"
+#include "java_utils.h"
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
-#include <util/fresh_symbol.h>
 #include <java_bytecode/java_types.h>
 
 #include <sstream>
@@ -116,20 +116,18 @@ bool remove_instanceoft::lower_instanceof(
   auto jlo = to_struct_tag_type(java_lang_object_type().subtype());
   exprt object_clsid = get_class_identifier_field(check_ptr, jlo, ns);
 
-  symbolt &clsid_tmp_sym = get_fresh_aux_symbol(
+  symbolt &clsid_tmp_sym = fresh_java_symbol(
     object_clsid.type(),
-    id2string(function_identifier),
     "class_identifier_tmp",
-    source_locationt(),
-    ID_java,
+    this_inst->source_location,
+    function_identifier,
     symbol_table);
 
-  symbolt &instanceof_result_sym = get_fresh_aux_symbol(
+  symbolt &instanceof_result_sym = fresh_java_symbol(
     bool_typet(),
-    id2string(function_identifier),
     "instanceof_result_tmp",
-    source_locationt(),
-    ID_java,
+    this_inst->source_location,
+    function_identifier,
     symbol_table);
 
   // Create
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
index 6750ac30fd6..6825005ca5f 100644
--- a/jbmc/src/java_bytecode/remove_java_new.cpp
+++ b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -14,11 +14,11 @@ Author: Peter Schrammel
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
+#include "java_utils.h"
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_cast.h>
 #include <util/expr_initializer.h>
-#include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
 
@@ -212,12 +212,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // Must directly assign the new array to a temporary
   // because goto-symex will notice `x=side_effect_exprt` but not
   // `x=typecast_exprt(side_effect_exprt(...))`
-  symbol_exprt new_array_data_symbol = get_fresh_aux_symbol(
+  symbol_exprt new_array_data_symbol = fresh_java_symbol(
                                          data_java_new_expr.type(),
-                                         id2string(function_identifier),
                                          "tmp_new_data_array",
                                          location,
-                                         ID_java,
+                                         function_identifier,
                                          symbol_table)
                                          .symbol_expr();
   code_declt array_decl(new_array_data_symbol);
@@ -260,14 +259,10 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
     goto_programt tmp;
 
-    symbol_exprt tmp_i = get_fresh_aux_symbol(
-                           length.type(),
-                           id2string(function_identifier),
-                           "tmp_index",
-                           location,
-                           ID_java,
-                           symbol_table)
-                           .symbol_expr();
+    symbol_exprt tmp_i =
+      fresh_java_symbol(
+        length.type(), "tmp_index", location, function_identifier, symbol_table)
+        .symbol_expr();
     code_declt decl(tmp_i);
     decl.add_source_location() = location;
     goto_programt::targett t_decl = tmp.insert_before(tmp.instructions.begin());
@@ -292,14 +287,10 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
       plus_exprt(data, tmp_i), data.type().subtype());
 
     code_blockt for_body;
-    symbol_exprt init_sym = get_fresh_aux_symbol(
-                              sub_type,
-                              id2string(function_identifier),
-                              "subarray_init",
-                              location,
-                              ID_java,
-                              symbol_table)
-                              .symbol_expr();
+    symbol_exprt init_sym =
+      fresh_java_symbol(
+        sub_type, "subarray_init", location, function_identifier, symbol_table)
+        .symbol_expr();
     code_declt init_decl(init_sym);
     init_decl.add_source_location() = location;
     for_body.add(std::move(init_decl));
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 4c75878c20c..378f9c14da7 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -14,7 +14,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_object_factory.h>
 #include <java_bytecode/java_pointer_casts.h>
 
-#include <util/fresh_symbol.h>
+#include "java_utils.h"
 #include <util/invariant_utils.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
@@ -161,12 +161,11 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
   {
     const auto &this_argument = required_type.parameters()[0];
     const typet &this_type = this_argument.type();
-    symbolt &init_symbol = get_fresh_aux_symbol(
+    symbolt &init_symbol = fresh_java_symbol(
       this_type,
-      id2string(symbol.name),
       "to_construct",
       synthesized_source_location,
-      ID_java,
+      symbol.name,
       symbol_table);
     const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
     code_assignt get_argument(
@@ -189,12 +188,11 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
     const typet &required_return_type = required_type.return_type();
     if(required_return_type != java_void_type())
     {
-      symbolt &to_return_symbol = get_fresh_aux_symbol(
+      symbolt &to_return_symbol = fresh_java_symbol(
         required_return_type,
-        id2string(symbol.name),
         "to_return",
         synthesized_source_location,
-        ID_java,
+        symbol.name,
         symbol_table);
       const exprt &to_return = to_return_symbol.symbol_expr();
       if(to_return_symbol.type.id() != ID_pointer)
diff --git a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
index 283c81f0c37..11a316fc387 100644
--- a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
+++ b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -21,11 +21,12 @@ refined_string_exprt convert_exprt_to_string_exprt_unit_test(
   java_string_library_preprocesst &preprocess,
   const exprt &deref,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_tablet &symbol_table,
   code_blockt &init_code)
 {
   return preprocess.convert_exprt_to_string_exprt(
-    deref, loc, symbol_table, init_code);
+    deref, loc, symbol_table, function_id, init_code);
 }
 
 TEST_CASE("Convert exprt to string exprt")
@@ -33,6 +34,7 @@ TEST_CASE("Convert exprt to string exprt")
   GIVEN("A location, a string expression, and a symbol table")
   {
     source_locationt loc;
+    loc.set_function("function_name");
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
     code_blockt code;
@@ -45,9 +47,9 @@ TEST_CASE("Convert exprt to string exprt")
     {
       refined_string_exprt string_expr =
         convert_exprt_to_string_exprt_unit_test(
-          preprocess, expr, loc, symbol_table, code);
+          preprocess, expr, loc, "function_id", symbol_table, code);
 
-      THEN("The type of the returd expression is that of refined strings")
+      THEN("The type of the returned expression is that of refined strings")
       {
         REQUIRE(string_expr.id() == ID_struct);
         REQUIRE(is_refined_string_type(string_expr.type()));