diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MethodReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MethodReference.java
index e8471e3230..6d33fda6e8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MethodReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MethodReference.java
@@ -374,7 +374,8 @@ public void visit(Visitor v) {
     public KeYJavaType getKeYJavaType(Services services, ExecutionContext ec) {
         IProgramMethod meth = method(services, determineStaticPrefixType(services, ec), ec);
         if (meth == null) {
-            return ec.getTypeReference().getKeYJavaType();
+            throw new IllegalStateException(
+                "Could not determine type for method " + name.toString());
         }
         return meth.getReturnType();
 
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java
index 60b6f262fa..10584b0885 100755
--- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java
+++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java
@@ -1,7 +1,7 @@
 package java.lang;
 
 public final class Math {
-    
+
     private Math() {}
     
     /*@ public normal_behavior
@@ -92,4 +92,6 @@ public static float max(float a, float b) {
     public static double pow(double a , double b);
     public static double exp(double a);
     public static double atan(double a);
+
+    public static double random();
 }