diff --git a/regression/jbmc-strings/instanceof/Test.class b/regression/jbmc-strings/instanceof/Test.class
new file mode 100644
index 00000000000..052fc84e521
Binary files /dev/null and b/regression/jbmc-strings/instanceof/Test.class differ
diff --git a/regression/jbmc-strings/instanceof/Test.java b/regression/jbmc-strings/instanceof/Test.java
new file mode 100644
index 00000000000..c01fcccf084
--- /dev/null
+++ b/regression/jbmc-strings/instanceof/Test.java
@@ -0,0 +1,9 @@
+public class Test {
+
+    public static String check(String s) {
+        if (s == null)
+            return "null";
+        assert(s instanceof String);
+        return "non-null";
+    }
+}
diff --git a/regression/jbmc-strings/instanceof/test.desc b/regression/jbmc-strings/instanceof/test.desc
new file mode 100644
index 00000000000..3c597735589
--- /dev/null
+++ b/regression/jbmc-strings/instanceof/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --function Test.check
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 6 .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 2d443a2e890..5c05b26c295 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -554,7 +554,7 @@ codet initialize_nondet_string_struct(
 
   // `obj` is `*expr`
   const struct_typet &struct_type = to_struct_type(ns.follow(obj.type()));
-  const irep_idt &class_id = struct_type.get_tag();
+  const irep_idt &class_id = "java::" + id2string(struct_type.get_tag());
 
   // @clsid = String and @lock = false:
   const symbol_typet jlo_symbol("java::java.lang.Object");
diff --git a/src/java_bytecode/java_root_class.cpp b/src/java_bytecode/java_root_class.cpp
index cbeec3ff40d..4c2d98b43b9 100644
--- a/src/java_bytecode/java_root_class.cpp
+++ b/src/java_bytecode/java_root_class.cpp
@@ -57,7 +57,8 @@ void java_root_class(symbolt &class_symbol)
 /// \param jlo [out] : object to initialize
 /// \param root_type: type of the root class
 /// \param lock: lock field
-/// \param class_identifier: class identifier field
+/// \param class_identifier: class identifier field, generally begins with
+///        "java::" prefix.
 void java_root_class_init(
   struct_exprt &jlo,
   const struct_typet &root_type,
diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
index 3d2dc659b3c..b410805e488 100644
--- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
+++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
@@ -79,7 +79,7 @@ SCENARIO(
           "return_array = cprover_associate_length_to_array_func"
           "(nondet_infinite_array, tmp_object_factory);",
           "arg = { .@java.lang.Object={ .@class_identifier"
-          "=\"java.lang.String\", .@lock=false },"
+          "=\"java::java.lang.String\", .@lock=false },"
           " .length=tmp_object_factory, "
           ".data=nondet_infinite_array };"};