diff --git a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs
index 427e8090..d7d7119b 100644
--- a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs
+++ b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs
@@ -11,6 +11,7 @@
 namespace System.Diagnostics.Contracts
 {
     [AttributeUsage(global::System.AttributeTargets.Assembly)]
+    [ContractVerification(false)]
     internal sealed class ContractDeclarativeAssemblyAttribute : global::System.Attribute
     {
     }
diff --git a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb
index fb02d6b7..25ec8aeb 100644
--- a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb
+++ b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb
@@ -5,8 +5,9 @@
 '  This file is included when building a contract declarative assembly
 '  in order to mark it as such for recognition by the tools
 '
-<Assembly: ContractDeclarativeAssemblyAttribute()> 
+<Assembly: ContractDeclarativeAssemblyAttribute()>
 
+<System.Diagnostics.Contracts.ContractVerification(False)>
 NotInheritable Class ContractDeclarativeAssemblyAttribute
     Inherits Global.System.Attribute
 End Class
diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs
index 5b2109c2..74cb325a 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs
@@ -870,6 +870,7 @@ public virtual Type[] GetGenericParameterConstraints() {
     public virtual MethodInfo[] GetMethods(BindingFlags arg0)
     {
       Contract.Ensures(Contract.Result<MethodInfo[]>() != null);
+      Contract.Ensures(Contract.ForAll(Contract.Result<MethodInfo[]>(), el => el != null));
 
       return default(MethodInfo[]);
     }
@@ -888,7 +889,7 @@ public virtual MethodInfo[] GetMethods()
       Contract.Ensures(Contract.Result<MethodInfo[]>() != null);
       Contract.Ensures(Contract.ForAll(Contract.Result<MethodInfo[]>(), el => el != null));
 
-      return default( MethodInfo[]);
+      return default(MethodInfo[]);
     }
 
     [Pure]
@@ -896,7 +897,7 @@ public virtual MethodInfo GetMethod(string name)
     {
       Contract.Requires(name != null);
 
-      return default( MethodInfo);
+      return default(MethodInfo);
     }
 
     [Pure]
@@ -904,7 +905,7 @@ public virtual MethodInfo GetMethod(string name, BindingFlags bindingAttr)
     {
       Contract.Requires(name != null);
 
-      return default( MethodInfo);
+      return default(MethodInfo);
     }
 
     [Pure]
@@ -913,7 +914,7 @@ public virtual MethodInfo GetMethod(string name, Type[] types)
       Contract.Requires(name != null);
       Contract.Requires(types != null);
 
-      return default( MethodInfo);
+      return default(MethodInfo);
     }
     //public  MethodInfo GetMethod(string name, Type[] types,  ParameterModifier[] modifiers)
     //{
@@ -942,7 +943,7 @@ public virtual ConstructorInfo[] GetConstructors(BindingFlags arg0)
     {
       Contract.Ensures(Contract.Result< ConstructorInfo[]>() != null);
 
-      return default( ConstructorInfo[]);
+      return default(ConstructorInfo[]);
     }
 
     [Pure]
@@ -951,14 +952,14 @@ public virtual ConstructorInfo[] GetConstructors()
       Contract.Ensures(Contract.Result< ConstructorInfo[]>() != null);
       Contract.Ensures(Contract.ForAll(Contract.Result<ConstructorInfo[]>(), el => el != null));
 
-      return default( ConstructorInfo[]);
+      return default(ConstructorInfo[]);
     }
 
     [Pure]
     public virtual ConstructorInfo GetConstructor(Type[] types)
     {
 
-      return default( ConstructorInfo);
+      return default(ConstructorInfo);
     }
 
 #if false
diff --git a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs
index 63568859..f2e4de47 100644
--- a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs
+++ b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs
@@ -7666,7 +7666,6 @@ public static NewArrayExpression NewArrayInit(Type type, params Expression[] ini
     {
       Contract.Requires(type != null);
       Contract.Requires(initializers != null);
-      Contract.Requires(initializers.Length >= 1);
       Contract.Ensures(Contract.Result<NewArrayExpression>() != null);
       return default(NewArrayExpression);
     }
diff --git a/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets b/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets
index 4fd3d2a3..f9912d42 100644
--- a/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets
+++ b/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets
@@ -59,7 +59,18 @@
           <PropertyGroup>
             <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.5</CodeContractsReferenceAssemblyLibPath>
           </PropertyGroup>
-        </When>        <Otherwise>
+        </When>
+        <When Condition="'$(TargetFrameworkVersion)' == 'v4.6'">
+          <PropertyGroup>
+            <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
+          </PropertyGroup>
+        </When>
+        <When Condition="'$(TargetFrameworkVersion)' == 'v4.6.1'">
+          <PropertyGroup>
+            <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
+          </PropertyGroup>
+        </When>
+        <Otherwise>
           <PropertyGroup>
             <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\v3.5</CodeContractsReferenceAssemblyLibPath>
           </PropertyGroup>
diff --git a/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets b/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets
index c8c504c8..50004f77 100644
--- a/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets
+++ b/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets
@@ -70,6 +70,11 @@
             <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
           </PropertyGroup>
         </When>
+        <When Condition="'$(TargetFrameworkVersion)' == 'v4.6.1'">
+          <PropertyGroup>
+            <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
+          </PropertyGroup>
+        </When>
         <Otherwise>
           <PropertyGroup>
             <CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\v3.5</CodeContractsReferenceAssemblyLibPath>