diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index f6dbc409471..fc05ad82213 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -222,9 +222,15 @@ void field_sensitivityt::field_assignments_rec(
     exprt ssa_rhs = state.rename(lhs, ns).get();
     simplify(ssa_rhs, ns);
 
-    ssa_exprt ssa_lhs = to_ssa_expr(lhs_fs);
-    state.assignment(
-      ssa_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness);
+    const ssa_exprt ssa_lhs = state
+                                .assignment(
+                                  to_ssa_expr(lhs_fs),
+                                  ssa_rhs,
+                                  ns,
+                                  true,
+                                  true,
+                                  allow_pointer_unsoundness)
+                                .get();
 
     // do the assignment
     target.assignment(
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index c7b31662373..7c6360134ef 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -38,7 +38,7 @@ goto_symex_statet::goto_symex_statet(
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
-    record_events(true),
+    record_events({true}),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
@@ -47,7 +47,8 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// write to a variable
+/// Check that \p expr is correctly renamed to level 2 and return true in case
+/// an error is detected.
 static bool check_renaming(const exprt &expr);
 
 static bool check_renaming(const typet &type)
@@ -151,9 +152,9 @@ goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
   return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
-void goto_symex_statet::assignment(
-  ssa_exprt &lhs, // L0/L1
-  const exprt &rhs,  // L2
+renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
+  ssa_exprt lhs,    // L0/L1
+  const exprt &rhs, // L2
   const namespacet &ns,
   bool rhs_is_simplified,
   bool record_value,
@@ -182,7 +183,8 @@ void goto_symex_statet::assignment(
 
   // do the l2 renaming
   increase_generation(l1_identifier, lhs);
-  lhs = set_indices<L2>(std::move(lhs), ns).get();
+  renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
+  lhs = l2_lhs.get();
 
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
@@ -233,6 +235,8 @@ void goto_symex_statet::assignment(
   value_set.output(ns, std::cout);
   std::cout << "**********************\n";
 #endif
+
+  return l2_lhs;
 }
 
 template <levelt level>
@@ -442,21 +446,21 @@ bool goto_symex_statet::l2_thread_read_encoding(
     else
       tmp = if_exprt{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
 
-    const bool record_events_bak=record_events;
-    record_events=false;
-    assignment(ssa_l1, tmp, ns, true, true);
-    record_events=record_events_bak;
+    record_events.push(false);
+    ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
+    record_events.pop();
 
     symex_target->assignment(
       guard_as_expr,
-      ssa_l1,
-      ssa_l1,
-      ssa_l1.get_original_expr(),
+      ssa_l2,
+      ssa_l2,
+      ssa_l2.get_original_expr(),
       tmp,
       source,
       symex_targett::assignment_typet::PHI);
 
-    expr = set_indices<L2>(std::move(ssa_l1), ns).get();
+    INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
+    expr = std::move(ssa_l2);
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())
@@ -466,7 +470,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // No event and no fresh index, but avoid constant propagation
-  if(!record_events)
+  if(!record_events.top())
   {
     expr = set_indices<L2>(std::move(ssa_l1), ns).get();
     return true;
@@ -488,7 +492,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   const ssa_exprt &expr,
   const namespacet &ns) const
 {
-  if(!record_events)
+  if(!record_events.top())
     return write_is_shared_resultt::NOT_SHARED;
 
   PRECONDITION(dirty != nullptr);
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index e568a5ee04b..3751037956f 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -108,13 +108,14 @@ class goto_symex_statet final : public goto_statet
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
-  void assignment(
-    ssa_exprt &lhs, // L0/L1
-    const exprt &rhs,  // L2
+  /// \return lhs renamed to level 2
+  renamedt<ssa_exprt, L2> assignment(
+    ssa_exprt lhs,    // L0/L1
+    const exprt &rhs, // L2
     const namespacet &ns,
     bool rhs_is_simplified,
     bool record_value,
-    bool allow_pointer_unsoundness=false);
+    bool allow_pointer_unsoundness = false);
 
   field_sensitivityt field_sensitivity;
 
@@ -197,7 +198,7 @@ class goto_symex_statet final : public goto_statet
   write_is_shared_resultt
   write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
 
-  bool record_events;
+  std::stack<bool> record_events;
 
   const incremental_dirtyt *dirty = nullptr;
 
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index d6c7eb69d32..317297c6c7e 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -130,8 +130,8 @@ void postconditiont::strengthen(exprt &dest)
        SSA_step.ssa_lhs.type().id()==ID_struct)
       return;
 
-    equal_exprt equality(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
-    get_original_name(equality);
+    exprt equality =
+      get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs});
 
     if(dest.is_true())
       dest.swap(equality);
@@ -169,8 +169,7 @@ bool postconditiont::is_used(
         it!=expr_set.end();
         it++)
     {
-      exprt tmp(*it);
-      get_original_name(tmp);
+      const exprt tmp = get_original_name(*it);
       find_symbols(tmp, symbols);
     }
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index abd9d8983be..dd0ccb50296 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -140,8 +140,7 @@ void preconditiont::compute_rec(exprt &dest)
   }
   else if(dest==SSA_step.ssa_lhs.get_original_expr())
   {
-    dest=SSA_step.ssa_rhs;
-    get_original_name(dest);
+    dest = get_original_name(SSA_step.ssa_rhs);
   }
   else
     Forall_operands(it, dest)
diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
index d187c11a776..949b47ceea3 100644
--- a/src/goto-symex/renaming_level.cpp
+++ b/src/goto-symex/renaming_level.cpp
@@ -97,26 +97,29 @@ void symex_level1t::restore_from(const current_namest &other)
   }
 }
 
-void get_original_name(exprt &expr)
+exprt get_original_name(exprt expr)
 {
-  get_original_name(expr.type());
+  expr.type() = get_original_name(std::move(expr.type()));
 
   if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol))
-    expr = to_ssa_expr(expr).get_original_expr();
+    return to_ssa_expr(expr).get_original_expr();
   else
+  {
     Forall_operands(it, expr)
-      get_original_name(*it);
+      *it = get_original_name(std::move(*it));
+    return expr;
+  }
 }
 
-void get_original_name(typet &type)
+typet get_original_name(typet type)
 {
   // rename all the symbols with their last known value
 
   if(type.id() == ID_array)
   {
     auto &array_type = to_array_type(type);
-    get_original_name(array_type.subtype());
-    get_original_name(array_type.size());
+    array_type.subtype() = get_original_name(std::move(array_type.subtype()));
+    array_type.size() = get_original_name(std::move(array_type.size()));
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -124,10 +127,12 @@ void get_original_name(typet &type)
     struct_union_typet::componentst &components = s_u_type.components();
 
     for(auto &component : components)
-      get_original_name(component.type());
+      component.type() = get_original_name(std::move(component.type()));
   }
   else if(type.id() == ID_pointer)
   {
-    get_original_name(to_pointer_type(type).subtype());
+    type.subtype() =
+      get_original_name(std::move(to_pointer_type(type).subtype()));
   }
+  return type;
 }
diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h
index c2a631619a7..8096ca37cf0 100644
--- a/src/goto-symex/renaming_level.h
+++ b/src/goto-symex/renaming_level.h
@@ -148,9 +148,9 @@ struct symex_level2t : public symex_renaming_levelt
 };
 
 /// Undo all levels of renaming
-void get_original_name(exprt &expr);
+exprt get_original_name(exprt expr);
 
 /// Undo all levels of renaming
-void get_original_name(typet &type);
+typet get_original_name(typet type);
 
 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 879827a3f1d..c1117be4ed1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -202,22 +202,31 @@ void goto_symext::symex_assign_rec(
       "assignment to `" + lhs.id_string() + "' not handled");
 }
 
-/// Replace "with" (or "update") expressions in \p ssa_rhs by their update
-/// values and move the index or member to the left-hand side \p lhs_mod. This
-/// effectively undoes the work that \ref goto_symext::symex_assign_array and
+/// Assignment from the rhs value to the lhs variable
+struct assignmentt final
+{
+  ssa_exprt lhs;
+  exprt rhs;
+};
+
+/// Replace "with" (or "update") expressions in the right-hand side of
+/// \p assignment by their update values and move the index or member to the
+/// left-hand side of \p assignment. This effectively undoes the work that
+/// \ref goto_symext::symex_assign_array and
 /// \ref goto_symext::symex_assign_struct_member have done, but now making use
 /// of the index/member that may only be known after renaming to L2 has taken
 /// place.
 /// \param [in, out] state: symbolic execution state to perform renaming
-/// \param [in,out] ssa_rhs: right-hand side
-/// \param [in,out] lhs_mod: left-hand side
+/// \param assignment: an assignment to rewrite
 /// \param ns: namespace
-static void rewrite_with_to_field_symbols(
+/// \return the updated assignment
+static assignmentt rewrite_with_to_field_symbols(
   goto_symext::statet &state,
-  exprt &ssa_rhs,
-  ssa_exprt &lhs_mod,
+  assignmentt assignment,
   const namespacet &ns)
 {
+  exprt &ssa_rhs = assignment.rhs;
+  ssa_exprt &lhs_mod = assignment.lhs;
 #ifdef USE_UPDATE
   while(ssa_rhs.id() == ID_update &&
         to_update_expr(ssa_rhs).designator().size() == 1 &&
@@ -281,6 +290,7 @@ static void rewrite_with_to_field_symbols(
     lhs_mod = to_ssa_expr(field_sensitive_lhs);
   }
 #endif
+  return assignment;
 }
 
 /// Replace byte-update operations that only affect individual fields of an
@@ -288,22 +298,23 @@ static void rewrite_with_to_field_symbols(
 /// "update") expressions, which \ref rewrite_with_to_field_symbols will then
 /// take care of.
 /// \param [in, out] state: symbolic execution state to perform renaming
-/// \param [in,out] ssa_rhs: right-hand side
-/// \param [in,out] lhs_mod: left-hand side
+/// \param assignment: assignment to transform
 /// \param ns: namespace
 /// \param do_simplify: set to true if, and only if, simplification is enabled
-static void shift_indexed_access_to_lhs(
+/// \return updated assignment
+static assignmentt shift_indexed_access_to_lhs(
   goto_symext::statet &state,
-  exprt &ssa_rhs,
-  ssa_exprt &lhs_mod,
+  assignmentt assignment,
   const namespacet &ns,
   bool do_simplify)
 {
+  exprt &ssa_rhs = assignment.rhs;
+  ssa_exprt &lhs_mod = assignment.lhs;
   if(
     ssa_rhs.id() == ID_byte_update_little_endian ||
     ssa_rhs.id() == ID_byte_update_big_endian)
   {
-    byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs);
+    const byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs);
     exprt byte_extract = byte_extract_exprt(
       byte_update.id() == ID_byte_update_big_endian
         ? ID_byte_extract_big_endian
@@ -316,8 +327,7 @@ static void shift_indexed_access_to_lhs(
 
     if(byte_extract.id() == ID_symbol)
     {
-      ssa_rhs = byte_update.value();
-      lhs_mod = to_ssa_expr(byte_extract);
+      return assignmentt{to_ssa_expr(byte_extract), byte_update.value()};
     }
     else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member)
     {
@@ -359,10 +369,11 @@ static void shift_indexed_access_to_lhs(
 
       // We may have shifted the previous lhs into the rhs; as the lhs is only
       // L1-renamed, we need to rename again.
-      ssa_rhs = state.rename(ssa_rhs, ns).get();
-      lhs_mod = to_ssa_expr(byte_extract);
+      return assignmentt{to_ssa_expr(byte_extract),
+                         state.rename(std::move(ssa_rhs), ns).get()};
     }
   }
+  return assignment;
 }
 
 /// Assign a struct expression to a symbol. If \ref symex_assign_symbol was used
@@ -426,46 +437,43 @@ void goto_symext::symex_assign_symbol(
     return;
   }
 
-  exprt ssa_rhs=rhs;
-
-  // put assignment guard into the rhs
-  if(!guard.empty())
-  {
-    if_exprt tmp_ssa_rhs(conjunction(guard), ssa_rhs, lhs, ssa_rhs.type());
-    tmp_ssa_rhs.swap(ssa_rhs);
-  }
-
-  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns).get();
-
-  ssa_exprt lhs_mod = lhs;
+  exprt l2_rhs = [&]() {
+    exprt guarded_rhs = rhs;
+    // put assignment guard into the rhs
+    if(!guard.empty())
+    {
+      guarded_rhs =
+        if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()};
+    }
+    return state.rename(std::move(guarded_rhs), ns).get();
+  }();
 
   // Note the following two calls are specifically required for
   // field-sensitivity. For example, with-expressions, which may have just been
   // introduced by symex_assign_struct_member, are transformed into member
   // expressions on the LHS. If we add an option to disable field-sensitivity
   // in the future these should be omitted.
-  shift_indexed_access_to_lhs(
-    state, l2_rhs, lhs_mod, ns, symex_config.simplify_opt);
-  rewrite_with_to_field_symbols(state, l2_rhs, lhs_mod, ns);
-
-  do_simplify(l2_rhs);
-
-  ssa_exprt l2_lhs = lhs_mod;
-  ssa_exprt l1_lhs = l2_lhs; // l2_lhs will be renamed to L2 by the following:
-  state.assignment(
-    l2_lhs,
-    l2_rhs,
-    ns,
-    symex_config.simplify_opt,
-    symex_config.constant_propagation,
-    symex_config.allow_pointer_unsoundness);
-
-  exprt ssa_full_lhs=full_lhs;
-  ssa_full_lhs = add_to_lhs(ssa_full_lhs, l2_lhs);
-  const bool record_events=state.record_events;
-  state.record_events=false;
-  exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
-  state.record_events=record_events;
+  auto assignment = shift_indexed_access_to_lhs(
+    state, assignmentt{lhs, std::move(l2_rhs)}, ns, symex_config.simplify_opt);
+  assignment = rewrite_with_to_field_symbols(state, std::move(assignment), ns);
+
+  do_simplify(assignment.rhs);
+
+  ssa_exprt &l1_lhs = assignment.lhs;
+  ssa_exprt l2_lhs = state
+                       .assignment(
+                         assignment.lhs,
+                         assignment.rhs,
+                         ns,
+                         symex_config.simplify_opt,
+                         symex_config.constant_propagation,
+                         symex_config.allow_pointer_unsoundness)
+                       .get();
+
+  exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs);
+  state.record_events.push(false);
+  const exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
+  state.record_events.pop();
 
   // do the assignment
   const symbolt &symbol = ns.lookup(l2_lhs.get_object_name());
@@ -483,14 +491,13 @@ void goto_symext::symex_assign_symbol(
   // Temporarily add the state guard
   guard.emplace_back(state.guard.as_expr());
 
-  exprt original_lhs = l2_full_lhs;
-  get_original_name(original_lhs);
+  const exprt original_lhs = get_original_name(l2_full_lhs);
   target.assignment(
     conjunction(guard),
     l2_lhs,
     l2_full_lhs,
     original_lhs,
-    l2_rhs,
+    assignment.rhs,
     state.source,
     assignment_type);
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 660bd640d04..55f3e7cc1d8 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -76,14 +76,13 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     CHECK_RETURN(field_generation == 1);
   }
 
-  const bool record_events=state.record_events;
-  state.record_events=false;
+  state.record_events.push(false);
   exprt expr_l2 = state.rename(std::move(ssa), ns).get();
   INVARIANT(
     expr_l2.id() == ID_symbol && expr_l2.get_bool(ID_C_SSA_symbol),
     "symbol to declare should not be replaced by constant propagation");
   ssa = to_ssa_expr(expr_l2);
-  state.record_events=record_events;
+  state.record_events.pop();
 
   // we hide the declaration of auxiliary variables
   // and if the statement itself is hidden
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 1e6d54747f5..5489a8df717 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -202,7 +202,6 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 {
   if(expr.id()==ID_dereference)
   {
-    dereference_exprt to_check = to_dereference_expr(expr);
     bool expr_is_not_null = false;
 
     if(state.threads.size() == 1)
@@ -210,7 +209,8 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
       const irep_idt &expr_function = state.source.function_id;
       if(!expr_function.empty())
       {
-        get_original_name(to_check);
+        const dereference_exprt to_check =
+          to_dereference_expr(get_original_name(expr));
 
         expr_is_not_null = path_storage.safe_pointers.at(expr_function)
                              .is_safe_dereference(to_check, state.source.pc);
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index baa61bc7647..0fdfcbbe938 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -310,7 +310,8 @@ void goto_symext::symex_goto(statet &state)
 
       ssa_exprt new_lhs =
         state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
-      state.assignment(new_lhs, new_rhs, ns, true, false);
+      new_lhs =
+        state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
 
       guardt guard{true_exprt{}, guard_manager};
 
@@ -527,11 +528,10 @@ static void merge_names(
       simplify(rhs, ns);
   }
 
-  ssa_exprt new_lhs = ssa;
-  const bool record_events = dest_state.record_events;
-  dest_state.record_events = false;
-  dest_state.assignment(new_lhs, rhs, ns, true, true);
-  dest_state.record_events = record_events;
+  dest_state.record_events.push(false);
+  const ssa_exprt new_lhs =
+    dest_state.assignment(ssa, rhs, ns, true, true).get();
+  dest_state.record_events.pop();
 
   log.conditional_output(
     log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 2a3fb8b92b2..a1eccab9bf4 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -747,10 +747,9 @@ void goto_symext::try_filter_value_sets(
     // something that just replaces `*&x` with `x` whenever it finds it.
     do_simplify(modified_condition);
 
-    const bool record_events = state.record_events;
-    state.record_events = false;
+    state.record_events.push(false);
     modified_condition = state.rename(std::move(modified_condition), ns).get();
-    state.record_events = record_events;
+    state.record_events.pop();
 
     do_simplify(modified_condition);
 
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index cdd483f6e32..66921875c32 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -85,8 +85,7 @@ void goto_symext::symex_start_thread(statet &state)
     ssa_exprt rhs = pair.second.first;
 
     exprt::operandst lhs_conditions;
-    const bool record_events=state.record_events;
-    state.record_events=false;
+    state.record_events.push(false);
     symex_assign_symbol(
       state,
       lhs_l1,
@@ -94,7 +93,7 @@ void goto_symext::symex_start_thread(statet &state)
       rhs,
       lhs_conditions,
       symex_targett::assignment_typet::HIDDEN);
-    state.record_events=record_events;
+    state.record_events.pop();
   }
 
   // initialize all variables marked thread-local