diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
index 2ec32e7ce98..b93fb7882ce 100644
--- a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
+++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.withDependency  --max-nondet-string-length 10000
+--function Test.withDependency  --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .*: SUCCESS
diff --git a/jbmc/regression/jbmc/throwing-function-return-value/test.desc b/jbmc/regression/jbmc/throwing-function-return-value/test.desc
index 4246e18eff2..4bebe0b1194 100644
--- a/jbmc/regression/jbmc/throwing-function-return-value/test.desc
+++ b/jbmc/regression/jbmc/throwing-function-return-value/test.desc
@@ -3,11 +3,13 @@ Test.class
 --function Test.main --show-vcc
 java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
 java::Test\.main:\(Z\)V::9::x!0@1#\d+ = 5 \+ java::Test\.main:\(Z\)V::9::x!0@1#\d+
+java::Test\.g:\(\)I#return_value!0#[0-9]+ = 5
 ^EXIT=0$
 ^SIGNAL=0$
 --
 return_value!0#0
 java::Sub\.g:\(\)
+java::Test\.g:\(\)I#return_value!0#[0-9]+ = [^5]
 --
 This checks that when a function may throw, we can nonetheless constant-propagate
 and populate the value-set for the normal-return path. In particular we don't
@@ -16,3 +18,6 @@ reading the return-value when not defined), nor do we expect to see any code
 from the Sub class, which is not accessible and can only be reached when
 constant propagation has lost information to the point we're not sure which type
 virtual calls against Test may find.
+The final check ensures there is no uncertainty about whether Test.g() may throw,
+which would result in a nondet return-value (corresponding to the hypothetical
+throwing path).
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 772256dd633..09f0d87f9a1 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -459,19 +459,6 @@ bool goto_symex_statet::l2_thread_read_encoding(
   return true;
 }
 
-/// Allocates a fresh L2 name for the given L1 identifier, and makes it the
-/// latest generation on this path. Does nothing if there isn't an expression
-/// keyed by the l1 identifier.
-void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier)
-{
-  // If we can't find the name in the local scope, this is a no-op.
-  auto current_names_iter = level2.current_names.find(identifier);
-  if(current_names_iter == level2.current_names.end())
-    return;
-
-  current_names_iter->second.second = fresh_l2_name_provider(identifier);
-}
-
 goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   const ssa_exprt &expr,
   const namespacet &ns) const
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 9fb65bf5bcb..ab0ec52a1a4 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -223,16 +223,18 @@ class goto_symex_statet final : public goto_statet
       l1_identifier, lhs, fresh_l2_name_provider);
   }
 
-  /// Increases the generation of the L1 identifier. Does nothing if there
-  /// isn't an expression keyed by it.
-  void increase_generation_if_exists(const irep_idt identifier);
-
   /// Drops an L1 name from the local L2 map
   void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it)
   {
     level2.current_names.erase(it);
   }
 
+  /// Drops an L1 name from the local L2 map
+  void drop_l1_name(const irep_idt &l1_identifier)
+  {
+    level2.current_names.erase(l1_identifier);
+  }
+
   std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
   {
     return fresh_l2_name_provider;
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index 898dd280277..f06b3b0167b 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -30,7 +30,10 @@ void goto_symext::symex_dead(statet &state)
   // can no longer appear
   state.value_set.values.erase(l1_identifier);
   state.propagation.erase(l1_identifier);
-  // increment the L2 index to ensure a merge on join points will propagate the
-  // value for branches that are still live
-  state.increase_generation_if_exists(l1_identifier);
+  // Remove from the local L2 renaming map; this means any reads from the dead
+  // identifier will use generation 0 (e.g. x!N@M#0, where N and M are positive
+  // integers), which is never defined by any write, and will be dropped by
+  // `goto_symext::merge_goto` on merging with branches where the identifier
+  // is still live.
+  state.drop_l1_name(l1_identifier);
 }