remove deprecated split_string variant

This function has been deprecated since 14.11.2019, and the replacement is
easy to put in place.

Author: Daniel Kroening

src/util/string_utils.cpp

@@ -99,9 +99,9 @@ void split_string(
   // delim can't be a space character if using strip
   PRECONDITION(!std::isspace(delim) || !strip);
 
-  std::vector<std::string> result;
+  std::vector<std::string> result =
+    split_string(s, delim, strip);
 
-  split_string(s, delim, result, strip);
   if(result.size() != 2)
   {
     throw deserialization_exceptiont{"expected string '" + s +

src/util/string_utils.h

@@ -20,35 +20,22 @@ std::string strip_string(const std::string &s);
 
 std::string capitalize(const std::string &str);
 
+void split_string(
+  const std::string &s,
+  char delim,
+  std::string &left,
+  std::string &right,
+  bool strip=false);
+
 /// Given a string s, split into a sequence of substrings when separated by
 /// specified delimiter.
 /// \param s: The string to split up
 /// \param delim: The character to use as the delimiter
-/// \param [out] result: The sub strings. Must be empty.
 /// \param strip: If true, strip_string will be used on each element, removing
 ///   whitespace from the beginning and end of each element
 /// \param remove_empty: If true, all empty-string elements will be removed.
 ///   This is applied after strip so whitespace only elements will be removed if
 ///   both are set to true.
-DEPRECATED(SINCE(
-  2019,
-  11,
-  14,
-  "use split_string(s, delim, strip, remove_empty) instead"))
-void split_string(
-  const std::string &s,
-  char delim,
-  std::vector<std::string> &result,
-  bool strip = false,
-  bool remove_empty = false);
-
-void split_string(
-  const std::string &s,
-  char delim,
-  std::string &left,
-  std::string &right,
-  bool strip=false);
-
 std::vector<std::string> split_string(
   const std::string &s,
   char delim,