diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 94a34f48000..9c170c7d224 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -869,7 +869,7 @@ void jbmc_parse_optionst::process_goto_function(
     if(using_symex_driven_loading)
     {
       // label the assertions
-      label_properties(goto_function.body);
+      label_properties(goto_function.body, function.get_function_id());
 
       goto_function.body.update();
       function.compute_location_numbers();
diff --git a/regression/cbmc/unique_labels1/bar.c b/regression/cbmc/unique_labels1/bar.c
new file mode 100644
index 00000000000..6f8d74c6062
--- /dev/null
+++ b/regression/cbmc/unique_labels1/bar.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(1 < 0);
+}
+
+void bar()
+{
+  foo();
+}
diff --git a/regression/cbmc/unique_labels1/main.c b/regression/cbmc/unique_labels1/main.c
new file mode 100644
index 00000000000..85c33c635b8
--- /dev/null
+++ b/regression/cbmc/unique_labels1/main.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(0);
+}
+
+void bar();
+
+int main()
+{
+  foo();
+  bar();
+}
diff --git a/regression/cbmc/unique_labels1/test.desc b/regression/cbmc/unique_labels1/test.desc
new file mode 100644
index 00000000000..cd854477093
--- /dev/null
+++ b/regression/cbmc/unique_labels1/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+bar.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+assertion\.2
+--
+Each of the assertions in the two functions named "foo" should have a unique
+prefix, and thus be numbered "<prefix>.assertion.1."
diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc
index 908ec83b393..aa43497a7ce 100644
--- a/regression/contracts/function_check_04/test.desc
+++ b/regression/contracts/function_check_04/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --apply-code-contracts
 ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
-^\[foo.1\] line 9 .*: FAILURE$
+^\[__CPROVER_initialize.1\] line 9 .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index c2d6698d3e1..53698881ebd 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/src/ansi-c/ansi_c_declaration.cpp
@@ -131,14 +131,14 @@ void ansi_c_declarationt::to_symbol(
   symbol.value=declarator.value();
   symbol.type=full_type(declarator);
   symbol.name=declarator.get_name();
-  symbol.pretty_name=symbol.name;
-  symbol.base_name=declarator.get_base_name();
+  symbol.display_name=declarator.get_base_name();
   symbol.is_type=get_is_typedef();
   symbol.location=declarator.source_location();
   symbol.is_extern=get_is_extern();
   symbol.is_macro=get_is_typedef() || get_is_enum_constant();
   symbol.is_parameter=get_is_parameter();
   symbol.is_weak=get_is_weak();
+  symbol.has_local_scope = !get_is_global();
 
   // is it a function?
 
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index f53b09b1d5a..1456aa0043e 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -206,7 +206,12 @@ symbol_exprt c_nondet_symbol_factory(
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
   CHECK_RETURN(!moving_symbol_failed);
 
-  symbol_factoryt state(symbol_table, loc, object_factory_parameters, lifetime);
+  symbol_factoryt state(
+    symbol_table,
+    loc,
+    goto_functionst::entry_point(),
+    object_factory_parameters,
+    lifetime);
 
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
index 9ccda4d90f9..6653b56dcff 100644
--- a/src/ansi-c/c_nondet_symbol_factory.h
+++ b/src/ansi-c/c_nondet_symbol_factory.h
@@ -38,13 +38,14 @@ class symbol_factoryt
   symbol_factoryt(
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
+    const irep_idt &name_prefix,
     const c_object_factory_parameterst &object_factory_params,
     const lifetimet lifetime)
     : symbol_table(_symbol_table),
       loc(loc),
       ns(_symbol_table),
       object_factory_params(object_factory_params),
-      allocate_objects(ID_C, loc, loc.get_function(), symbol_table),
+      allocate_objects(ID_C, loc, name_prefix, symbol_table),
       lifetime(lifetime)
   {
   }
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 006e75dfea5..083ce0d26f8 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -160,6 +160,8 @@ void expr2ct::get_shorthands(const exprt &expr)
       irep_idt func;
 
       const symbolt *symbol;
+      // we use the source-level function name as a means to detect collisions,
+      // which is ok, because this is about generating user-visible output
       if(!ns.lookup(symbol_id, symbol))
         func=symbol->location.get_function();
 
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index d7301bb147c..d12c81a56f3 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -38,11 +38,18 @@ static std::string type2name_tag(
   if(ns.lookup(identifier, symbol))
     return "SYM#"+id2string(identifier)+"#";
 
+  std::string result;
+
+  // this isn't really a qualifier, but the linker needs to
+  // distinguish these - should likely be fixed in the linker instead
+  if(symbol->has_local_scope)
+    result += 'l';
+
   assert(symbol && symbol->is_type);
 
   if(symbol->type.id()!=ID_struct &&
      symbol->type.id()!=ID_union)
-    return type2name(symbol->type, ns, symbol_number);
+    return result + type2name(symbol->type, ns, symbol_number);
 
   // assign each symbol a number when seen for the first time
   std::pair<symbol_numbert::iterator, bool> entry=
@@ -50,9 +57,8 @@ static std::string type2name_tag(
         identifier,
         std::make_pair(symbol_number.size(), true)));
 
-  std::string result = "SYM" +
-                       id2string(to_struct_union_type(symbol->type).get_tag()) +
-                       '#' + std::to_string(entry.first->second.first);
+  result += "SYM" + id2string(to_struct_union_type(symbol->type).get_tag()) +
+            '#' + std::to_string(entry.first->second.first);
 
   // new entry, add definition
   if(entry.second)
@@ -99,11 +105,6 @@ static std::string type2name(
   if(type.get_bool(ID_C_noreturn))
     result+='n';
 
-  // this isn't really a qualifier, but the linker needs to
-  // distinguish these - should likely be fixed in the linker instead
-  if(!type.source_location().get_function().empty())
-    result+='l';
-
   if(type.id().empty())
     throw "empty type encountered";
   else if(type.id()==ID_empty)
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 13b9f4821ac..9f3f788ef1a 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -426,6 +426,8 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   symbol.is_type=is_typedef;
   symbol.is_macro=is_typedef && !is_template_parameter;
   symbol.pretty_name=pretty_name;
+  symbol.has_local_scope =
+    !cpp_typecheck.cpp_scopes.current_scope().is_global_scope();
 
   // Constant? These are propagated.
   if(symbol.type.get_bool(ID_C_constant) &&
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 432e33c5976..9e7891f8a75 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -233,6 +233,7 @@ void cpp_typecheckt::typecheck_compound_type(
       cpp_scopes.current_scope().suffix;
     symbol.type.set(
       ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));
+    symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
     // move early, must be visible before doing body
     symbolt *new_symbol;
diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp
index 061946fb763..1373366f79a 100644
--- a/src/cpp/cpp_typecheck_enum_type.cpp
+++ b/src/cpp/cpp_typecheck_enum_type.cpp
@@ -178,6 +178,7 @@ void cpp_typecheckt::typecheck_enum_type(typet &type)
     symbol.is_type=true;
     symbol.is_macro=false;
     symbol.pretty_name=pretty_name;
+    symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
     // move early, must be visible before doing body
     symbolt *new_symbol;
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index b4dadc6422d..c34ce8e7dab 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -178,6 +178,7 @@ void cpp_typecheckt::typecheck_class_template(
 
   symbol.pretty_name=
     cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
+  symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
   symbolt *new_symbol;
   if(symbol_table.move(symbol, new_symbol))
diff --git a/src/goto-instrument/aggressive_slicer.cpp b/src/goto-instrument/aggressive_slicer.cpp
index 3e047c6285c..b330ed6ae71 100644
--- a/src/goto-instrument/aggressive_slicer.cpp
+++ b/src/goto-instrument/aggressive_slicer.cpp
@@ -92,7 +92,7 @@ void aggressive_slicert::doit()
     auto property_loc = find_property(p, goto_model.goto_functions);
     if(!property_loc.has_value())
       throw "unable to find property in call graph";
-    note_functions_to_keep(property_loc.value().get_function());
+    note_functions_to_keep(property_loc->first);
   }
 
   // Add functions within distance of shortest path functions
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index 47caa7848a8..daad5dd7487 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -61,7 +61,9 @@ class code_contractst
 
   const symbolt &new_tmp_symbol(
     const typet &type,
-    const source_locationt &source_location);
+    const source_locationt &source_location,
+    const irep_idt &function_id,
+    const irep_idt &mode);
 };
 
 static void check_apply_invariants(
@@ -248,14 +250,16 @@ void code_contractst::code_contracts(
 
 const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
-  const source_locationt &source_location)
+  const source_locationt &source_location,
+  const irep_idt &function_id,
+  const irep_idt &mode)
 {
   return get_fresh_aux_symbol(
     type,
-    id2string(source_location.get_function()),
+    id2string(function_id) + "::tmp_cc",
     "tmp_cc",
     source_location,
-    irep_idt(),
+    mode,
     symbol_table);
 }
 
@@ -301,7 +305,8 @@ void code_contractst::add_contract_check(
   g->source_location=skip->source_location;
 
   // prepare function call including all declarations
-  code_function_callt call(ns.lookup(function).symbol_expr());
+  const symbolt &function_symbol = ns.lookup(function);
+  code_function_callt call(function_symbol.symbol_expr());
   replace_symbolt replace;
 
   // decl ret
@@ -310,9 +315,12 @@ void code_contractst::add_contract_check(
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
-    symbol_exprt r=
-      new_tmp_symbol(gf.type.return_type(),
-                     d->source_location).symbol_expr();
+    symbol_exprt r = new_tmp_symbol(
+                       gf.type.return_type(),
+                       d->source_location,
+                       function,
+                       function_symbol.mode)
+                       .symbol_expr();
     d->code=code_declt(r);
 
     call.lhs()=r;
@@ -330,9 +338,10 @@ void code_contractst::add_contract_check(
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
-    symbol_exprt p=
-      new_tmp_symbol(p_it->type(),
-                     d->source_location).symbol_expr();
+    symbol_exprt p =
+      new_tmp_symbol(
+        p_it->type(), d->source_location, function, function_symbol.mode)
+        .symbol_expr();
     d->code=code_declt(p);
 
     call.arguments().push_back(p);
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index a6069441905..7139882c3ab 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -168,11 +168,9 @@ void dump_ct::operator()(std::ostream &os)
     const symbolt &symbol=ns.lookup(*it);
     const irep_idt &type_id=symbol.type.id();
 
-    if(symbol.is_type &&
-       symbol.location.get_function().empty() &&
-       (type_id==ID_struct ||
-        type_id==ID_union ||
-        type_id==ID_c_enum))
+    if(
+      symbol.is_type && !symbol.has_local_scope &&
+      (type_id == ID_struct || type_id == ID_union || type_id == ID_c_enum))
     {
       if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       {
@@ -293,7 +291,7 @@ void dump_ct::convert_compound_declaration(
     const symbolt &symbol,
     std::ostream &os_body)
 {
-  if(!symbol.location.get_function().empty())
+  if(symbol.has_local_scope)
     return;
 
   // do compound type body
@@ -737,8 +735,7 @@ void dump_ct::gather_global_typedefs()
   {
     const symbolt &symbol=symbol_entry.second;
 
-    if(symbol.is_macro && symbol.is_type &&
-       symbol.location.get_function().empty())
+    if(symbol.is_macro && symbol.is_type && !symbol.has_local_scope)
     {
       const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
       PRECONDITION(!typedef_str.empty());
@@ -843,9 +840,10 @@ void dump_ct::convert_global_variable(
     std::ostream &os,
     local_static_declst &local_static_decls)
 {
-  const irep_idt &func=symbol.location.get_function();
-  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
-      !converted_global.insert(symbol.name).second)
+  const bool global = !symbol.has_local_scope;
+  if(
+    (global || symbol.is_extern || symbol.value.is_not_nil()) &&
+    !converted_global.insert(symbol.name).second)
     return;
 
   code_declt d(symbol.symbol_expr());
@@ -856,8 +854,7 @@ void dump_ct::convert_global_variable(
 
   // add a tentative declaration to cater for symbols in the initializer
   // relying on it this symbol
-  if((func.empty() || symbol.is_extern) &&
-     (symbol.value.is_nil() || !syms.empty()))
+  if((global || symbol.is_extern) && (symbol.value.is_nil() || !syms.empty()))
   {
     os << "// " << symbol.name << '\n';
     os << "// " << symbol.location << '\n';
@@ -889,7 +886,7 @@ void dump_ct::convert_global_variable(
     d.copy_to_operands(symbol.value);
   }
 
-  if(!func.empty() && !symbol.is_extern)
+  if(!global && !symbol.is_extern)
   {
     local_static_decls.emplace(symbol.name, d);
   }
diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp
index 3559caae777..21d62c42337 100644
--- a/src/goto-instrument/generate_function_bodies.cpp
+++ b/src/goto-instrument/generate_function_bodies.cpp
@@ -169,12 +169,14 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
     const exprt &lhs,
     const std::size_t initial_depth,
     const source_locationt &source_location,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table,
     goto_programt &dest) const
   {
     symbol_factoryt symbol_factory(
       symbol_table,
       source_location,
+      function_id,
       object_factory_parameters,
       lifetimet::DYNAMIC);
 
@@ -235,6 +237,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
           dereference_expr,
           1, // depth 1 since we pass the dereferenced pointer
           function_symbol.location,
+          function_name,
           symbol_table,
           dest);
 
@@ -260,6 +263,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
         symbol_exprt(global_sym.name, global_sym.type),
         0,
         function_symbol.location,
+        irep_idt(),
         symbol_table,
         dest);
 
@@ -291,6 +295,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
         aux_symbol.symbol_expr(),
         0,
         function_symbol.location,
+        function_name,
         symbol_table,
         dest);
 
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 7243c40c446..28d901372f1 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1416,8 +1416,7 @@ void goto_program2codet::add_local_types(const typet &type)
       const irep_idt &identifier=to_symbol_type(type).get_identifier();
       const symbolt &symbol=ns.lookup(identifier);
 
-      if(symbol.location.get_function().empty() ||
-         !type_names_set.insert(identifier).second)
+      if(!symbol.has_local_scope || !type_names_set.insert(identifier).second)
         return;
 
       for(const auto &c : to_struct_union_type(full_type).components())
@@ -1432,8 +1431,7 @@ void goto_program2codet::add_local_types(const typet &type)
     const irep_idt &identifier=to_c_enum_tag_type(type).get_identifier();
     const symbolt &symbol=ns.lookup(identifier);
 
-    if(symbol.location.get_function().empty() ||
-       !type_names_set.insert(identifier).second)
+    if(!symbol.has_local_scope || !type_names_set.insert(identifier).second)
       return;
 
     assert(!identifier.empty());
@@ -1979,11 +1977,10 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
       const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
       const symbolt &symbol=ns.lookup(identifier);
 
-      if(symbol.is_static_lifetime &&
-         symbol.type.id()!=ID_code &&
-         !symbol.is_extern &&
-         !symbol.location.get_function().empty() &&
-         local_static_set.insert(identifier).second)
+      if(
+        symbol.is_static_lifetime && symbol.type.id() != ID_code &&
+        !symbol.is_extern && symbol.has_local_scope &&
+        local_static_set.insert(identifier).second)
       {
         if(symbol.value.is_not_nil())
         {
diff --git a/src/goto-instrument/wmm/abstract_event.h b/src/goto-instrument/wmm/abstract_event.h
index 7509fb53df8..bc5da6816bb 100644
--- a/src/goto-instrument/wmm/abstract_event.h
+++ b/src/goto-instrument/wmm/abstract_event.h
@@ -34,6 +34,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
   irep_idt variable;
   unsigned id;
   source_locationt source_location;
+  irep_idt function_id;
   bool local;
 
   // for ASMfence
@@ -61,10 +62,20 @@ class abstract_eventt:public graph_nodet<empty_edget>
   }
 
   abstract_eventt(
-    operationt _op, unsigned _th, irep_idt _var,
-    unsigned _id, source_locationt _loc, bool _local)
-    :operation(_op), thread(_th), variable(_var), id(_id),
-    source_location(_loc), local(_local)
+    operationt _op,
+    unsigned _th,
+    irep_idt _var,
+    unsigned _id,
+    source_locationt _loc,
+    irep_idt _function_id,
+    bool _local)
+    : operation(_op),
+      thread(_th),
+      variable(_var),
+      id(_id),
+      source_location(_loc),
+      function_id(_function_id),
+      local(_local)
   {
   }
 
@@ -74,6 +85,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
     irep_idt _var,
     unsigned _id,
     source_locationt _loc,
+    irep_idt _function_id,
     bool _local,
     bool WRf,
     bool WWf,
@@ -81,20 +93,21 @@ class abstract_eventt:public graph_nodet<empty_edget>
     bool RWf,
     bool WWc,
     bool RWc,
-    bool RRc):
-    operation(_op),
-    thread(_th),
-    variable(_var),
-    id(_id),
-    source_location(_loc),
-    local(_local),
-    WRfence(RWf),
-    WWfence(WWf),
-    RRfence(RRf),
-    RWfence(WRf),
-    WWcumul(WWc),
-    RWcumul(RWc),
-    RRcumul(RRc)
+    bool RRc)
+    : operation(_op),
+      thread(_th),
+      variable(_var),
+      id(_id),
+      source_location(_loc),
+      function_id(_function_id),
+      local(_local),
+      WRfence(RWf),
+      WWfence(WWf),
+      RRfence(RRf),
+      RWfence(WRf),
+      WWcumul(WWc),
+      RWcumul(RWc),
+      RRcumul(RRc)
   {
   }
 
@@ -106,6 +119,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
     variable=other.variable;
     id=other.id;
     source_location=other.source_location;
+    function_id = other.function_id;
     local=other.local;
   }
 
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
index 575a3fffcd0..95e2a3712ba 100644
--- a/src/goto-instrument/wmm/event_graph.cpp
+++ b/src/goto-instrument/wmm/event_graph.cpp
@@ -94,10 +94,10 @@ event_idt event_grapht::copy_segment(event_idt begin, event_idt end)
   const abstract_eventt &end_event=operator[](end);
 
   /* not sure -- we should allow cross function cycles */
-  if(begin_event.source_location.get_file()!=end_event.source_location
-    .get_file()
-    || begin_event.source_location.get_function()!=end_event.source_location
-    .get_function())
+  if(
+    begin_event.source_location.get_file() !=
+      end_event.source_location.get_file() ||
+    begin_event.function_id != end_event.function_id)
     return end;
 
   if(duplicated_bodies.find(std::make_pair(begin_event, end_event))
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index a4d64441bef..ec6919a8335 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -199,8 +199,8 @@ void instrumentert::cfg_visitort::visit_cfg_function(
       #ifdef ATOMIC_BREAK
       visit_cfg_thread();
       #elif defined ATOMIC_FENCE
-      visit_cfg_fence(i_it);
-      #else
+      visit_cfg_fence(i_it, function_id);
+#else
       /* propagates */
       visit_cfg_propagate(i_it);
       #endif
@@ -222,11 +222,11 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     else if(is_fence(instruction, instrumenter.ns))
     {
       instrumenter.message.debug() << "Constructing a fence" << messaget::eom;
-      visit_cfg_fence(i_it);
+      visit_cfg_fence(i_it, function_id);
     }
     else if(model!=TSO && is_lwfence(instruction, instrumenter.ns))
     {
-      visit_cfg_lwfence(i_it);
+      visit_cfg_lwfence(i_it, function_id);
     }
     else if(model==TSO && is_lwfence(instruction, instrumenter.ns))
     {
@@ -236,7 +236,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     else if(instruction.is_other()
       && instruction.code.get_statement()==ID_fence)
     {
-      visit_cfg_asm_fence(i_it);
+      visit_cfg_asm_fence(i_it, function_id);
     }
     else if(instruction.is_function_call())
     {
@@ -535,6 +535,9 @@ void inline instrumentert::cfg_visitort::visit_cfg_duplicate(
       }
     }
 
+    // The code below uses heuristics to limit false positives: no cycles across
+    // inlined functions, which we would detect when file names or
+    // (user-provided) function names change _within a single goto_program_.
     if(!found_pos
       || new_targ->source_location.get_function()
         !=targ->source_location.get_function()
@@ -742,11 +745,18 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_lwfence(
-  goto_programt::instructionst::iterator i_it)
+  goto_programt::instructionst::iterator i_it,
+  const irep_idt &function_id)
 {
   const goto_programt::instructiont &instruction=*i_it;
-  const abstract_eventt new_fence_event(abstract_eventt::operationt::Lwfence,
-    thread, "f", instrumenter.unique_id++, instruction.source_location, false);
+  const abstract_eventt new_fence_event(
+    abstract_eventt::operationt::Lwfence,
+    thread,
+    "f",
+    instrumenter.unique_id++,
+    instruction.source_location,
+    function_id,
+    false);
   const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
   const event_idt new_fence_gnode=egraph_alt.add_node();
@@ -774,7 +784,8 @@ void instrumentert::cfg_visitort::visit_cfg_lwfence(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_asm_fence(
-  goto_programt::instructionst::iterator i_it)
+  goto_programt::instructionst::iterator i_it,
+  const irep_idt &function_id)
 {
   const goto_programt::instructiont &instruction=*i_it;
   bool WRfence=instruction.code.get_bool(ID_WRfence);
@@ -784,9 +795,21 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence(
   bool WWcumul=instruction.code.get_bool(ID_WWcumul);
   bool RRcumul=instruction.code.get_bool(ID_RRcumul);
   bool RWcumul=instruction.code.get_bool(ID_RWcumul);
-  const abstract_eventt new_fence_event(abstract_eventt::operationt::ASMfence,
-    thread, "asm", instrumenter.unique_id++, instruction.source_location,
-    false, WRfence, WWfence, RRfence, RWfence, WWcumul, RWcumul, RRcumul);
+  const abstract_eventt new_fence_event(
+    abstract_eventt::operationt::ASMfence,
+    thread,
+    "asm",
+    instrumenter.unique_id++,
+    instruction.source_location,
+    function_id,
+    false,
+    WRfence,
+    WWfence,
+    RRfence,
+    RWfence,
+    WWcumul,
+    RWcumul,
+    RRcumul);
   const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
   const event_idt new_fence_gnode=egraph_alt.add_node();
@@ -867,9 +890,14 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     assert(read_expr);
 #endif
 
-    const abstract_eventt new_read_event(abstract_eventt::operationt::Read,
-      thread, id2string(read), instrumenter.unique_id++,
-      instruction.source_location, local(read));
+    const abstract_eventt new_read_event(
+      abstract_eventt::operationt::Read,
+      thread,
+      id2string(read),
+      instrumenter.unique_id++,
+      instruction.source_location,
+      function_id,
+      local(read));
 
     const event_idt new_read_node=egraph.add_node();
     egraph[new_read_node]=new_read_event;
@@ -965,9 +993,14 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     // assert(write_expr);
 
     /* creates Write */
-    const abstract_eventt new_write_event(abstract_eventt::operationt::Write,
-      thread, id2string(write), instrumenter.unique_id++,
-      instruction.source_location, local(write));
+    const abstract_eventt new_write_event(
+      abstract_eventt::operationt::Write,
+      thread,
+      id2string(write),
+      instrumenter.unique_id++,
+      instruction.source_location,
+      function_id,
+      local(write));
 
     const event_idt new_write_node=egraph.add_node();
     egraph[new_write_node](new_write_event);
@@ -1137,11 +1170,18 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_fence(
-  goto_programt::instructionst::iterator i_it)
+  goto_programt::instructionst::iterator i_it,
+  const irep_idt &function_id)
 {
   const goto_programt::instructiont &instruction=*i_it;
-  const abstract_eventt new_fence_event(abstract_eventt::operationt::Fence,
-    thread, "F", instrumenter.unique_id++, instruction.source_location, false);
+  const abstract_eventt new_fence_event(
+    abstract_eventt::operationt::Fence,
+    thread,
+    "F",
+    instrumenter.unique_id++,
+    instruction.source_location,
+    function_id,
+    false);
   const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
   const event_idt new_fence_gnode=egraph_alt.add_node();
@@ -1440,7 +1480,7 @@ void inline instrumentert::print_outputs_local(
       if(render_po_aligned)
         same_po[ev.thread].insert(*it_e);
       if(render_by_function)
-        same_file[ev.source_location.get_function()].insert(*it_e);
+        same_file[ev.function_id].insert(*it_e);
       else if(render_by_file)
         same_file[ev.source_location.get_file()].insert(*it_e);
       if(ev.thread>max_thread)
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
index 377bafbb012..ef0a987ca9a 100644
--- a/src/goto-instrument/wmm/goto2graph.h
+++ b/src/goto-instrument/wmm/goto2graph.h
@@ -142,10 +142,16 @@ class instrumentert
       local_may_aliast &local_may
 #endif
     ); // NOLINT(whitespace/parens)
-    void visit_cfg_fence(goto_programt::instructionst::iterator i_it);
+    void visit_cfg_fence(
+      goto_programt::instructionst::iterator i_it,
+      const irep_idt &function_id);
     void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
-    void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it);
-    void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it);
+    void visit_cfg_lwfence(
+      goto_programt::instructionst::iterator i_it,
+      const irep_idt &function_id);
+    void visit_cfg_asm_fence(
+      goto_programt::instructionst::iterator i_it,
+      const irep_idt &function_id);
     void visit_cfg_function_call(value_setst &value_sets,
       goto_programt::instructionst::iterator i_it,
       memory_modelt model,
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
index 76c47e6b00e..86dc6d5b4f9 100644
--- a/src/goto-programs/read_bin_goto_object.cpp
+++ b/src/goto-programs/read_bin_goto_object.cpp
@@ -60,7 +60,7 @@ static bool read_bin_goto_object_v5(
     sym.is_state_var = (flags &(1 << 9))!=0;
     sym.is_parameter = (flags &(1 << 8))!=0;
     sym.is_auxiliary = (flags &(1 << 7))!=0;
-    // sym.binding = (flags &(1 << 6))!=0;
+    sym.has_local_scope = (flags & (1 << 6)) != 0;
     sym.is_lvalue = (flags &(1 << 5))!=0;
     sym.is_static_lifetime = (flags &(1 << 4))!=0;
     sym.is_thread_local = (flags &(1 << 3))!=0;
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 1768c55c2c9..355d6039d06 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -42,7 +42,9 @@ class remove_function_pointerst
 
   void operator()(goto_functionst &goto_functions);
 
-  bool remove_function_pointers(goto_programt &goto_program);
+  bool remove_function_pointers(
+    goto_programt &goto_program,
+    const irep_idt &function_id);
 
   // a set of function symbols
   using functionst = remove_const_function_pointerst::functionst;
@@ -51,10 +53,12 @@ class remove_function_pointerst
   /// target in the given goto-program by a case-split
   /// over a given set of functions
   /// \param goto_program: The goto program that contains target
+  /// \param function_id: Name of function containing the target
   /// \param target: location with function call with function pointer
   /// \param functions: The set of functions to consider
   void remove_function_pointer(
     goto_programt &goto_program,
+    const irep_idt &function_id,
     goto_programt::targett target,
     const functionst &functions);
 
@@ -76,9 +80,11 @@ class remove_function_pointerst
   /// target in the given goto-program by determining
   /// functions that have a compatible signature
   /// \param goto_program: The goto program that contains target
+  /// \param function_id: Name of function containing the target
   /// \param target: location with function call with function pointer
   void remove_function_pointer(
     goto_programt &goto_program,
+    const irep_idt &function_id,
     goto_programt::targett target);
 
   std::unordered_set<irep_idt> address_taken;
@@ -97,6 +103,7 @@ class remove_function_pointerst
 
   void fix_argument_types(code_function_callt &function_call);
   void fix_return_type(
+    const irep_idt &in_function_id,
     code_function_callt &function_call,
     goto_programt &dest);
 };
@@ -225,6 +232,7 @@ void remove_function_pointerst::fix_argument_types(
 }
 
 void remove_function_pointerst::fix_return_type(
+  const irep_idt &in_function_id,
   code_function_callt &function_call,
   goto_programt &dest)
 {
@@ -245,7 +253,7 @@ void remove_function_pointerst::fix_return_type(
 
   symbolt &tmp_symbol = get_fresh_aux_symbol(
     code_type.return_type(),
-    id2string(function_call.source_location().get_function()),
+    id2string(in_function_id),
     "tmp_return_val_" + id2string(function_symbol.base_name),
     function_call.source_location(),
     function_symbol.mode,
@@ -264,6 +272,7 @@ void remove_function_pointerst::fix_return_type(
 
 void remove_function_pointerst::remove_function_pointer(
   goto_programt &goto_program,
+  const irep_idt &function_id,
   goto_programt::targett target)
 {
   const code_function_callt &code = target->get_function_call();
@@ -352,11 +361,12 @@ void remove_function_pointerst::remove_function_pointer(
     }
   }
 
-  remove_function_pointer(goto_program, target, functions);
+  remove_function_pointer(goto_program, function_id, target, functions);
 }
 
 void remove_function_pointerst::remove_function_pointer(
   goto_programt &goto_program,
+  const irep_idt &function_id,
   goto_programt::targett target,
   const functionst &functions)
 {
@@ -386,7 +396,7 @@ void remove_function_pointerst::remove_function_pointer(
     // the signature of the function might not match precisely
     fix_argument_types(t1->get_function_call());
 
-    fix_return_type(t1->get_function_call(), new_code_calls);
+    fix_return_type(function_id, t1->get_function_call(), new_code_calls);
     // goto final
     goto_programt::targett t3=new_code_calls.add_instruction();
     t3->make_goto(t_final, true_exprt());
@@ -466,7 +476,8 @@ void remove_function_pointerst::remove_function_pointer(
 }
 
 bool remove_function_pointerst::remove_function_pointers(
-  goto_programt &goto_program)
+  goto_programt &goto_program,
+  const irep_idt &function_id)
 {
   bool did_something=false;
 
@@ -477,7 +488,7 @@ bool remove_function_pointerst::remove_function_pointers(
 
       if(code.function().id()==ID_dereference)
       {
-        remove_function_pointer(goto_program, target);
+        remove_function_pointer(goto_program, function_id, target);
         did_something=true;
       }
     }
@@ -499,7 +510,7 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
   {
     goto_programt &goto_program=f_it->second.body;
 
-    if(remove_function_pointers(goto_program))
+    if(remove_function_pointers(goto_program, f_it->first))
       did_something=true;
   }
 
@@ -507,10 +518,12 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
     functions.compute_location_numbers();
 }
 
-bool remove_function_pointers(message_handlert &_message_handler,
+bool remove_function_pointers(
+  message_handlert &_message_handler,
   symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
   goto_programt &goto_program,
+  const irep_idt &function_id,
   bool add_safety_assertion,
   bool only_remove_const_fps)
 {
@@ -522,7 +535,7 @@ bool remove_function_pointers(message_handlert &_message_handler,
       only_remove_const_fps,
       goto_functions);
 
-  return rfp.remove_function_pointers(goto_program);
+  return rfp.remove_function_pointers(goto_program, function_id);
 }
 
 void remove_function_pointers(
diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h
index 4a7bbfb09b5..bff989e1cea 100644
--- a/src/goto-programs/remove_function_pointers.h
+++ b/src/goto-programs/remove_function_pointers.h
@@ -14,6 +14,8 @@ Date: June 2003
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 
+#include <util/irep.h>
+
 class goto_functionst;
 class goto_programt;
 class goto_modelt;
@@ -40,7 +42,8 @@ bool remove_function_pointers(
   symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
   goto_programt &goto_program,
+  const irep_idt &function_id,
   bool add_safety_assertion,
-  bool only_remove_const_fps=false);
+  bool only_remove_const_fps = false);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp
index fa62a53c6d9..b43348870fe 100644
--- a/src/goto-programs/set_properties.cpp
+++ b/src/goto-programs/set_properties.cpp
@@ -47,6 +47,7 @@ void label_properties(goto_modelt &goto_model)
 
 void label_properties(
   goto_programt &goto_program,
+  const irep_idt &function_id,
   std::map<irep_idt, std::size_t> &property_counters)
 {
   for(goto_programt::instructionst::iterator
@@ -57,9 +58,7 @@ void label_properties(
     if(!it->is_assert())
       continue;
 
-    irep_idt function=it->source_location.get_function();
-
-    std::string prefix=id2string(function);
+    std::string prefix = id2string(function_id);
     if(it->source_location.get_property_class()!="")
     {
       if(prefix!="")
@@ -87,10 +86,10 @@ void label_properties(
   }
 }
 
-void label_properties(goto_programt &goto_program)
+void label_properties(goto_programt &goto_program, const irep_idt &function_id)
 {
   std::map<irep_idt, std::size_t> property_counters;
-  label_properties(goto_program, property_counters);
+  label_properties(goto_program, function_id, property_counters);
 }
 
 void set_properties(
@@ -126,7 +125,7 @@ void label_properties(goto_functionst &goto_functions)
       it=goto_functions.function_map.begin();
       it!=goto_functions.function_map.end();
       it++)
-    label_properties(it->second.body, property_counters);
+    label_properties(it->second.body, it->first, property_counters);
 }
 
 void make_assertions_false(goto_modelt &goto_model)
diff --git a/src/goto-programs/set_properties.h b/src/goto-programs/set_properties.h
index 53d1bee93d7..fbf6c711ce1 100644
--- a/src/goto-programs/set_properties.h
+++ b/src/goto-programs/set_properties.h
@@ -26,7 +26,7 @@ void make_assertions_false(goto_functionst &);
 void make_assertions_false(goto_modelt &);
 
 void label_properties(goto_functionst &);
-void label_properties(goto_programt &);
+void label_properties(goto_programt &, const irep_idt &);
 void label_properties(goto_modelt &);
 
 #endif // CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
index f5f4da55af2..9ec4e5db51e 100644
--- a/src/goto-programs/show_properties.cpp
+++ b/src/goto-programs/show_properties.cpp
@@ -21,10 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_functions.h"
 #include "goto_model.h"
 
-
-optionalt<source_locationt> find_property(
-    const irep_idt &property,
-    const goto_functionst & goto_functions)
+optionalt<std::pair<irep_idt, source_locationt>>
+find_property(const irep_idt &property, const goto_functionst &goto_functions)
 {
   for(const auto &fct : goto_functions.function_map)
   {
@@ -36,7 +34,7 @@ optionalt<source_locationt> find_property(
       {
         if(ins.source_location.get_property_id() == property)
         {
-          return ins.source_location;
+          return std::make_pair(fct.first, ins.source_location);
         }
       }
     }
diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h
index ea8cc46e4a7..13613574bb3 100644
--- a/src/goto-programs/show_properties.h
+++ b/src/goto-programs/show_properties.h
@@ -46,11 +46,10 @@ void show_properties(
 /// \param property: irep_idt that identifies property
 /// \param goto_functions: program in which to search for
 ///   the property
-/// \return optional<source_locationt> the location of the
+/// \return A pair of function identifier and source location of the
 ///   property, if found.
-optionalt<source_locationt> find_property(
-    const irep_idt &property,
-    const goto_functionst &goto_functions);
+optionalt<std::pair<irep_idt, source_locationt>>
+find_property(const irep_idt &property, const goto_functionst &goto_functions);
 
 /// \brief Collects the properties in the goto program into a `json_arrayt`
 /// \param json_properties: JSON array to hold the properties
diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp
index 509904cd3ea..fceed1bbbd1 100644
--- a/src/goto-programs/show_symbol_table.cpp
+++ b/src/goto-programs/show_symbol_table.cpp
@@ -223,7 +223,8 @@ static void show_symbol_table_json_ui(
       {"isVolatile", jsont::json_boolean(symbol.is_volatile)},
       {"isParameter", jsont::json_boolean(symbol.is_parameter)},
       {"isAuxiliary", jsont::json_boolean(symbol.is_auxiliary)},
-      {"isWeak", jsont::json_boolean(symbol.is_weak)}};
+      {"isWeak", jsont::json_boolean(symbol.is_weak)},
+      {"hasLocalScope", jsont::json_boolean(symbol.has_local_scope)}};
 
     result.push_back(id2string(symbol.name), std::move(symbol_json));
   }
diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp
index 4a5fa525410..83cda7eedd7 100644
--- a/src/goto-programs/write_goto_binary.cpp
+++ b/src/goto-programs/write_goto_binary.cpp
@@ -62,7 +62,7 @@ bool write_goto_binary_v5(
     flags = (flags << 1) | static_cast<int>(sym.is_state_var);
     flags = (flags << 1) | static_cast<int>(sym.is_parameter);
     flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
-    flags = (flags << 1) | static_cast<int>(false); // sym.binding;
+    flags = (flags << 1) | static_cast<int>(sym.has_local_scope);
     flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
     flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
     flags = (flags << 1) | static_cast<int>(sym.is_thread_local);
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 5184ddf568d..49725fe6619 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -992,14 +992,13 @@ irep_idt symex_target_equationt::SSA_stept::get_property_id() const
   else if(source.pc->is_goto())
   {
     // this is likely an unwinding assertion
-    property_id = id2string(source.pc->source_location.get_function()) +
-                  ".unwind." + std::to_string(source.pc->loop_number);
+    property_id = id2string(source.function_id) + ".unwind." +
+                  std::to_string(source.pc->loop_number);
   }
   else if(source.pc->is_function_call())
   {
     // this is likely a recursion unwinding assertion
-    property_id =
-      id2string(source.pc->source_location.get_function()) + ".recursion";
+    property_id = id2string(source.function_id) + ".recursion";
   }
   else
   {
diff --git a/src/json-symtab-language/json_symbol.cpp b/src/json-symtab-language/json_symbol.cpp
index cd6b0d79bee..45006753613 100644
--- a/src/json-symtab-language/json_symbol.cpp
+++ b/src/json-symtab-language/json_symbol.cpp
@@ -107,6 +107,8 @@ symbolt symbol_from_json(const jsont &in)
       result.is_auxiliary = try_get_bool(kv.second, "isAuxiliary");
     else if(kv.first == "isWeak")
       result.is_weak = try_get_bool(kv.second, "isWeak");
+    else if(kv.first == "hasLocalScope")
+      result.has_local_scope = try_get_bool(kv.second, "hasLocalScope");
     else if(kv.first == "prettyType")
     {
     } // ignore
diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index d44fb5f674f..b7ccb9141fb 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -48,6 +48,8 @@ void symbolt::show(std::ostream &out) const
     out << " auxiliary";
   if(is_weak)
     out << " weak";
+  if(has_local_scope)
+    out << " local_scope";
   if(is_property)
     out << " property";
   if(is_state_var)
@@ -58,12 +60,10 @@ void symbolt::show(std::ostream &out) const
     out << " volatile";
   if(!mode.empty())
     out << " mode=" << mode;
-  if(!base_name.empty())
-    out << " base_name=" << base_name;
   if(!module.empty())
     out << " module=" << module;
-  if(!pretty_name.empty())
-    out << " pretty_name=" << pretty_name;
+  if(!display_name.empty())
+    out << " display_name=" << display_name;
   out << '\n';
   out << "  location: " << location << '\n';
 
@@ -90,9 +90,8 @@ void symbolt::swap(symbolt &b)
   SYM_SWAP1(type);
   SYM_SWAP1(value);
   SYM_SWAP1(name);
-  SYM_SWAP1(pretty_name);
+  SYM_SWAP1(display_name);
   SYM_SWAP1(module);
-  SYM_SWAP1(base_name);
   SYM_SWAP1(mode);
   SYM_SWAP1(location);
 
@@ -108,6 +107,7 @@ void symbolt::swap(symbolt &b)
   SYM_SWAP2(is_parameter);
   SYM_SWAP2(is_auxiliary);
   SYM_SWAP2(is_weak);
+  SYM_SWAP2(has_local_scope);
   SYM_SWAP2(is_lvalue);
   SYM_SWAP2(is_static_lifetime);
   SYM_SWAP2(is_thread_local);
@@ -139,10 +139,7 @@ bool symbolt::is_well_formed() const
   // to have it's base name as a suffix to it's more
   // general name.
 
-  // Exception: Java symbols' base names do not have type signatures
-  // (for example, they can have name "someclass.method:(II)V" and base name
-  // "method")
-  if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
+  if(!has_suffix(id2string(name), id2string(display_name)))
   {
     bool criterion_must_hold = true;
 
@@ -165,6 +162,13 @@ bool symbolt::is_well_formed() const
         criterion_must_hold = false;
       }
     }
+    // Exception: Java symbols' base names do not have type signatures
+    // (for example, they can have name "someclass.method:(II)V" and base name
+    // "method")
+    else if(mode == ID_java)
+    {
+      return id2string(name).find(id2string(display_name)) != std::string::npos;
+    }
 
     // Linker renaming may have added $linkN suffixes to the name, and other
     // suffixes such as #return_value may have then be subsequently added.
@@ -207,9 +211,8 @@ bool symbolt::operator==(const symbolt &other) const
     location == other.location &&
     name == other.name &&
     module == other.module &&
-    base_name == other.base_name &&
     mode == other.mode &&
-    pretty_name == other.pretty_name &&
+    display_name == other.display_name &&
     is_type == other.is_type &&
     is_macro == other.is_macro &&
     is_exported == other.is_exported &&
@@ -220,6 +223,7 @@ bool symbolt::operator==(const symbolt &other) const
     is_parameter == other.is_parameter &&
     is_auxiliary == other.is_auxiliary &&
     is_weak == other.is_weak &&
+    has_local_scope == other.has_local_scope &&
     is_lvalue == other.is_lvalue &&
     is_static_lifetime == other.is_static_lifetime &&
     is_thread_local == other.is_thread_local &&
diff --git a/src/util/symbol.h b/src/util/symbol.h
index d34c8351c43..3f1853f868f 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -42,20 +42,11 @@ class symbolt
   /// Name of module the symbol belongs to
   irep_idt module;
 
-  /// Base (non-scoped) name
-  irep_idt base_name;
-
   /// Language mode
   irep_idt mode;
 
   /// Language-specific display name
-  irep_idt pretty_name;
-
-  /// Return language specific display name if present.
-  const irep_idt &display_name() const
-  {
-    return pretty_name.empty()?name:pretty_name;
-  }
+  irep_idt display_name;
 
   // global use
   bool is_type, is_macro, is_exported,
@@ -63,8 +54,8 @@ class symbolt
 
   // ANSI-C
   bool is_static_lifetime, is_thread_local;
-  bool is_lvalue, is_file_local, is_extern, is_volatile,
-       is_parameter, is_auxiliary, is_weak;
+  bool is_lvalue, is_file_local, is_extern, is_volatile, is_parameter,
+    is_auxiliary, is_weak, has_local_scope;
 
   symbolt()
   {
@@ -78,13 +69,12 @@ class symbolt
     value.make_nil();
     location.make_nil();
 
-    name=module=base_name=mode=pretty_name=irep_idt();
+    name=module=mode=display_name=irep_idt();
 
-    is_type=is_macro=is_exported=
-    is_input=is_output=is_state_var=is_property=
-    is_static_lifetime=is_thread_local=
-    is_lvalue=is_file_local=is_extern=is_volatile=
-    is_parameter=is_auxiliary=is_weak=false;
+    is_type = is_macro = is_exported = is_input = is_output = is_state_var =
+      is_property = is_static_lifetime = is_thread_local = is_lvalue =
+        is_file_local = is_extern = is_volatile = is_parameter = is_auxiliary =
+          is_weak = has_local_scope = false;
   }
 
   void swap(symbolt &b);
@@ -153,13 +143,14 @@ class auxiliary_symbolt:public symbolt
     is_thread_local=true;
     is_file_local=true;
     is_auxiliary=true;
+    has_local_scope = true;
   }
 
   auxiliary_symbolt(const irep_idt &name, const typet &type):
     auxiliary_symbolt()
   {
     this->name=name;
-    this->base_name=name;
+    this->display_name = name;
     this->type=type;
   }
 };
@@ -177,6 +168,7 @@ class parameter_symbolt:public symbolt
     is_thread_local=true;
     is_file_local=true;
     is_parameter=true;
+    has_local_scope = true;
   }
 };