Use consistent types with function_application_exprt

It seems that the type should be the return type of the function.

Author: tautschnig

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -185,7 +185,7 @@ SCENARIO("instantiate_not_contains",
   {
     // Creating "ab".lastIndexOf("b", 0)
     const function_application_exprt func(
-      symbol_exprt(ID_cprover_string_last_index_of_func),
+      symbol_exprt(ID_cprover_string_last_index_of_func, t.length_type()),
       {ab, b, from_integer(2)},
       t.length_type());
 

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

@@ -65,19 +65,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 
     // fun1 is s3 = s1.concat(s2)
     const function_application_exprt fun1(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, fun_type),
       {string3.op0(), string3.op1(), string1, string2},
       fun_type);
 
     // fun2 is s5 = s3.concat(s4)
     const function_application_exprt fun2(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, fun_type),
       {string5.op0(), string5.op1(), string3, string4},
       fun_type);
 
     // fun3 is s6 = s5.concat(s2)
     const function_application_exprt fun3(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, fun_type),
       {string6.op0(), string6.op1(), string5, string2},
       fun_type);