remove_level2 function returning a level1t<exprt>

Make clearer that remove_level2 returns an expression renamed up to
level 1.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -224,17 +224,16 @@ void goto_symex_statet::assignment(
     // update value sets
     exprt l1_rhs(rhs);
     get_l1_name(l1_rhs);
-
-    ssa_exprt l1_lhs(lhs);
-    l1_lhs.remove_level_2();
+    level1t<ssa_exprt> l1_lhs = remove_level2(lhs);
 
     if(run_validation_checks)
     {
-      DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
+      DATA_INVARIANT(
+        !check_renaming_l1(l1_lhs.expr), "lhs renaming failed on l1");
       DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
     }
 
-    value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
+    value_set.assign(l1_lhs.expr, l1_rhs, ns, rhs_is_simplified, is_shared);
   }
 
   #if 0

src/goto-symex/renaming_level.h

@@ -71,6 +71,12 @@ struct level1t
   underlyingt expr;
 };
 
+inline level1t<ssa_exprt> remove_level2(ssa_exprt ssa)
+{
+  ssa.remove_level_2();
+  return level1t<ssa_exprt>{ssa};
+}
+
 /// Set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.