diff --git a/jbmc/regression/jbmc/class-fields/Test.class b/jbmc/regression/jbmc/class-fields/Test.class
new file mode 100644
index 00000000000..a69b61691fe
Binary files /dev/null and b/jbmc/regression/jbmc/class-fields/Test.class differ
diff --git a/jbmc/regression/jbmc/class-fields/Test.java b/jbmc/regression/jbmc/class-fields/Test.java
new file mode 100644
index 00000000000..5ee259eb337
--- /dev/null
+++ b/jbmc/regression/jbmc/class-fields/Test.java
@@ -0,0 +1,10 @@
+public class Test {
+
+  public static void main() {
+
+    java.lang.Class c = Test.class;
+    assert false;
+
+  }
+
+}
diff --git a/jbmc/regression/jbmc/class-fields/java/lang/Class.class b/jbmc/regression/jbmc/class-fields/java/lang/Class.class
new file mode 100644
index 00000000000..6af088fde91
Binary files /dev/null and b/jbmc/regression/jbmc/class-fields/java/lang/Class.class differ
diff --git a/jbmc/regression/jbmc/class-fields/java/lang/Class.java b/jbmc/regression/jbmc/class-fields/java/lang/Class.java
new file mode 100644
index 00000000000..96b348b7594
--- /dev/null
+++ b/jbmc/regression/jbmc/class-fields/java/lang/Class.java
@@ -0,0 +1,11 @@
+package java.lang;
+
+public class Class {
+
+  public Integer field;
+
+  protected void cproverNondetInitialize() {
+    org.cprover.CProver.assume(field == null);
+  }
+
+}
diff --git a/jbmc/regression/jbmc/class-fields/test.desc b/jbmc/regression/jbmc/class-fields/test.desc
new file mode 100644
index 00000000000..abf3d4e911c
--- /dev/null
+++ b/jbmc/regression/jbmc/class-fields/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Test\.java line 6.*: FAILURE$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 2556ee4d7e9..62b18d3dcf7 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -94,11 +94,6 @@ static void java_static_lifetime_init(
         if(allow_null)
         {
           irep_idt nameid=sym.symbol_expr().get_identifier();
-          std::string namestr=id2string(nameid);
-          const std::string suffix="@class_model";
-          // Static '.class' fields are always non-null.
-          if(has_suffix(namestr, suffix))
-            allow_null=false;
           if(allow_null && is_java_string_literal_id(nameid))
             allow_null=false;
           if(allow_null && is_non_null_library_global(nameid))
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 6e9617cb109..b8ed2371242 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -874,10 +874,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
-  // Determine whether the pointer can be null. In particular the pointers
-  // inside the java.lang.Class class shall not be null
-  const bool not_null = !allow_null || class_identifier == "java.lang.Class";
-
   // Alternatively, if this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
   bool must_be_null=
@@ -889,7 +885,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
     // <expr> = nullptr;
     new_object_assignments.add(set_null_inst);
   }
-  else if(not_null)
+  else if(!allow_null)
   {
     // Add the following code to assignments:
     // <expr> = <aoe>;