Minor code improvements in generator_insert

Remove duplicate code for add_axioms_for_insert_float.
Style: indentation in add_axioms_for_insert.
Remove useless comment.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -58,7 +58,6 @@ exprt string_constraint_generatort::add_axioms_for_insert(
   PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
   array_string_exprt s1 = get_string_expr(f.arguments()[2]);
   array_string_exprt s2 = get_string_expr(f.arguments()[4]);
-  // TODO: where is arguments[3] used?
   array_string_exprt res =
     char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
@@ -175,15 +174,5 @@ exprt string_constraint_generatort::add_axioms_for_insert_double(
 exprt string_constraint_generatort::add_axioms_for_insert_float(
   const function_application_exprt &f)
 {
-  PRECONDITION(f.arguments().size() == 5);
-  const array_string_exprt res =
-    char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
-  const array_string_exprt s1 = get_string_expr(f.arguments()[2]);
-  const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length().type();
-  const typet &char_type = s1.content().type().subtype();
-  const array_string_exprt s2 = fresh_string(index_type, char_type);
-  const exprt return_code =
-    add_axioms_for_string_of_float(s2, f.arguments()[4]);
-  return add_axioms_for_insert(res, s1, s2, offset);
+  return add_axioms_for_insert_double(f);
 }