Remove utf16_native_endian_to_java(std::wstring)

This has been replaced by
utf16_native_endian_to_java_string(std::wstring)

Author: jeannielynnmoulton

src/solvers/strings/string_refinement_util.cpp

@@ -63,7 +63,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
   for(std::size_t i = 0; i < arr.operands().size() && i < length; i++)
     out[i] = numeric_cast_v<unsigned>(to_constant_expr(arr.operands()[i]));
 
-  return utf16_native_endian_to_java(out);
+  return utf16_native_endian_to_java_string(out);
 }
 
 sparse_arrayt::sparse_arrayt(const with_exprt &expr)

src/util/unicode.cpp

@@ -352,17 +352,6 @@ std::string utf16_native_endian_to_java_string(const std::wstring &in)
   return result.str();
 }
 
-/// \param in: String in UTF-16 (native endianness) format
-/// \return String in US-ASCII format, with \\uxxxx escapes for other characters
-std::string utf16_native_endian_to_java(const std::wstring &in)
-{
-  std::ostringstream result;
-  const std::locale loc;
-  for(const auto ch : in)
-    utf16_native_endian_to_java(ch, result, loc);
-  return result.str();
-}
-
 std::string utf16_native_endian_to_utf8(const char16_t utf16_char)
 {
   return utf16_native_endian_to_utf8(std::u16string(1, utf16_char));