(Re-)activating an ancient rule for the treatment of exactInstance of null (#3706)

Author: wadoon

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key

@@ -382,13 +382,15 @@
 
     // ------------ dynamic types ------------------ //
 
-    /* // will be uncommented soon
-        dynamic_type_for_null {
-       \find (G::exactInstance(null) = TRUE ==>)
-       \varcond(G not Null) // Woj: parser doesn't allow this at the moment
-       \replacewith(false)
-     };
-    };*/
+    // Woj: parser doesn't allow this at the moment
+    // will be uncommented soon
+    // MU: ... uncommented more than 18 years later
+    dynamic_type_for_null {
+        \find (G::exactInstance(null))
+        \varcond(\not\same(G,Null))
+        \replacewith(FALSE)
+        \heuristics(concrete)
+    };
 
     // --------------- variable declarations --------------------------------------//