string refiner no longer needs to consider renamed function symbols

The mathematical functions used by the string refiner are no longer renamed,
and thus, there's no longer any need to extract the original name from an
ssa_exprt.

Author: Daniel Kroening

src/solvers/strings/string_constraint_generator_main.cpp

@@ -346,8 +346,8 @@ static irep_idt get_function_name(const function_application_exprt &expr)
 {
   const exprt &name = expr.function();
   PRECONDITION(name.id() == ID_symbol);
-  return is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
-                           : to_symbol_expr(name).get_identifier();
+  PRECONDITION(!is_ssa_expr(name));
+  return to_symbol_expr(name).get_identifier();
 }
 
 optionalt<exprt> string_constraint_generatort::make_array_pointer_association(

src/solvers/strings/string_refinement_util.cpp

@@ -209,8 +209,9 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
   array_poolt &array_pool)
 {
   const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
-  const irep_idt &id = is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
-                                         : name.get_identifier();
+  PRECONDITION(!is_ssa_expr(name));
+
+  const irep_idt &id = name.get_identifier();
 
   if(id == ID_cprover_string_insert_func)
     return util_make_unique<string_insertion_builtin_functiont>(

src/util/simplify_expr.cpp

@@ -165,8 +165,12 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
 {
   const function_application_exprt &function_app =
     to_function_application_expr(expr);
-  irep_idt func_id =
-    function_app.function().find(ID_expression).get(ID_identifier);
+
+  if(function_app.function().id() != ID_symbol)
+    return true;
+
+  const irep_idt func_id =
+    to_symbol_expr(function_app.function()).get_identifier();
 
   // Starts-with is used for .equals.
   if(func_id == ID_cprover_string_startswith_func)