diff --git a/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class
new file mode 100644
index 00000000000..b4af31db093
Binary files /dev/null and b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class differ
diff --git a/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java
new file mode 100644
index 00000000000..eb8200154c6
--- /dev/null
+++ b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java
@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetCharSequence
+{
+  static void main()
+  {
+    CharSequence x = CProver.nondetWithNull();
+    assert x == null || x instanceof CharSequence;
+  }
+}
diff --git a/regression/cbmc-java/NondetCharSequence/test.desc b/regression/cbmc-java/NondetCharSequence/test.desc
new file mode 100644
index 00000000000..baaa60614e5
--- /dev/null
+++ b/regression/cbmc-java/NondetCharSequence/test.desc
@@ -0,0 +1,8 @@
+CORE
+NondetCharSequence.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/NondetString/NondetString.class b/regression/cbmc-java/NondetString/NondetString.class
new file mode 100644
index 00000000000..1e93b74e30f
Binary files /dev/null and b/regression/cbmc-java/NondetString/NondetString.class differ
diff --git a/regression/cbmc-java/NondetString/NondetString.java b/regression/cbmc-java/NondetString/NondetString.java
new file mode 100644
index 00000000000..e2c14ae76f7
--- /dev/null
+++ b/regression/cbmc-java/NondetString/NondetString.java
@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetString
+{
+  static void main()
+  {
+    String x = CProver.nondetWithNull();
+    assert x == null || x instanceof String;
+  }
+}
diff --git a/regression/cbmc-java/NondetString/test.desc b/regression/cbmc-java/NondetString/test.desc
new file mode 100644
index 00000000000..6756c4a7630
--- /dev/null
+++ b/regression/cbmc-java/NondetString/test.desc
@@ -0,0 +1,8 @@
+CORE
+NondetString.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class b/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class
new file mode 100644
index 00000000000..4a2de67ab40
Binary files /dev/null and b/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class differ
diff --git a/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java b/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java
new file mode 100644
index 00000000000..820435872b7
--- /dev/null
+++ b/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java
@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuffer
+{
+  static void main()
+  {
+    StringBuffer x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuffer;
+  }
+}
diff --git a/regression/cbmc-java/NondetStringBuffer/test.desc b/regression/cbmc-java/NondetStringBuffer/test.desc
new file mode 100644
index 00000000000..8c520b5f387
--- /dev/null
+++ b/regression/cbmc-java/NondetStringBuffer/test.desc
@@ -0,0 +1,8 @@
+CORE
+NondetStringBuffer.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.class b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.class
new file mode 100644
index 00000000000..e85a3349f01
Binary files /dev/null and b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.class differ
diff --git a/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java
new file mode 100644
index 00000000000..feec3c3ac6b
--- /dev/null
+++ b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java
@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuilder
+{
+  static void main()
+  {
+    StringBuilder x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuilder;
+  }
+}
diff --git a/regression/cbmc-java/NondetStringBuilder/test.desc b/regression/cbmc-java/NondetStringBuilder/test.desc
new file mode 100644
index 00000000000..6aa68c42d41
--- /dev/null
+++ b/regression/cbmc-java/NondetStringBuilder/test.desc
@@ -0,0 +1,8 @@
+CORE
+NondetStringBuilder.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 4bd9380547f..6e9617cb109 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -841,20 +841,27 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // and asign to `expr` the address of such object
   code_blockt non_null_inst;
 
-  if(
-    java_string_library_preprocesst::implements_java_char_sequence_pointer(
-      expr.type()))
+  // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not
+  // have the expected fields (typically this happens if --refine-strings was not passed). In this
+  // case we fall back to normal pointer target init.
+
+  bool string_init_succeeded = false;
+
+  if(java_string_library_preprocesst::implements_java_char_sequence_pointer(
+       expr.type()))
   {
-    add_nondet_string_pointer_initialization(
-      expr,
-      object_factory_parameters.max_nondet_string_length,
-      object_factory_parameters.string_printable,
-      symbol_table,
-      loc,
-      object_factory_parameters.function_id,
-      assignments);
+    string_init_succeeded =
+      !add_nondet_string_pointer_initialization(
+        expr,
+        object_factory_parameters.max_nondet_string_length,
+        object_factory_parameters.string_printable,
+        symbol_table,
+        loc,
+        object_factory_parameters.function_id,
+        assignments);
   }
-  else
+
+  if(!string_init_succeeded)
   {
     gen_pointer_target_init(
       non_null_inst,