Correct insert builtin function construction

The arguments were not in the right order.
We also need to seperate construction of concatenation since it was
using insertion.

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -210,13 +210,26 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont(
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
 {
-  PRECONDITION(fun_args.size() > 3);
+  PRECONDITION(fun_args.size() > 4);
+  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
+  input1 = array_pool.find(arg1.op1(), arg1.op0());
+  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[4]);
+  input2 = array_pool.find(arg2.op1(), arg2.op0());
+  result = array_pool.find(fun_args[1], fun_args[0]);
+  args.push_back(fun_args[3]);
+  args.insert(args.end(), fun_args.begin() + 5, fun_args.end());
+}
+
+string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
+  const std::vector<exprt> &fun_args,
+  array_poolt &array_pool)
+{
+  PRECONDITION(fun_args.size() == 4);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
   input1 = array_pool.find(arg1.op1(), arg1.op0());
   const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
   input2 = array_pool.find(arg2.op1(), arg2.op0());
   result = array_pool.find(fun_args[1], fun_args[0]);
-  args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
 }
 
 optionalt<std::vector<mp_integer>> eval_string(

src/solvers/refinement/string_refinement_util.h

@@ -242,15 +242,17 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
 
   optionalt<exprt>
   eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+protected:
+  string_insertion_builtin_functiont() = default;
 };
 
 class string_concatenation_builtin_functiont final:
   public string_insertion_builtin_functiont
 {
 public:
   string_concatenation_builtin_functiont(
-    const std::vector<exprt> &fun_args, array_poolt &array_pool):
-    string_insertion_builtin_functiont(fun_args, array_pool) { }
+    const std::vector<exprt> &fun_args, array_poolt &array_pool);
 
   std::vector<mp_integer> eval(
     const std::vector<mp_integer> &input1_value,