check_l1_renaming function for ssa_exprt

This is required to replace the use of value_sett by symex_value_sett so
that we can provide the right type of arguments.

Author: romainbrenguier

src/goto-symex/renamed.cpp

@@ -112,6 +112,13 @@ optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr)
   return {};
 }
 
+optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr)
+{
+  if(is_l1_renamed(expr))
+    return renamedt<ssa_exprt, L1>(std::move(expr));
+  return {};
+}
+
 optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr)
 {
   if(is_l2_renamed(expr))

src/goto-symex/renamed.h

@@ -77,6 +77,7 @@ class renamedt : private underlyingt
       get_mutated_expr);
 
   friend optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
+  friend optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr);
   friend optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
   friend optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
 
@@ -124,6 +125,8 @@ bool is_l1_renamed(const exprt &expr);
 /// \return a renamed object if \p expr has been renamed to level 1
 NODISCARD optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
 
+NODISCARD optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr);
+
 /// \return a renamed object if \p expr has been renamed to level 2
 NODISCARD optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);