Do not assign a non-ssa expr to an object that is accessed via an ssa_exprt ref

Previously a variable `expr` of type `exprt &` was cast to `ssa_exprt &` and
assigned to variable `ssa`. Later the object was modified via assigning a
non-ssa expression to `expr`, violating the invariants of `ssa_exprt`.

Author: danpoe

src/goto-symex/goto_symex_state.cpp

@@ -285,13 +285,10 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
 
-      if(l2_thread_read_encoding(ssa, ns))
+      // renaming taken care of by l2_thread_encoding, or already at L2
+      if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty())
       {
-        // renaming taken care of by l2_thread_encoding
-      }
-      else if(!ssa.get_level_2().empty())
-      {
-        // already at L2
+        return renamedt<exprt, level>(std::move(ssa));
       }
       else
       {
@@ -300,11 +297,15 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
         auto p_it = propagation.find(ssa.get_identifier());
 
         if(p_it.has_value())
-          expr = *p_it; // already L2
+        {
+          return renamedt<exprt, level>(*p_it); // already L2
+        }
         else
+        {
           ssa = set_indices<L2>(std::move(ssa), ns).get();
+          return renamedt<exprt, level>(std::move(ssa));
+        }
       }
-      return renamedt<exprt, level>(std::move(ssa));
     }
   }
   else if(expr.id()==ID_symbol)