Make symex_level2t::operator() handle non-empty L2

This was handled by set_l2_indices, but it is neccessary to handle it in
symex_level2t for making set_l2_indices return a renamedt.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -250,8 +250,6 @@ goto_symex_statet::set_l1_indices(ssa_exprt ssa_expr, const namespacet &ns)
 ssa_exprt
 goto_symex_statet::set_l2_indices(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  if(!ssa_expr.get_level_2().empty())
-    return ssa_expr;
   renamedt<ssa_exprt, L2> l2 =
     level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
   return l2.get();

src/goto-symex/renaming_level.cpp

@@ -69,6 +69,12 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
 renamedt<ssa_exprt, L2> symex_level2t::
 operator()(renamedt<ssa_exprt, L1> l1_expr) const
 {
+  if(!l1_expr.get().get_level_2().empty())
+  {
+    // TODO reaching here means the information that l1_expr was L2 has
+    // TODO been lost somewhere during execution, which should be avoided
+    return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
+  }
   l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier()));
   return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
 }