diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index de101357478..e9366ada31e 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -37,7 +37,11 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 
   symex_state = util_make_unique<goto_symex_statet>(
     symex_targett::sourcet(goto_functionst::entry_point(), *this),
-    guard_manager);
+    guard_manager,
+    [this](const irep_idt &id) {
+      return path_storage.get_unique_l2_index(id);
+    });
+
   symex.symex_with_state(
     *symex_state,
     [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index d0f7e300727..376f8e3feda 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -91,8 +91,9 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       if(has_prefix(id2string(symbol.base_name), "auto_object"))
       {
         // done already?
-        if(state.level2.current_names.find(ssa_expr.get_identifier())==
-           state.level2.current_names.end())
+        if(
+          state.get_level2().current_names.find(ssa_expr.get_identifier()) ==
+          state.get_level2().current_names.end())
         {
           initialize_auto_object(expr, state);
         }
diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h
index 452e2df446a..23ae0b9c14a 100644
--- a/src/goto-symex/goto_state.h
+++ b/src/goto-symex/goto_state.h
@@ -28,8 +28,15 @@ class goto_statet
   /// Distance from entry
   unsigned depth = 0;
 
+protected:
   symex_level2t level2;
 
+public:
+  const symex_level2t &get_level2() const
+  {
+    return level2;
+  }
+
   /// Uses level 1 names, and is used to do dereferencing
   value_sett value_set;
 
@@ -55,6 +62,12 @@ class goto_statet
   unsigned atomic_section_id = 0;
 
   /// Constructors
+  goto_statet() = default;
+  goto_statet &operator=(const goto_statet &other) = default;
+  goto_statet &operator=(goto_statet &&other) = default;
+  goto_statet(const goto_statet &other) = default;
+  goto_statet(goto_statet &&other) = default;
+
   explicit goto_statet(const class goto_symex_statet &s);
 
   explicit goto_statet(guard_managert &guard_manager)
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index a0a42884a46..97d898a60df 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -31,13 +31,15 @@ static void get_l1_name(exprt &expr);
 
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
-  guard_managert &manager)
+  guard_managert &manager,
+  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(manager),
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
     record_events(true),
-    dirty()
+    dirty(),
+    fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
   call_stack().new_frame(source);
@@ -213,9 +215,7 @@ void goto_symex_statet::assignment(
 #endif
 
   // do the l2 renaming
-  const auto level2_it =
-    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
-  symex_renaming_levelt::increase_counter(level2_it);
+  increase_generation(l1_identifier, lhs);
   lhs = set_indices<L2>(std::move(lhs), ns).get();
 
   // in case we happen to be multi-threaded, record the memory access
@@ -440,10 +440,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     if(a_s_read.second.empty())
     {
-      auto level2_it =
-        level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
-          .first;
-      symex_renaming_levelt::increase_counter(level2_it);
+      increase_generation(l1_identifier, ssa_l1);
       a_s_read.first=level2.current_count(l1_identifier);
     }
     const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
@@ -477,10 +474,6 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return true;
   }
 
-  const auto level2_it =
-    level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
-      .first;
-
   // No event and no fresh index, but avoid constant propagation
   if(!record_events)
   {
@@ -489,7 +482,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // produce a fresh L2 name
-  symex_renaming_levelt::increase_counter(level2_it);
+  increase_generation(l1_identifier, ssa_l1);
   expr = set_indices<L2>(std::move(ssa_l1), ns).get();
 
   // and record that
@@ -500,6 +493,35 @@ 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.
+/// \return the newly allocated generation number
+std::size_t goto_symex_statet::increase_generation(
+  const irep_idt l1_identifier,
+  const ssa_exprt &lhs)
+{
+  auto current_emplace_res =
+    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+
+  current_emplace_res.first->second.second =
+    fresh_l2_name_provider(l1_identifier);
+
+  return current_emplace_res.first->second.second;
+}
+
+/// 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);
+}
+
 /// thread encoding
 bool goto_symex_statet::l2_thread_write_encoding(
   const ssa_exprt &expr,
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 778b1743ddf..db38fbc74e3 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -42,7 +42,10 @@ Author: Daniel Kroening, kroening@kroening.com
 class goto_symex_statet final : public goto_statet
 {
 public:
-  goto_symex_statet(const symex_targett::sourcet &, guard_managert &manager);
+  goto_symex_statet(
+    const symex_targett::sourcet &,
+    guard_managert &manager,
+    std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
 
   /// \brief Fake "copy constructor" that initializes the `symex_target` member
@@ -202,7 +205,24 @@ class goto_symex_statet final : public goto_statet
   unsigned total_vccs = 0;
   unsigned remaining_vccs = 0;
 
+  /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
+  //  latest generation on this path.
+  std::size_t
+  increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs);
+
+  /// 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);
+  }
+
 private:
+  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
+
   /// \brief Dangerous, do not use
   ///
   /// Copying a state S1 to S2 risks S2 pointing to a deallocated
diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h
index 3753263d8ea..4a9410a8e79 100644
--- a/src/goto-symex/path_storage.h
+++ b/src/goto-symex/path_storage.h
@@ -98,15 +98,16 @@ class path_storaget
   /// error-handling paths.
   std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 
-  /// Provide a unique index for a given \p id, starting from \p minimum_index.
-  std::size_t get_unique_index(const irep_idt &id, std::size_t minimum_index)
+  /// Provide a unique L1 index for a given \p id, starting from
+  /// \p minimum_index.
+  std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
   {
-    auto entry = unique_index_map.emplace(id, minimum_index);
-
-    if(!entry.second)
-      entry.first->second = std::max(entry.first->second + 1, minimum_index);
+    return get_unique_index(l1_indices, id, minimum_index);
+  }
 
-    return entry.first->second;
+  std::size_t get_unique_l2_index(const irep_idt &id)
+  {
+    return get_unique_index(l2_indices, id, 1);
   }
 
 private:
@@ -115,8 +116,24 @@ class path_storaget
   virtual patht &private_peek() = 0;
   virtual void private_pop() = 0;
 
+  typedef std::unordered_map<irep_idt, std::size_t> name_index_mapt;
+
+  std::size_t get_unique_index(
+    name_index_mapt &unique_index_map,
+    const irep_idt &id,
+    std::size_t minimum_index)
+  {
+    auto entry = unique_index_map.emplace(id, minimum_index);
+
+    if(!entry.second)
+      entry.first->second = std::max(entry.first->second + 1, minimum_index);
+
+    return entry.first->second;
+  }
+
   /// Storage used by \ref get_unique_index.
-  std::unordered_map<irep_idt, std::size_t> unique_index_map;
+  name_index_mapt l1_indices;
+  name_index_mapt l2_indices;
 };
 
 /// \brief LIFO save queue: depth-first search, try to finish paths
diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
index ced74b85a52..96c065483dd 100644
--- a/src/goto-symex/renaming_level.cpp
+++ b/src/goto-symex/renaming_level.cpp
@@ -73,8 +73,7 @@ operator()(renamedt<ssa_exprt, L1> l1_expr) const
   return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
 }
 
-void symex_level1t::restore_from(
-  const symex_renaming_levelt::current_namest &other)
+void symex_level1t::restore_from(const current_namest &other)
 {
   auto it = current_names.begin();
   for(const auto &pair : other)
diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h
index 268ba69a3e7..6a8e9353289 100644
--- a/src/goto-symex/renaming_level.h
+++ b/src/goto-symex/renaming_level.h
@@ -32,7 +32,13 @@ enum levelt
 /// during symex to ensure static single assignment (SSA) form.
 struct symex_renaming_levelt
 {
+  symex_renaming_levelt() = default;
   virtual ~symex_renaming_levelt() = default;
+  symex_renaming_levelt &
+  operator=(const symex_renaming_levelt &other) = default;
+  symex_renaming_levelt &operator=(symex_renaming_levelt &&other) = default;
+  symex_renaming_levelt(const symex_renaming_levelt &other) = default;
+  symex_renaming_levelt(symex_renaming_levelt &&other) = default;
 
   /// Map identifier to ssa_exprt and counter
   typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
@@ -125,6 +131,10 @@ struct symex_level2t : public symex_renaming_levelt
 
   symex_level2t() = default;
   ~symex_level2t() override = default;
+  symex_level2t &operator=(const symex_level2t &other) = default;
+  symex_level2t &operator=(symex_level2t &&other) = default;
+  symex_level2t(const symex_level2t &other) = default;
+  symex_level2t(symex_level2t &&other) = default;
 };
 
 /// Undo all levels of renaming
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index f7721c68673..f8c14dc41c0 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -70,7 +70,7 @@ void goto_symext::symex_atomic_end(statet &state)
   for(const auto &pair : state.written_in_atomic_section)
   {
     ssa_exprt w = pair.first;
-    w.set_level_2(state.level2.current_count(w.get_identifier()));
+    w.set_level_2(state.get_level2().current_count(w.get_identifier()));
 
     // guard is the disjunction over writes
     PRECONDITION(!pair.second.empty());
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index f274086ed6b..a79ecd5faac 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -45,7 +45,5 @@ void goto_symext::symex_dead(statet &state)
   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
-  auto level2_it = state.level2.current_names.find(l1_identifier);
-  if(level2_it != state.level2.current_names.end())
-    symex_renaming_levelt::increase_counter(level2_it);
+  state.increase_generation_if_exists(l1_identifier);
 }
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 31088fb9e8a..a37e45f2ec4 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -43,7 +43,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   ssa_exprt ssa = state.add_object(
     expr,
     [this](const irep_idt &l0_name) {
-      return path_storage.get_unique_index(l0_name, 1);
+      return path_storage.get_unique_l1_index(l0_name, 1);
     },
     ns);
   const irep_idt &l1_identifier = ssa.get_identifier();
@@ -66,10 +66,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   }
 
   // L2 renaming
-  bool is_new =
-    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
-      .second;
-  CHECK_RETURN(is_new);
+  std::size_t generation = state.increase_generation(l1_identifier, ssa);
+  CHECK_RETURN(generation == 1);
+
   const bool record_events=state.record_events;
   state.record_events=false;
   exprt expr_l2 = state.rename(std::move(ssa), ns);
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 67dae5958ac..ccc3be8d87e 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -349,8 +349,8 @@ static void pop_frame(goto_symext::statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    for(auto c_it = state.level2.current_names.begin();
-        c_it != state.level2.current_names.end();) // no ++c_it
+    for(auto c_it = state.get_level2().current_names.begin();
+        c_it != state.get_level2().current_names.end();) // no ++c_it
     {
       const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
       // could use iteration over local_objects as l1_o_id is prefix
@@ -364,7 +364,7 @@ static void pop_frame(goto_symext::statet &state)
       }
       auto cur = c_it;
       ++c_it;
-      state.level2.current_names.erase(cur);
+      state.drop_l1_name(cur);
     }
   }
 
@@ -402,7 +402,7 @@ static void locality(
     (void)state.add_object(
       ns.lookup(param).symbol_expr(),
       [&path_storage, &frame_nr](const irep_idt &l0_name) {
-        return path_storage.get_unique_index(l0_name, frame_nr);
+        return path_storage.get_unique_l1_index(l0_name, frame_nr);
       },
       ns);
   }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 2073ec5a85e..390e03896bd 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -210,17 +210,26 @@ void goto_symext::symex_goto(statet &state)
   // merge_gotos when we visit new_state_pc
   framet::goto_state_listt &goto_state_list =
     state.call_stack().top().goto_state_map[new_state_pc];
-  goto_state_list.emplace_back(state.source, state);
 
-  symex_transition(state, state_pc, backward);
-
-  // adjust guards
+  // On an unconditional GOTO we don't need our state, as it will be overwritten
+  // by merge_goto. Therefore we move it onto goto_state_list instead of copying
+  // as usual.
   if(new_guard.is_true())
   {
+    // The move here only moves goto_statet, the base class of goto_symex_statet
+    // and not the entire thing.
+    goto_state_list.emplace_back(state.source, std::move(state));
+
+    symex_transition(state, state_pc, backward);
+
     state.guard = guardt(false_exprt(), guard_manager);
   }
   else
   {
+    goto_state_list.emplace_back(state.source, state);
+
+    symex_transition(state, state_pc, backward);
+
     // produce new guard symbol
     exprt guard_expr;
 
@@ -319,20 +328,28 @@ void goto_symext::merge_goto(
       "atomic sections differ across branches",
       state.source.pc->source_location);
 
-  // do SSA phi functions
-  phi_function(goto_state, state);
+  if(!goto_state.guard.is_false())
+  {
+    if(state.guard.is_false())
+    {
+      // Important to note that we're moving into our base class here.
+      static_cast<goto_statet &>(state) = std::move(goto_state);
+    }
+    else
+    {
+      // do SSA phi functions
+      phi_function(goto_state, state);
 
-  // merge value sets
-  if(state.guard.is_false() && !goto_state.guard.is_false())
-    state.value_set = std::move(goto_state.value_set);
-  else if(!goto_state.guard.is_false())
-    state.value_set.make_union(goto_state.value_set);
+      // merge value sets
+      state.value_set.make_union(goto_state.value_set);
 
-  // adjust guard
-  state.guard|=goto_state.guard;
+      // adjust guard
+      state.guard |= goto_state.guard;
 
-  // adjust depth
-  state.depth=std::min(state.depth, goto_state.depth);
+      // adjust depth
+      state.depth = std::min(state.depth, goto_state.depth);
+    }
+  }
 }
 
 /// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and
@@ -505,8 +522,8 @@ void goto_symext::phi_function(
   statet &dest_state)
 {
   if(
-    goto_state.level2.current_names.empty() &&
-    dest_state.level2.current_names.empty())
+    goto_state.get_level2().current_names.empty() &&
+    dest_state.get_level2().current_names.empty())
     return;
 
   guardt diff_guard = goto_state.guard;
@@ -514,8 +531,8 @@ void goto_symext::phi_function(
   diff_guard -= dest_state.guard;
 
   for_each2(
-    goto_state.level2.current_names,
-    dest_state.level2.current_names,
+    goto_state.get_level2().current_names,
+    dest_state.get_level2().current_names,
     [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) {
       merge_names(
         goto_state,
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 159d127be30..d0e66eb15ca 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -324,10 +324,16 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
     throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
+  // Get our path_storage pointer because this state will live beyond
+  // this instance of goto_symext, so we can't take the reference directly.
+  auto *storage = &path_storage;
+
   // create and prepare the state
   auto state = util_make_unique<statet>(
     symex_targett::sourcet(entry_point_id, start_function->body),
-    guard_manager);
+    guard_manager,
+    [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
+
   CHECK_RETURN(!state->threads.empty());
   CHECK_RETURN(!state->call_stack().empty());
 
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index e4e5b8306f6..4f4807a1674 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -52,8 +52,8 @@ void goto_symext::symex_start_thread(statet &state)
   // create a copy of the local variables for the new thread
   framet &frame = state.call_stack().top();
 
-  for(auto c_it = state.level2.current_names.begin();
-      c_it != state.level2.current_names.end();
+  for(auto c_it = state.get_level2().current_names.begin();
+      c_it != state.get_level2().current_names.end();
       ++c_it)
   {
     const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
@@ -67,7 +67,7 @@ void goto_symext::symex_start_thread(statet &state)
     // get L0 name for current thread
     lhs.set_level_0(t);
     const irep_idt &l0_name = lhs.get_identifier();
-    std::size_t l1_index = path_storage.get_unique_index(l0_name, 0);
+    std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
     CHECK_RETURN(l1_index == 0);
 
     // set up L1 name
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index 3eddaf1dd8a..f34d4ede04a 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -53,6 +53,15 @@ class symex_targett
         pc(_goto_program.instructions.begin())
     {
     }
+
+    sourcet(sourcet &&other) noexcept
+      : thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc)
+    {
+    }
+
+    sourcet(const sourcet &other) = default;
+    sourcet &operator=(const sourcet &other) = default;
+    sourcet &operator=(sourcet &&other) = default;
   };
 
   enum class assignment_typet
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index fff3f3afa94..78e63444cd2 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -45,6 +45,11 @@ class value_sett
   {
   }
 
+  value_sett(value_sett &&other)
+    : location_number(other.location_number), values(std::move(other.values))
+  {
+  }
+
   virtual ~value_sett() = default;
 
   value_sett(const value_sett &other) = default;