diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/C.class b/jbmc/regression/jbmc-strings/CharacterToChars/C.class
new file mode 100644
index 00000000000..6763c2bc8f0
Binary files /dev/null and b/jbmc/regression/jbmc-strings/CharacterToChars/C.class differ
diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/C.java b/jbmc/regression/jbmc-strings/CharacterToChars/C.java
new file mode 100644
index 00000000000..13b0a4c6c29
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/CharacterToChars/C.java
@@ -0,0 +1,20 @@
+public class C {
+
+    public void test() {
+        char[] c = Character.toChars(5);
+        assert c.length == 1;
+        assert c[0] == 5;
+
+        char[] two_bytes = Character.toChars(0x10000);
+        assert two_bytes.length == 2;
+        assert two_bytes[0] == '\ud800';
+        assert two_bytes[1] == '\udc00';
+    }
+
+    public void shouldFail() {
+        char[] c = Character.toChars(20);
+        assert c.length == 1;
+        assert c[0] == 100;
+    }
+
+}
diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc b/jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc
new file mode 100644
index 00000000000..9576aaffcef
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc
@@ -0,0 +1,10 @@
+CORE
+C.class
+--function C.shouldFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::C\.shouldFail:\(\)V\.assertion.1\] line 16 assertion at file C\.java line 16 function java::C\.shouldFail:\(\)V bytecode-index 12: SUCCESS
+\[java::C\.shouldFail:\(\)V\.assertion.2\] line 17 assertion at file C\.java line 17 function java::C\.shouldFail:\(\)V bytecode-index 23: FAILURE
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/test.desc b/jbmc/regression/jbmc-strings/CharacterToChars/test.desc
new file mode 100644
index 00000000000..bdfb1ce7ebe
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/CharacterToChars/test.desc
@@ -0,0 +1,8 @@
+CORE
+C.class
+--function C.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
index 130f0b4fa5e..cf242141a71 100644
--- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp
+++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
@@ -321,15 +321,6 @@ exprt character_refine_preprocesst::expr_of_high_surrogate(
   return std::move(high_surrogate);
 }
 
-/// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.highSurrogate:(C)Z
-codet character_refine_preprocesst::convert_high_surrogate(
-  conversion_inputt &target)
-{
-  return convert_char_function(
-    &character_refine_preprocesst::expr_of_high_surrogate, target);
-}
-
 /// Determines if the specified character is an ASCII lowercase character.
 /// \param chr: An expression of type character
 /// \param type: A type for the output
@@ -1141,16 +1132,6 @@ exprt character_refine_preprocesst::expr_of_low_surrogate(
   return plus_exprt(uDC00, mod_exprt(chr, u0400));
 }
 
-/// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.lowSurrogate:(I)C
-/// \param target: a position in a goto program
-codet character_refine_preprocesst::convert_low_surrogate(
-  conversion_inputt &target)
-{
-  return convert_char_function(
-    &character_refine_preprocesst::expr_of_low_surrogate, target);
-}
-
 /// Returns the value obtained by reversing the order of the bytes in the
 /// specified char value.
 /// \param chr: An expression of type character
@@ -1174,37 +1155,6 @@ codet character_refine_preprocesst::convert_reverse_bytes(
     &character_refine_preprocesst::expr_of_reverse_bytes, target);
 }
 
-/// Converts the specified character (Unicode code point) to its UTF-16
-/// representation stored in a char array. If the specified code point is a BMP
-/// (Basic Multilingual Plane or Plane 0) value, the resulting char array has
-/// the same value as codePoint. If the specified code point is a supplementary
-/// code point, the resulting char array has the corresponding surrogate pair.
-/// \param chr: An expression of type character
-/// \param type: A type for the output
-/// \return A character array expression of the given type
-exprt character_refine_preprocesst::expr_of_to_chars(
-  const exprt &chr, const typet &type)
-{
-  array_typet array_type=to_array_type(type);
-  const typet &char_type=array_type.subtype();
-  exprt low_surrogate=expr_of_low_surrogate(chr, char_type);
-  array_exprt case1({low_surrogate}, array_type);
-  exprt high_surrogate = expr_of_high_surrogate(chr, char_type);
-  array_exprt case2(
-    {std::move(low_surrogate), std::move(high_surrogate)}, array_type);
-  return if_exprt(
-    expr_of_is_bmp_code_point(chr, type), std::move(case1), std::move(case2));
-}
-
-/// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.toChars:(I)[C
-/// \param target: a position in a goto program
-codet character_refine_preprocesst::convert_to_chars(conversion_inputt &target)
-{
-  return convert_char_function(
-    &character_refine_preprocesst::expr_of_to_chars, target);
-}
-
 /// Converts function call to an assignment of an expression corresponding to
 /// the java method Character.toCodePoint:(CC)I
 /// \param target: a position in a goto program
@@ -1433,8 +1383,6 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_get_type_int;
   conversion_table["java::java.lang.Character.hashCode:()I"]=
       &character_refine_preprocesst::convert_hash_code;
-  conversion_table["java::java.lang.Character.highSurrogate:(I)C"]=
-      &character_refine_preprocesst::convert_high_surrogate;
   conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
       &character_refine_preprocesst::convert_is_alphabetic;
   conversion_table["java::java.lang.Character.isBmpCodePoint:(I)Z"]=
@@ -1523,8 +1471,6 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_is_whitespace_char;
   conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
       &character_refine_preprocesst::convert_is_whitespace_int;
-  conversion_table["java::java.lang.Character.lowSurrogate:(I)C"]=
-      &character_refine_preprocesst::convert_is_low_surrogate;
 
   // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
   // Not supported "java::java.lang.Character.offsetByCodePoints:"
@@ -1532,8 +1478,6 @@ void character_refine_preprocesst::initialize_conversion_table()
 
   conversion_table["java::java.lang.Character.reverseBytes:(C)C"]=
       &character_refine_preprocesst::convert_reverse_bytes;
-  conversion_table["java::java.lang.Character.toChars:(I)[C"]=
-      &character_refine_preprocesst::convert_to_chars;
 
   // Not supported "java::java.lang.Character.toChars:(I[CI)I"