diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 0469fddcfb4..5906c38680d 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -69,11 +69,7 @@ bool scratch_programt::check_sat(bool do_slice)
 
 exprt scratch_programt::eval(const exprt &e)
 {
-  exprt ssa=e;
-
-  symex_state->rename(ssa, ns);
-
-  return checker->get(ssa);
+  return checker->get(symex_state->rename<goto_symex_statet::L2>(e, ns));
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index e4d5af7095e..e341c6c89f5 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -163,11 +163,11 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  rename(lhs, ns, L1);
+  lhs = rename_ssa<L1>(std::move(lhs), ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
-  rename(lhs.type(), l1_identifier, ns);
+  rename<L2>(lhs.type(), l1_identifier, ns);
   lhs.update_type();
   if(run_validation_checks)
   {
@@ -263,10 +263,31 @@ void goto_symex_statet::set_l2_indices(
   ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }
 
-void goto_symex_statet::rename(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+template <goto_symex_statet::levelt level>
+ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
+{
+  static_assert(
+    level == L0 || level == L1,
+    "rename_ssa can only be used for levels L0 and L1");
+  if(level == L0)
+    set_l0_indices(ssa, ns);
+  else if(level == L1)
+    set_l1_indices(ssa, ns);
+  else
+    UNREACHABLE;
+
+  rename<level>(ssa.type(), ssa.get_identifier(), ns);
+  ssa.update_type();
+  return ssa;
+}
+
+/// Ensure `rename_ssa` gets compiled for L0
+template ssa_exprt goto_symex_statet::rename_ssa<goto_symex_statet::L0>(
+  ssa_exprt ssa,
+  const namespacet &ns);
+
+template <goto_symex_statet::levelt level>
+exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -277,20 +298,16 @@ void goto_symex_statet::rename(
 
     if(level == L0)
     {
-      set_l0_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
-      ssa.update_type();
+      ssa = rename_ssa<L0>(std::move(ssa), ns);
     }
     else if(level == L1)
     {
-      set_l1_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
-      ssa.update_type();
+      ssa = rename_ssa<L1>(std::move(ssa), ns);
     }
     else if(level==L2)
     {
       set_l1_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
+      rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
 
       if(l2_thread_read_encoding(ssa, ns))
@@ -318,33 +335,24 @@ void goto_symex_statet::rename(
   {
     // we never rename function symbols
     if(as_const(expr).type().id() == ID_code)
-    {
-      rename(
-        expr.type(),
-        to_symbol_expr(expr).get_identifier(),
-        ns,
-        level);
-
-      return;
-    }
-
-    expr=ssa_exprt(expr);
-    rename(expr, ns, level);
+      rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
+    else
+      expr = rename<level>(ssa_exprt{expr}, ns);
   }
   else if(expr.id()==ID_address_of)
   {
     auto &address_of_expr = to_address_of_expr(expr);
-    rename_address(address_of_expr.object(), ns, level);
+    rename_address<level>(address_of_expr.object(), ns);
     to_pointer_type(expr.type()).subtype() =
       as_const(address_of_expr).object().type();
   }
   else
   {
-    rename(expr.type(), irep_idt(), ns, level);
+    rename<level>(expr.type(), irep_idt(), ns);
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns, level);
+      *it = rename<level>(std::move(*it), ns);
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -356,6 +364,7 @@ void goto_symex_statet::rename(
       "Type of renamed expr should be the same as operands for with_exprt and "
       "if_exprt");
   }
+  return expr;
 }
 
 /// thread encoding
@@ -535,10 +544,8 @@ bool goto_symex_statet::l2_thread_write_encoding(
   return threads.size()>1;
 }
 
-void goto_symex_statet::rename_address(
-  exprt &expr,
-  const namespacet &ns,
-  levelt level)
+template <goto_symex_statet::levelt level>
+void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
@@ -548,13 +555,13 @@ void goto_symex_statet::rename_address(
     // only do L1!
     set_l1_indices(ssa, ns);
 
-    rename(expr.type(), ssa.get_identifier(), ns, level);
+    rename<level>(expr.type(), ssa.get_identifier(), ns);
     ssa.update_type();
   }
   else if(expr.id()==ID_symbol)
   {
     expr=ssa_exprt(expr);
-    rename_address(expr, ns, level);
+    rename_address<level>(expr, ns);
   }
   else
   {
@@ -562,20 +569,20 @@ void goto_symex_statet::rename_address(
     {
       index_exprt &index_expr=to_index_expr(expr);
 
-      rename_address(index_expr.array(), ns, level);
+      rename_address<level>(index_expr.array(), ns);
       PRECONDITION(index_expr.array().type().id() == ID_array);
       expr.type() = to_array_type(index_expr.array().type()).subtype();
 
       // the index is not an address
-      rename(index_expr.index(), ns, level);
+      index_expr.index() = rename<level>(std::move(index_expr.index()), ns);
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      rename(if_expr.cond(), ns, level);
-      rename_address(if_expr.true_case(), ns, level);
-      rename_address(if_expr.false_case(), ns, level);
+      if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns);
+      rename_address<level>(if_expr.true_case(), ns);
+      rename_address<level>(if_expr.false_case(), ns);
 
       if_expr.type()=if_expr.true_case().type();
     }
@@ -583,7 +590,7 @@ void goto_symex_statet::rename_address(
     {
       member_exprt &member_expr=to_member_expr(expr);
 
-      rename_address(member_expr.struct_op(), ns, level);
+      rename_address<level>(member_expr.struct_op(), ns);
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
@@ -600,17 +607,17 @@ void goto_symex_statet::rename_address(
         expr.type()=comp.type();
       }
       else
-        rename(expr.type(), irep_idt(), ns, level);
+        rename<level>(expr.type(), irep_idt(), ns);
     }
     else
     {
       // this could go wrong, but we would have to re-typecheck ...
-      rename(expr.type(), irep_idt(), ns, level);
+      rename<level>(expr.type(), irep_idt(), ns);
 
       // do this recursively; we assume here
       // that all the operands are addresses
       Forall_operands(it, expr)
-        rename_address(*it, ns, level);
+        rename_address<level>(*it, ns);
     }
   }
 }
@@ -668,11 +675,11 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   return false;
 }
 
+template <goto_symex_statet::levelt level>
 void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,
-  const namespacet &ns,
-  levelt level)
+  const namespacet &ns)
 {
   // check whether there are symbol expressions in the type; if not, there
   // is no need to expand the struct/union tags in the type
@@ -711,8 +718,8 @@ void goto_symex_statet::rename(
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);
-    rename(array_type.subtype(), irep_idt(), ns, level);
-    rename(array_type.size(), ns, level);
+    rename<level>(array_type.subtype(), irep_idt(), ns);
+    array_type.size() = rename<level>(std::move(array_type.size()), ns);
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -723,14 +730,17 @@ void goto_symex_statet::rename(
     {
       // be careful, or it might get cyclic
       if(component.type().id() == ID_array)
-        rename(to_array_type(component.type()).size(), ns, level);
+      {
+        auto &array_type = to_array_type(component.type());
+        array_type.size() = rename<level>(std::move(array_type.size()), ns);
+      }
       else if(component.type().id() != ID_pointer)
-        rename(component.type(), irep_idt(), ns, level);
+        rename<level>(component.type(), irep_idt(), ns);
     }
   }
   else if(type.id()==ID_pointer)
   {
-    rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
+    rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
   }
 
   if(level==L2 &&
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index c4eab3bfc59..76e77366969 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -179,12 +179,16 @@ class goto_symex_statet final : public goto_statet
   ///
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
-  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
-  void rename(
-    typet &type,
-    const irep_idt &l1_identifier,
-    const namespacet &ns,
-    levelt level=L2);
+  template <levelt level = L2>
+  exprt rename(exprt expr, const namespacet &ns);
+
+  /// Version of rename which is specialized for SSA exprt.
+  /// Implementation only exists for level L0 and L1.
+  template <levelt level>
+  ssa_exprt rename_ssa(ssa_exprt ssa, const namespacet &ns);
+
+  template <levelt level = L2>
+  void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
   void assignment(
     ssa_exprt &lhs, // L0/L1
@@ -195,7 +199,8 @@ class goto_symex_statet final : public goto_statet
     bool allow_pointer_unsoundness=false);
 
 protected:
-  void rename_address(exprt &expr, const namespacet &ns, levelt level);
+  template <levelt>
+  void rename_address(exprt &expr, const namespacet &ns);
 
   /// Update level 0 values.
   void set_l0_indices(ssa_exprt &expr, const namespacet &ns);
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 6a14b74bd8b..32f93d89a50 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -212,13 +212,13 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  state.rename(ssa_rhs, ns);
-  do_simplify(ssa_rhs);
+  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns);
+  do_simplify(l2_rhs);
 
   ssa_exprt ssa_lhs=lhs;
   state.assignment(
     ssa_lhs,
-    ssa_rhs,
+    l2_rhs,
     ns,
     symex_config.simplify_opt,
     symex_config.constant_propagation,
@@ -228,7 +228,7 @@ void goto_symext::symex_assign_symbol(
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename(ssa_full_lhs, ns);
+  exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -254,8 +254,9 @@ void goto_symext::symex_assign_symbol(
   target.assignment(
     tmp_guard.as_expr(),
     ssa_lhs,
-    ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
-    ssa_rhs,
+    l2_full_lhs,
+    add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
+    l2_rhs,
     state.source,
     assignment_type);
 }
@@ -406,8 +407,7 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard=lhs.cond();
-  state.rename(renamed_guard, ns);
+  exprt renamed_guard = state.rename(lhs.cond(), ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 55af78d76bb..105f4fe5ba8 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -71,8 +71,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt tmp_size=size;
-    state.rename(tmp_size, ns); // to allow constant propagation
+    // to allow constant propagation
+    exprt tmp_size = state.rename(size, ns);
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -164,8 +164,8 @@ void goto_symext::symex_allocate(
 
   state.symbol_table.add(value_symbol);
 
-  exprt zero_init=code.op1();
-  state.rename(zero_init, ns); // to allow constant propagation
+  // to allow constant propagation
+  exprt zero_init = state.rename(code.op1(), ns);
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -233,8 +233,8 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  exprt tmp=code.op0();
-  state.rename(tmp, ns); // to allow constant propagation
+  // to allow constant propagation
+  exprt tmp = state.rename(code.op0(), ns);
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
@@ -311,8 +311,7 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs=rhs;
-  state.rename(tmp_rhs, ns);
+  exprt tmp_rhs = state.rename(rhs, ns);
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
@@ -336,17 +335,15 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg=code.op0();
-
-  state.rename(id_arg, ns);
+  exprt id_arg = state.rename(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
-    do_simplify(args.back());
+    exprt l2_arg = state.rename(code.operands()[i], ns);
+    do_simplify(l2_arg);
+    args.emplace_back(std::move(l2_arg));
   }
 
   const irep_idt input_id=get_string_argument(id_arg, ns);
@@ -359,18 +356,15 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-
-  exprt id_arg=code.op0();
-
-  state.rename(id_arg, ns);
+  exprt id_arg = state.rename(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
-    do_simplify(args.back());
+    exprt l2_arg = state.rename(code.operands()[i], ns);
+    do_simplify(l2_arg);
+    args.emplace_back(std::move(l2_arg));
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
@@ -481,11 +475,7 @@ void goto_symext::symex_trace(
     irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
 
     for(std::size_t j=2; j<code.arguments().size(); j++)
-    {
-      exprt var(code.arguments()[j]);
-      state.rename(var, ns);
-      vars.push_back(var);
-    }
+      vars.push_back(state.rename(code.arguments()[j], ns));
 
     target.output(state.guard.as_expr(), state.source, event, vars);
   }
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index 52b0f98b307..a2efbbd0101 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -26,8 +26,7 @@ void goto_symext::symex_dead(statet &state)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa(code.symbol());
-  state.rename(ssa, ns, goto_symex_statet::L1);
+  ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
@@ -38,12 +37,12 @@ void goto_symext::symex_dead(statet &state)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
-    state.value_set.assign(ssa, rhs, ns, true, false);
+    const exprt l1_rhs =
+      state.rename<goto_symex_statet::L1>(std::move(rhs), ns);
+    state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 
-  ssa_exprt ssa_lhs=to_ssa_expr(ssa);
-  const irep_idt &l1_identifier=ssa_lhs.get_identifier();
+  const irep_idt &l1_identifier = ssa.get_identifier();
 
   // prevent propagation
   state.propagation.erase(l1_identifier);
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index aa4122826ab..69897f28737 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -37,9 +37,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa(expr);
-  state.rename(ssa, ns, goto_symex_statet::L1);
-  const irep_idt &l1_identifier=ssa.get_identifier();
+  ssa_exprt ssa = state.rename_ssa<statet::L1>(ssa_exprt{expr}, ns);
+  const irep_idt &l1_identifier = ssa.get_identifier();
 
   // rename type to L2
   state.rename(ssa.type(), l1_identifier, ns);
@@ -54,8 +53,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename(rhs, ns, goto_symex_statet::L1);
-    state.value_set.assign(ssa, rhs, ns, true, false);
+    exprt l1_rhs = state.rename<goto_symex_statet::L1>(std::move(rhs), ns);
+    state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 
   // prevent propagation
@@ -70,7 +69,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   symex_renaming_levelt::increase_counter(level2_it);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename(ssa, ns);
+  exprt expr_l2 = state.rename(std::move(ssa), ns);
+  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;
 
   // we hide the declaration of auxiliary variables
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 3c18d106d90..552ad65b4ef 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -357,11 +357,11 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  state.rename(expr, ns, goto_symex_statet::L1);
+  exprt l1_expr = state.rename<goto_symex_statet::L1>(expr, ns);
 
   // start the recursion!
-  dereference_rec(expr, state);
+  dereference_rec(l1_expr, state);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  state.rename(expr, ns, goto_symex_statet::L1);
+  expr = state.rename<goto_symex_statet::L1>(std::move(l1_expr), ns);
 }
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index ba53ba96b98..6cf0d0dce1c 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -50,9 +50,9 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      symbol_exprt sym_expr=sym.symbol_expr();
-      state.rename(sym_expr, ns, goto_symex_statet::L1);
-      sym.name=to_ssa_expr(sym_expr).get_identifier();
+      const ssa_exprt sym_expr = state.rename_ssa<goto_symex_statet::L1>(
+        ssa_exprt{sym.symbol_expr()}, ns);
+      sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
     }
@@ -70,9 +70,9 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      symbol_exprt sym_expr=sym.symbol_expr();
-      state.rename(sym_expr, ns, goto_symex_statet::L1);
-      sym.name=to_ssa_expr(sym_expr).get_identifier();
+      const ssa_exprt sym_expr = state.rename_ssa<goto_symex_statet::L1>(
+        ssa_exprt{sym.symbol_expr()}, ns);
+      sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
     }
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 49f1cd179c1..9921bdd6cd4 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -261,7 +261,7 @@ void goto_symext::symex_function_call_code(
   // read the arguments -- before the locality renaming
   exprt::operandst arguments = call.arguments();
   for(auto &a : arguments)
-    state.rename(a, ns);
+    a = state.rename(std::move(a), ns);
 
   // we hide the call if the caller and callee are both hidden
   const bool hidden = state.top().hidden_function && goto_function.is_hidden();
@@ -395,8 +395,8 @@ static void locality(
       it++)
   {
     // get L0 name
-    ssa_exprt ssa(ns.lookup(*it).symbol_expr());
-    state.rename(ssa, ns, goto_symex_statet::L0);
+    ssa_exprt ssa = state.rename_ssa<goto_symex_statet::L0>(
+      ssa_exprt{ns.lookup(*it).symbol_expr()}, ns);
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
@@ -418,17 +418,18 @@ static void locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.rename(ssa, ns, goto_symex_statet::L1);
+    ssa_exprt ssa_l1 =
+      state.rename_ssa<goto_symex_statet::L1>(std::move(ssa), ns);
 
-    irep_idt l1_name=ssa.get_identifier();
+    irep_idt l1_name = ssa_l1.get_identifier();
     unsigned offset=0;
 
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
       symex_renaming_levelt::increase_counter(c_it);
       ++offset;
-      ssa.set_level_1(frame_nr+offset);
-      l1_name=ssa.get_identifier();
+      ssa_l1.set_level_1(frame_nr + offset);
+      l1_name = ssa_l1.get_identifier();
     }
 
     // now unique -- store
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index e5977b63ecc..50a1b9c71a9 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -37,8 +37,7 @@ void goto_symext::symex_goto(statet &state)
   exprt old_guard = instruction.get_condition();
   clean_expr(old_guard, state, false);
 
-  exprt new_guard=old_guard;
-  state.rename(new_guard, ns);
+  exprt new_guard = state.rename(old_guard, ns);
   do_simplify(new_guard);
 
   if(new_guard.is_false())
@@ -248,8 +247,8 @@ void goto_symext::symex_goto(statet &state)
         symbol_exprt(statet::guard_identifier(), bool_typet());
       exprt new_rhs = boolean_negate(new_guard);
 
-      ssa_exprt new_lhs(guard_symbol_expr);
-      state.rename(new_lhs, ns, goto_symex_statet::L1);
+      ssa_exprt new_lhs =
+        state.rename_ssa<statet::L1>(ssa_exprt{guard_symbol_expr}, ns);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
       guardt guard{true_exprt{}};
@@ -269,8 +268,7 @@ void goto_symext::symex_goto(statet &state)
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr = boolean_negate(guard_symbol_expr);
-      state.rename(guard_expr, ns);
+      guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns);
     }
 
     if(state.has_saved_jump_target)
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 94e46ea9220..4ad370eae64 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -95,18 +95,18 @@ void goto_symext::vcc(
   }
 
   // now rename, enables propagation
-  state.rename(expr, ns);
+  exprt l2_expr = state.rename(std::move(expr), ns);
 
   // now try simplifier on it
-  do_simplify(expr);
+  do_simplify(l2_expr);
 
-  if(expr.is_true())
+  if(l2_expr.is_true())
     return;
 
-  state.guard.guard_expr(expr);
+  state.guard.guard_expr(l2_expr);
 
   state.remaining_vccs++;
-  target.assertion(state.guard.as_expr(), expr, msg, state.source);
+  target.assertion(state.guard.as_expr(), l2_expr, msg, state.source);
 }
 
 void goto_symext::symex_assume(statet &state, const exprt &cond)
@@ -410,8 +410,7 @@ void goto_symext::symex_step(
     {
       exprt tmp = instruction.get_condition();
       clean_expr(tmp, state, false);
-      state.rename(tmp, ns);
-      symex_assume(state, tmp);
+      symex_assume(state, state.rename(std::move(tmp), ns));
     }
 
     symex_transition(state);
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index b339f85f489..97fa11c5b5d 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -73,8 +73,8 @@ void goto_symext::symex_start_thread(statet &state)
       std::forward_as_tuple(lhs.get_l1_object_identifier()),
       std::forward_as_tuple(lhs, 0));
     CHECK_RETURN(emplace_result.second);
-    state.rename(lhs, ns, goto_symex_statet::L1);
-    const irep_idt l1_name=lhs.get_l1_object_identifier();
+    const ssa_exprt lhs_l1 = state.rename_ssa<statet::L1>(std::move(lhs), ns);
+    const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);
     new_thread.call_stack.back().local_objects.insert(l1_name);
@@ -87,7 +87,7 @@ void goto_symext::symex_start_thread(statet &state)
     state.record_events=false;
     symex_assign_symbol(
       state,
-      lhs,
+      lhs_l1,
       nil_exprt(),
       rhs,
       guard,