Remove L1 case from rename

rename_level1 should be called instead now.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -365,78 +365,63 @@ void goto_symex_statet::rename(
   levelt level)
 {
   // rename all the symbols with their last known value
+  PRECONDITION(level == L2);
 
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
     ssa_exprt &ssa=to_ssa_expr(expr);
+    set_l1_indices(level0, level1, ssa, source.thread_nr, ns);
+    rename(expr.type(), ssa.get_identifier(), ns);
+    ssa.update_type();
 
-    if(level == L1)
+    if(l2_thread_read_encoding(ssa, ns))
+    {
+      // renaming taken care of by l2_thread_encoding
+    }
+    else if(!ssa.get_level_2().empty())
     {
-      set_l1_indices(level1, ssa, source.thread_nr, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
-      ssa.update_type();
+      // already at L2
     }
-    else if(level==L2)
+    else
     {
-      set_l1_indices(level1, ssa, source.thread_nr, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
-      ssa.update_type();
+      // We also consider propagation if we go up to L2.
+      // L1 identifiers are used for propagation!
+      auto p_it = propagation.find(ssa.get_identifier());
 
-      if(l2_thread_read_encoding(ssa, ns))
-      {
-        // renaming taken care of by l2_thread_encoding
-      }
-      else if(!ssa.get_level_2().empty())
-      {
-        // already at L2
-      }
+      if(p_it != propagation.end())
+        expr = p_it->second; // already L2
       else
-      {
-        // We also consider propagation if we go up to L2.
-        // L1 identifiers are used for propagation!
-        auto p_it = propagation.find(ssa.get_identifier());
-
-        if(p_it != propagation.end())
-          expr=p_it->second; // already L2
-        else
-          set_l2_indices(level1, level2, ssa, source.thread_nr, ns);
-      }
+        set_l2_indices(level0, level1, level2, ssa, source.thread_nr, ns);
     }
-    else
-      UNREACHABLE;
   }
   else if(expr.id()==ID_symbol)
   {
     // we never rename function symbols
     if(expr.type().id() == ID_code)
     {
-      rename(
-        expr.type(),
-        to_symbol_expr(expr).get_identifier(),
-        ns,
-        level);
+      rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns, L2);
 
       return;
     }
 
     expr=ssa_exprt(expr);
-    rename(expr, ns, level);
+    rename(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(address_of_expr.object(), ns, L2);
     to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();
   }
   else
   {
     // this could go wrong, but we would have to re-typecheck ...
-    rename(expr.type(), irep_idt(), ns, level);
+    rename(expr.type(), irep_idt(), ns, L2);
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns, level);
+      rename(*it, ns);
 
     // some fixes
     if(expr.id()==ID_with)