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

@@ -215,7 +215,21 @@ 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 && fun_args.size() <= 6);
   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]);

src/solvers/refinement/string_refinement_util.h

@@ -246,6 +246,9 @@ 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
@@ -254,10 +257,7 @@ class string_concatenation_builtin_functiont final
 public:
   string_concatenation_builtin_functiont(
     const std::vector<exprt> &fun_args,
-    array_poolt &array_pool)
-    : string_insertion_builtin_functiont(fun_args, array_pool)
-  {
-  }
+    array_poolt &array_pool);
 
   std::vector<mp_integer> eval(
     const std::vector<mp_integer> &input1_value,