diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp
index 3a6092092ab..5269e7004b3 100644
--- a/jbmc/src/java_bytecode/nondet.cpp
+++ b/jbmc/src/java_bytecode/nondet.cpp
@@ -123,7 +123,9 @@ code_blockt generate_nondet_switch(
     this_block.add(switch_case);
     this_block.add(code_breakt());
     code_switch_caset this_case(
-      from_integer(case_number, switch_value.type()), this_block);
+      from_integer(case_number, switch_value.type())
+        .with_source_location(source_location),
+      this_block);
     switch_block.add(std::move(this_case));
     ++case_number;
   }
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index 1483ee0ea44..f243fd2087c 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -77,6 +77,7 @@ add_subdirectory(k-induction)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
+add_subdirectory(goto-cc-multi-file)
 add_subdirectory(goto-cc-regression-gh-issue-5380)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
diff --git a/regression/Makefile b/regression/Makefile
index 7a8732ac264..c29abf01af7 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -50,6 +50,7 @@ DIRS = cbmc-shadow-memory \
        goto-harness \
        goto-harness-multi-file-project \
        goto-cc-file-local \
+       goto-cc-multi-file \
        goto-cc-regression-gh-issue-5380 \
        linking-goto-binaries \
        symtab2gb \
diff --git a/regression/cbmc-cover/location3/main.c b/regression/cbmc-cover/location3/main.c
new file mode 100644
index 00000000000..d09b61f219e
--- /dev/null
+++ b/regression/cbmc-cover/location3/main.c
@@ -0,0 +1,22 @@
+int main()
+{
+  int b, c;
+
+  if(b)
+  {
+    if(c)
+    {
+      c = 1;
+    }
+    else
+    {
+      c = 2;
+    }
+  }
+  else
+  {
+    b = 0;
+  }
+
+  return 1;
+}
diff --git a/regression/cbmc-cover/location3/test.desc b/regression/cbmc-cover/location3/test.desc
new file mode 100644
index 00000000000..48e1a80f280
--- /dev/null
+++ b/regression/cbmc-cover/location3/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.\d+\] file main.c line 9 function main block \d+ \(lines main.c:main:9,10\): SATISFIED$
+^\[main.coverage.\d+\] file main.c line 15 function main block \d+ \(lines main.c:main:15\): SATISFIED$
+^\*\* 7 of 7 covered \(100.0%\)
+--
+^warning: ignoring
+--
+All gotos must have a source location annotated.
diff --git a/regression/goto-cc-multi-file/CMakeLists.txt b/regression/goto-cc-multi-file/CMakeLists.txt
new file mode 100644
index 00000000000..53647ddb692
--- /dev/null
+++ b/regression/goto-cc-multi-file/CMakeLists.txt
@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)
diff --git a/regression/goto-cc-multi-file/maintain-location/main.c b/regression/goto-cc-multi-file/maintain-location/main.c
new file mode 100644
index 00000000000..a55afb81e20
--- /dev/null
+++ b/regression/goto-cc-multi-file/maintain-location/main.c
@@ -0,0 +1,11 @@
+int foo()
+{
+  return 0;
+}
+
+int main()
+{
+  int result;
+  result = foo();
+  return result;
+}
diff --git a/regression/goto-cc-multi-file/maintain-location/other.c b/regression/goto-cc-multi-file/maintain-location/other.c
new file mode 100644
index 00000000000..6a794a79c27
--- /dev/null
+++ b/regression/goto-cc-multi-file/maintain-location/other.c
@@ -0,0 +1,6 @@
+int foo();
+
+int bar()
+{
+  return foo();
+}
diff --git a/regression/goto-cc-multi-file/maintain-location/test.desc b/regression/goto-cc-multi-file/maintain-location/test.desc
new file mode 100644
index 00000000000..4cdabb403ff
--- /dev/null
+++ b/regression/goto-cc-multi-file/maintain-location/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+other.c
+file main.c line 9 function main
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+We previously lost the location attached to the call of `foo` in function main.
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index ab278de784f..f4535763987 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -1044,15 +1044,16 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     new_expr = size_of_opt.value();
   }
 
+  source_locationt location = expr.source_location();
   new_expr.swap(expr);
-
+  expr.add_source_location() = location;
   expr.add(ID_C_c_sizeof_type)=type;
 
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
     side_effect_exprt side_effect_expr(
-      ID_statement_expression, void_type(), expr.source_location());
+      ID_statement_expression, void_type(), location);
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -1064,8 +1065,9 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     // It is not obvious whether the type or 'e' should be evaluated
     // first.
 
-    binary_exprt comma_expr{
-      std::move(side_effect_expr), ID_comma, expr, expr.type()};
+    exprt comma_expr =
+      binary_exprt{std::move(side_effect_expr), ID_comma, expr, expr.type()}
+        .with_source_location(location);
     expr.swap(comma_expr);
   }
 }
@@ -4656,6 +4658,8 @@ class is_compile_time_constantt
 
 void c_typecheck_baset::make_constant(exprt &expr)
 {
+  source_locationt location = expr.find_source_location();
+
   // Floating-point expressions may require a rounding mode.
   // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
   // Some compilers have command-line options to override.
@@ -4664,10 +4668,11 @@ void c_typecheck_baset::make_constant(exprt &expr)
   adjust_float_expressions(expr, rounding_mode);
 
   simplify(expr, *this);
+  expr.add_source_location() = location;
 
   if(!is_compile_time_constantt(*this)(expr))
   {
-    error().source_location=expr.find_source_location();
+    error().source_location = location;
     error() << "expected constant expression, but got '" << to_string(expr)
             << "'" << eom;
     throw 0;
@@ -4676,13 +4681,15 @@ void c_typecheck_baset::make_constant(exprt &expr)
 
 void c_typecheck_baset::make_constant_index(exprt &expr)
 {
+  source_locationt location = expr.find_source_location();
   make_constant(expr);
   make_index_type(expr);
   simplify(expr, *this);
+  expr.add_source_location() = location;
 
   if(!is_compile_time_constantt(*this)(expr))
   {
-    error().source_location=expr.find_source_location();
+    error().source_location = location;
     error() << "conversion to integer constant failed" << eom;
     throw 0;
   }
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
index 162daad11d8..5632868d13a 100644
--- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
+++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -673,7 +673,8 @@ static void instantiate_atomic_fetch_op(
   block.add(code_frontend_assignt{deref_ptr, std::move(op_expr)});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -736,7 +737,8 @@ static void instantiate_atomic_op_fetch(
 
   // this instruction implies an mfence, i.e., WRfence
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -767,11 +769,11 @@ static void instantiate_sync_fetch(
     parameter_exprs[1],
     from_integer(std::memory_order_seq_cst, signed_int_type())};
 
-  block.add(code_returnt{
-    side_effect_expr_function_callt{symbol_exprt::typeless(atomic_name),
-                                    std::move(arguments),
-                                    typet{},
-                                    source_location}});
+  block.add(code_returnt{side_effect_expr_function_callt{
+    symbol_exprt::typeless(atomic_name).with_source_location(source_location),
+    std::move(arguments),
+    typet{},
+    source_location}});
 }
 
 static void instantiate_sync_bool_compare_and_swap(
@@ -790,7 +792,8 @@ static void instantiate_sync_bool_compare_and_swap(
   // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
 
   block.add(code_returnt{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_compare_exchange),
+    symbol_exprt::typeless(ID___atomic_compare_exchange)
+      .with_source_location(source_location),
     {parameter_exprs[0],
      address_of_exprt{parameter_exprs[1]},
      address_of_exprt{parameter_exprs[2]},
@@ -968,7 +971,8 @@ static void instantiate_atomic_load(
                                   dereference_exprt{parameter_exprs[0]}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -999,7 +1003,8 @@ static void instantiate_atomic_load_n(
   block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_load),
+    symbol_exprt::typeless(ID___atomic_load)
+      .with_source_location(source_location),
     {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
     typet{},
     source_location}});
@@ -1028,7 +1033,8 @@ static void instantiate_atomic_store(
                                   dereference_exprt{parameter_exprs[1]}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[2]},
     typet{},
     source_location}});
@@ -1051,13 +1057,14 @@ static void instantiate_atomic_store_n(
   // This built-in function implements an atomic store operation. It writes
   // val into *ptr.
 
-  block.add(code_expressiont{
-    side_effect_expr_function_callt{symbol_exprt::typeless(ID___atomic_store),
-                                    {parameter_exprs[0],
-                                     address_of_exprt{parameter_exprs[1]},
-                                     parameter_exprs[2]},
-                                    typet{},
-                                    source_location}});
+  block.add(code_expressiont{side_effect_expr_function_callt{
+    symbol_exprt::typeless(ID___atomic_store)
+      .with_source_location(source_location),
+    {parameter_exprs[0],
+     address_of_exprt{parameter_exprs[1]},
+     parameter_exprs[2]},
+    typet{},
+    source_location}});
 }
 
 static void instantiate_atomic_exchange(
@@ -1083,7 +1090,8 @@ static void instantiate_atomic_exchange(
                                   dereference_exprt{parameter_exprs[1]}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[3]},
     typet{},
     source_location}});
@@ -1114,7 +1122,8 @@ static void instantiate_atomic_exchange_n(
   block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_exchange),
+    symbol_exprt::typeless(ID___atomic_exchange)
+      .with_source_location(source_location),
     {parameter_exprs[0],
      address_of_exprt{parameter_exprs[1]},
      address_of_exprt{result},
@@ -1171,7 +1180,8 @@ static void instantiate_atomic_compare_exchange(
                                dereference_exprt{parameter_exprs[2]}};
   assign.add_source_location() = source_location;
   code_expressiont success_fence{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[4]},
     typet{},
     source_location}};
@@ -1181,7 +1191,8 @@ static void instantiate_atomic_compare_exchange(
                                          deref_ptr};
   assign_not_equal.add_source_location() = source_location;
   code_expressiont failure_fence{side_effect_expr_function_callt{
-    symbol_exprt::typeless("__atomic_thread_fence"),
+    symbol_exprt::typeless("__atomic_thread_fence")
+      .with_source_location(source_location),
     {parameter_exprs[5]},
     typet{},
     source_location}};
@@ -1212,7 +1223,8 @@ static void instantiate_atomic_compare_exchange_n(
   // desired, bool weak, int success_memorder, int failure_memorder)
 
   block.add(code_returnt{side_effect_expr_function_callt{
-    symbol_exprt::typeless(ID___atomic_compare_exchange),
+    symbol_exprt::typeless(ID___atomic_compare_exchange)
+      .with_source_location(source_location),
     {parameter_exprs[0],
      parameter_exprs[1],
      address_of_exprt{parameter_exprs[2]},
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
index e46b4b2ed15..43426ace345 100644
--- a/src/assembler/remove_asm.cpp
+++ b/src/assembler/remove_asm.cpp
@@ -133,7 +133,8 @@ void remove_asmt::gcc_asm_function_call(
       arguments.size(), code_typet::parametert{void_pointer}},
     empty_typet()};
 
-  symbol_exprt fkt(function_identifier, fkt_type);
+  auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location(
+    code.source_location());
 
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
@@ -189,8 +190,8 @@ void remove_asmt::msc_asm_function_call(
       arguments.size(), code_typet::parametert{void_pointer}},
     empty_typet()};
 
-  symbol_exprt fkt(function_identifier, fkt_type);
-
+  auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location(
+    code.source_location());
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
   dest.add(
diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp
index 35dce3e458a..2c9e1f32f4f 100644
--- a/src/goto-programs/goto_clean_expr.cpp
+++ b/src/goto-programs/goto_clean_expr.cpp
@@ -284,7 +284,14 @@ void goto_convertt::clean_expr(
 
     // generate guard for argument side-effects
     generate_ifthenelse(
-      if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
+      if_expr.cond(),
+      source_location,
+      tmp_true,
+      if_expr.true_case().source_location(),
+      tmp_false,
+      if_expr.false_case().source_location(),
+      dest,
+      mode);
 
     return;
   }
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index b4e1a931982..f7725df3136 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -526,6 +526,13 @@ void goto_convertt::convert_switch_case(
 
     exprt::operandst &case_op_dest=cases_entry->second->second;
     case_op_dest.push_back(code.case_op());
+    // make sure we have a source location in the case operand as otherwise we
+    // end up with a GOTO instruction without a source location
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      case_op_dest.back().source_location().is_not_nil(),
+      "case operand should have a source location",
+      case_op_dest.back().pretty(),
+      code.pretty());
   }
 }
 
@@ -1613,17 +1620,34 @@ void goto_convertt::convert_ifthenelse(
   // convert 'then'-branch
   goto_programt tmp_then;
   convert(code.then_case(), tmp_then, mode);
+  source_locationt then_end_location =
+    code.then_case().get_statement() == ID_block
+      ? to_code_block(code.then_case()).end_location()
+      : code.then_case().source_location();
 
   goto_programt tmp_else;
+  source_locationt else_end_location;
 
   if(has_else)
+  {
     convert(code.else_case(), tmp_else, mode);
+    else_end_location = code.else_case().get_statement() == ID_block
+                          ? to_code_block(code.else_case()).end_location()
+                          : code.else_case().source_location();
+  }
 
   exprt tmp_guard=code.cond();
   clean_expr(tmp_guard, dest, mode);
 
   generate_ifthenelse(
-    tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
+    tmp_guard,
+    source_location,
+    tmp_then,
+    then_end_location,
+    tmp_else,
+    else_end_location,
+    dest,
+    mode);
 }
 
 void goto_convertt::collect_operands(
@@ -1655,9 +1679,11 @@ static inline bool is_size_one(const goto_programt &g)
 /// if(guard) true_case; else false_case;
 void goto_convertt::generate_ifthenelse(
   const exprt &guard,
+  const source_locationt &source_location,
   goto_programt &true_case,
+  const source_locationt &then_end_location,
   goto_programt &false_case,
-  const source_locationt &source_location,
+  const source_locationt &else_end_location,
   goto_programt &dest,
   const irep_idt &mode)
 {
@@ -1727,13 +1753,17 @@ void goto_convertt::generate_ifthenelse(
 
   // Flip around if no 'true' case code.
   if(is_empty(true_case))
+  {
     return generate_ifthenelse(
       boolean_negate(guard),
+      source_location,
       false_case,
+      else_end_location,
       true_case,
-      source_location,
+      then_end_location,
       dest,
       mode);
+  }
 
   bool has_else=!is_empty(false_case);
 
@@ -1753,14 +1783,13 @@ void goto_convertt::generate_ifthenelse(
 
   // do the x label
   goto_programt tmp_x;
-  goto_programt::targett x = tmp_x.add(goto_programt::make_incomplete_goto(
-    true_exprt(), true_case.instructions.back().source_location()));
+  goto_programt::targett x = tmp_x.add(
+    goto_programt::make_incomplete_goto(true_exprt(), then_end_location));
 
   // do the z label
   goto_programt tmp_z;
-  goto_programt::targett z = tmp_z.add(goto_programt::make_skip());
-  // We deliberately don't set a location for 'z', it's a dummy
-  // target.
+  goto_programt::targett z = tmp_z.add(
+    goto_programt::make_skip(has_else ? else_end_location : then_end_location));
 
   // y: Q;
   goto_programt tmp_y;
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 661260dd1d8..ee10e914326 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -576,7 +576,9 @@ class goto_convertt:public messaget
   // if(cond) { true_case } else { false_case }
   void generate_ifthenelse(
     const exprt &cond,
+    const source_locationt &,
     goto_programt &true_case,
+    const source_locationt &,
     goto_programt &false_case,
     const source_locationt &,
     goto_programt &dest,
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index f8bc52605ec..7db4f3456b7 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -205,6 +205,7 @@ static void fix_argument_types(code_function_callt &function_call)
 static void fix_return_type(
   const irep_idt &in_function_id,
   code_function_callt &function_call,
+  const source_locationt &source_location,
   symbol_tablet &symbol_table,
   goto_programt &dest)
 {
@@ -226,7 +227,7 @@ static void fix_return_type(
     code_type.return_type(),
     id2string(in_function_id),
     "tmp_return_val_" + id2string(function_symbol.base_name),
-    function_call.source_location(),
+    source_location,
     function_symbol.mode,
     symbol_table);
 
@@ -239,7 +240,7 @@ static void fix_return_type(
     old_lhs,
     make_byte_extract(
       tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()),
-    function_call.source_location())));
+    source_location)));
 }
 
 void remove_function_pointerst::remove_function_pointer(
@@ -407,7 +408,8 @@ void remove_function_pointer(
     fix_argument_types(new_call);
 
     goto_programt tmp;
-    fix_return_type(function_id, new_call, symbol_table, tmp);
+    fix_return_type(
+      function_id, new_call, target->source_location(), symbol_table, tmp);
 
     auto call = new_code_calls.add(
       goto_programt::make_function_call(new_call, target->source_location()));
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 5ed4d1dfb03..b4ba95fab2f 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -100,6 +100,11 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 
   const exprt &e = it->second;
 
+  source_locationt previous_source_location{s.source_location()};
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    previous_source_location.is_not_nil(),
+    "front-ends should construct symbol expressions with source locations",
+    s.pretty());
   if(e.type().id() != ID_array && e.type().id() != ID_code)
   {
     typet type = s.type();
@@ -107,6 +112,7 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
   }
   else
     static_cast<exprt &>(s) = e;
+  s.add_source_location() = std::move(previous_source_location);
 
   return false;
 }
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index f36cc67b453..0ae667630a4 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -236,7 +236,7 @@ exprt value_set_dereferencet::handle_dereference_base_case(
       pointer.type(),
       "derefd_pointer",
       "derefd_pointer",
-      source_locationt(),
+      pointer.find_source_location(),
       language_mode,
       new_symbol_table);
 
diff --git a/src/util/expr.h b/src/util/expr.h
index 56e8611a7d3..08e1d57a7e0 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -97,6 +97,22 @@ class exprt:public irept
   const operandst &operands() const
   { return (const operandst &)get_sub(); }
 
+  /// Add the source location from \p location, if it is non-nil.
+  exprt &with_source_location(source_locationt location) &
+  {
+    if(location.is_not_nil())
+      add_source_location() = std::move(location);
+    return *this;
+  }
+
+  /// Add the source location from \p location, if it is non-nil.
+  exprt &&with_source_location(source_locationt location) &&
+  {
+    if(location.is_not_nil())
+      add_source_location() = std::move(location);
+    return std::move(*this);
+  }
+
   /// Add the source location from \p other, if it has any.
   exprt &with_source_location(const exprt &other) &
   {
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index ce30b84b239..7487f69c3bb 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -51,7 +51,12 @@ bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
     s.type() == it->second.type(),
     "types to be replaced should match. s.type:\n" + s.type().pretty() +
       "\nit->second.type:\n" + it->second.type().pretty());
+  source_locationt previous_source_location{s.source_location()};
   static_cast<exprt &>(s) = it->second;
+  // back-end generated or internal symbols (like rounding mode) might not have
+  // a source location
+  if(s.source_location().is_nil() && previous_source_location.is_not_nil())
+    s.add_source_location() = std::move(previous_source_location);
 
   return false;
 }
@@ -334,7 +339,12 @@ bool unchecked_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
   if(it == expr_map.end())
     return true;
 
+  source_locationt previous_source_location{s.source_location()};
   static_cast<exprt &>(s) = it->second;
+  // back-end generated or internal symbols (like rounding mode) might not have
+  // a source location
+  if(s.source_location().is_nil() && previous_source_location.is_not_nil())
+    s.add_source_location() = std::move(previous_source_location);
 
   return false;
 }
@@ -415,7 +425,12 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr(
 
   // Note s_copy is no longer a symbol_exprt due to the replace operation,
   // and after this line `s` won't be either
+  source_locationt previous_source_location{s.source_location()};
   s = s_copy;
+  // back-end generated or internal symbols (like rounding mode) might not have
+  // a source location
+  if(s.source_location().is_nil() && previous_source_location.is_not_nil())
+    s.add_source_location() = std::move(previous_source_location);
 
   return false;
 }
diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp
index 5df2031434e..e92c79967e6 100644
--- a/src/util/ssa_expr.cpp
+++ b/src/util/ssa_expr.cpp
@@ -41,6 +41,7 @@ ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
 {
   set(ID_C_SSA_symbol, true);
   add(ID_expression, expr);
+  with_source_location(expr.source_location());
   std::ostringstream os;
   initialize_ssa_identifier(os, expr);
   const std::string id = os.str();
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 90b2877f1f4..431de0bfa00 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -161,6 +161,38 @@ class symbol_exprt : public nullary_exprt
   {
     return get(ID_identifier);
   }
+
+  /// Add the source location from \p location, if it is non-nil.
+  symbol_exprt &with_source_location(source_locationt location) &
+  {
+    if(location.is_not_nil())
+      add_source_location() = std::move(location);
+    return *this;
+  }
+
+  /// Add the source location from \p location, if it is non-nil.
+  symbol_exprt &&with_source_location(source_locationt location) &&
+  {
+    if(location.is_not_nil())
+      add_source_location() = std::move(location);
+    return std::move(*this);
+  }
+
+  /// Add the source location from \p other, if it has any.
+  symbol_exprt &with_source_location(const exprt &other) &
+  {
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return *this;
+  }
+
+  /// Add the source location from \p other, if it has any.
+  symbol_exprt &&with_source_location(const exprt &other) &&
+  {
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return std::move(*this);
+  }
 };
 
 // NOLINTNEXTLINE(readability/namespace)
diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index 12f60c5f01a..5335125c9c5 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -120,7 +120,7 @@ void symbolt::swap(symbolt &b)
 ///   type of the symbol object.
 symbol_exprt symbolt::symbol_expr() const
 {
-  return symbol_exprt(name, type);
+  return symbol_exprt(name, type).with_source_location(location);
 }
 
 /// Check that the instance object is well formed.
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index 3bdc97c2fd2..4b9ff978e99 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -337,8 +337,13 @@ void symex_eventt::validate_resume(
   REQUIRE(!events.empty());
 
   int dst = 0;
-  if(!state.saved_target->source_location().get_line().empty())
+  if(
+    state.saved_target->source_location().get_file() !=
+      "<built-in-additions>" &&
+    !state.saved_target->source_location().get_line().empty())
+  {
     dst = std::stoi(state.saved_target->source_location().get_line().c_str());
+  }
 
   if(state.has_saved_next_instruction)
   {