Make the models compile with JDK 25

src/main/java/java/lang/Class.java

@@ -271,7 +271,9 @@ public ClassLoader getClassLoader() {
             // DIFFBLUE MODEL LIBRARY
             // removed for compatibility with Java 9 and newer
             // ClassLoader.checkClassLoaderPermission(cl, Reflection.getCallerClass());
-            ClassLoader.checkClassLoaderPermission(cl, null);
+            // removed for compatibility with Java 25, where this method no
+            // longer exists
+            // ClassLoader.checkClassLoaderPermission(cl, null);
         }
         return cl;
     }

src/main/java/java/lang/Object.java

@@ -34,10 +34,9 @@ public class Object {
     // lock needed for synchronization in JBMC
     // used by monitorenter, monitorexit, wait, and notify
     // Not present in the original Object class
-    public int cproverMonitorCount;
+    public int cproverMonitorCount = 0;
 
     public Object() {
-      cproverMonitorCount = 0;
     }
 
     /**

src/main/java/java/net/URLEncoder.java

@@ -35,10 +35,6 @@
 import java.nio.charset.IllegalCharsetNameException;
 import java.nio.charset.UnsupportedCharsetException ;
 import java.util.BitSet;
-import java.security.AccessController;
-import java.security.PrivilegedAction;
-import sun.security.action.GetBooleanAction;
-import sun.security.action.GetPropertyAction;
 
 /**
  * Utility class for HTML form encoding. This class contains static methods
@@ -140,9 +136,11 @@ public class URLEncoder {
         dontNeedEncoding.set('.');
         dontNeedEncoding.set('*');
 
-        dfltEncName = AccessController.doPrivileged(
-            new GetPropertyAction("file.encoding")
-        );
+        // DIFFBLUE MODEL LIBRARY
+        // sun.security.action.GetPropertyAction is not available in Java 25,
+        // and AccessController.doPrivileged has no effect without a
+        // security manager
+        dfltEncName = System.getProperty("file.encoding");
     }
 
     /**