Extract a rename_level1_ssa function

This can be useful when we now from the caller that the expression is
already is in SSA form.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -271,6 +271,15 @@ goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
   return ssa;
 }
 
+ssa_exprt
+goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
+{
+  set_l1_indices(ssa, ns);
+  rename<L1>(ssa.type(), ssa.get_identifier(), ns);
+  ssa.update_type();
+  return ssa;
+}
+
 template <goto_symex_statet::levelt level>
 void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
 {
@@ -287,9 +296,7 @@ void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
     }
     else if(level == L1)
     {
-      set_l1_indices(ssa, ns);
-      rename<level>(expr.type(), ssa.get_identifier(), ns);
-      ssa.update_type();
+      ssa = rename_level1_ssa(std::move(ssa), ns);
     }
     else if(level==L2)
     {

src/goto-symex/goto_symex_state.h

@@ -184,6 +184,8 @@ class goto_symex_statet final : public goto_statet
 
   ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
 
+  ssa_exprt rename_level1_ssa(ssa_exprt ssa, const namespacet &ns);
+
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);