diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Math.cs b/Microsoft.Research/Contracts/MsCorlib/System.Math.cs
index a0a985e0..47f53711 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.Math.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.Math.cs
@@ -93,29 +93,40 @@ public static Decimal Abs(Decimal value)
     [Pure]
     public static float Abs(float value)
     {
+      Contract.Ensures((Contract.Result<float>() >= 0.0) || float.IsNaN(Contract.Result<float>()) || float.IsPositiveInfinity(Contract.Result<float>()));
+
+      // 2015-03-26: tom-englert
+      // Disabled, since this was too complex for the checker to understand.
+      // e.g. new Rect(0, 0, Math.Abs(a), Math.Abs(b)) raised a warning that with and height are unproven to be positive values.
+
       // !NaN ==>  >= 0
-      Contract.Ensures(float.IsNaN(value) || Contract.Result<float>() >= 0.0);
+      // Contract.Ensures(float.IsNaN(value) || Contract.Result<float>() >= 0.0);
 
       // NaN ==> NaN
-      Contract.Ensures(!float.IsNaN(value) || float.IsNaN(Contract.Result<float>()));
+      // Contract.Ensures(!float.IsNaN(value) || float.IsNaN(Contract.Result<float>()));
 
       // Infty ==> +Infty
-      Contract.Ensures(!float.IsInfinity(value) || float.IsPositiveInfinity(Contract.Result<float>()));
+      // Contract.Ensures(!float.IsInfinity(value) || float.IsPositiveInfinity(Contract.Result<float>()));
 
       return default(float);
     }
 
     [Pure]
     public static double Abs(double value)
-    {      
+    {
+      Contract.Ensures((Contract.Result<double>() >= 0.0) || double.IsNaN(Contract.Result<double>()) || double.IsPositiveInfinity(Contract.Result<double>()));
+
+      // 2015-03-26: tom-englert
+      // Disabled, since this was too complex for the checker to understand.
+      // e.g. new Rect(0, 0, Math.Abs(a), Math.Abs(b)) raised a warning that with and height are unproven to be positive values.
+
       // !NaN ==>  >= 0
-      Contract.Ensures(double.IsNaN(value) || Contract.Result<double>() >= 0.0);
+      // Contract.Ensures(double.IsNaN(value) || Contract.Result<double>() >= 0.0);
 
       // NaN ==> NaN
-      Contract.Ensures(!double.IsNaN(value) || double.IsNaN(Contract.Result<double>()));
-
+      // Contract.Ensures(!double.IsNaN(value) || double.IsNaN(Contract.Result<double>()));
       // Infty ==> +Infty
-      Contract.Ensures(!double.IsInfinity(value) || double.IsPositiveInfinity(Contract.Result<double>()));
+      // Contract.Ensures(!double.IsInfinity(value) || double.IsPositiveInfinity(Contract.Result<double>()));
 
       return default(double);
     }
diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs
index a6484eee..af2ee496 100644
--- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs
+++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Rect.cs
@@ -16,6 +16,7 @@
 using System.ComponentModel;
 using System.Diagnostics.Contracts;
 
+
 namespace System.Windows
 {
   // Summary:
@@ -214,7 +215,7 @@ public double Height
       }
       set
       {
-        Contract.Requires(!this.IsEmpty);
+        // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
         Contract.Requires(value >= 0.0 || Double.IsNaN(value));
 
         Contract.Ensures(this.Height == value || Double.IsNaN(value));
@@ -339,7 +340,7 @@ public double Width
       }
       set
       {
-        Contract.Requires(!this.IsEmpty);
+        // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
         Contract.Requires(value >= 0.0 || Double.IsNaN(value));
 
         Contract.Ensures(this.Width == value || Double.IsNaN(value));
@@ -361,7 +362,7 @@ public double X
       }
       set
       {
-        Contract.Requires(!this.IsEmpty);
+        // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
 
         Contract.Ensures(this.X == value || Double.IsNaN(value));
       }
@@ -382,7 +383,7 @@ public double Y
       }
       set
       {
-        Contract.Requires(!this.IsEmpty);
+        // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
 
         Contract.Ensures(this.Y == value || Double.IsNaN(value));
       }
@@ -484,8 +485,7 @@ public double Y
     //     the rectangle's System.Windows.Rect.Top and System.Windows.Rect.Bottom properties.
     public void Inflate(Size size)
     {
-      Contract.Requires(!this.IsEmpty);
-
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.Contract.Requires(!this.IsEmpty);
     }
     //
     // Summary:
@@ -500,8 +500,7 @@ public void Inflate(Size size)
     //     The amount by which to expand or shrink the top and bottom sides of the rectangle.
     public void Inflate(double width, double height)
     {
-      Contract.Requires(!this.IsEmpty);
-
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
     }
     //
     // Summary:
@@ -523,7 +522,7 @@ public void Inflate(double width, double height)
     //     The resulting rectangle.
     public static Rect Inflate(Rect rect, Size size)
     {
-      Contract.Requires(!rect.IsEmpty);
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
 
       return default(Rect);
     }
@@ -546,7 +545,7 @@ public static Rect Inflate(Rect rect, Size size)
     //     The resulting rectangle.
     public static Rect Inflate(Rect rect, double width, double height)
     {
-      Contract.Requires(!rect.IsEmpty);
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
 
       return default(Rect);
     }
@@ -599,8 +598,7 @@ public static Rect Inflate(Rect rect, double width, double height)
     //     This method is called on the System.Windows.Rect.Empty rectangle.
     public void Offset(Vector offsetVector)
     {
-      Contract.Requires(!this.IsEmpty);
-
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
     }
     //
     // Summary:
@@ -618,8 +616,7 @@ public void Offset(Vector offsetVector)
     //     This method is called on the System.Windows.Rect.Empty rectangle.
     public void Offset(double offsetX, double offsetY)
     {
-      Contract.Requires(!this.IsEmpty);
-
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
     }
     //
     // Summary:
@@ -641,7 +638,7 @@ public void Offset(double offsetX, double offsetY)
     //     rect is System.Windows.Rect.Empty.
     public static Rect Offset(Rect rect, Vector offsetVector)
     {
-      Contract.Requires(!rect.IsEmpty);
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
 
       return default(Rect);
     }
@@ -668,7 +665,7 @@ public static Rect Offset(Rect rect, Vector offsetVector)
     //     rect is System.Windows.Rect.Empty.
     public static Rect Offset(Rect rect, double offsetX, double offsetY)
     {
-      Contract.Requires(!rect.IsEmpty);
+      // Contract.Requires(!this.IsEmpty); => Is true, but impossible to proof with acceptable effort.
 
       return default(Rect);
     }
diff --git a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs
index 6e2ea04a..5598ccfb 100644
--- a/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs
+++ b/Microsoft.Research/Contracts/WindowsBase/System.Windows.Size.cs
@@ -140,7 +140,7 @@ public double Height
       }
       set
       {
-        Contract.Requires(!this.IsEmpty);
+        // Contract.Requires(!this.IsEmpty); => see comment in Rect
         Contract.Requires(value >= 0.0 || Double.IsNaN(value));
 
         Contract.Ensures(this.Height == value || Double.IsNaN(value));
@@ -179,7 +179,7 @@ public double Width
       }
       set
       {
-        Contract.Requires(!this.IsEmpty);
+        // Contract.Requires(!this.IsEmpty); => see comment in Rect
         Contract.Requires(value >= 0.0 || Double.IsNaN(value));
 
         Contract.Ensures(this.Width == value || Double.IsNaN(value));