From 9548b88e711d2abedd5db7c8af3e30c8ac2f200d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 6 Oct 2016 16:24:49 +0100
Subject: [PATCH] Added dummy code contracts for .NET Core/CoreCLR builds.

---
 src/api/dotnet/core/DummyContracts.cs | 59 +++++++++++++++++++++++++++
 src/api/dotnet/core/project.json      | 21 ++++++++++
 2 files changed, 80 insertions(+)
 create mode 100644 src/api/dotnet/core/DummyContracts.cs
 create mode 100644 src/api/dotnet/core/project.json

diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs
new file mode 100644
index 000000000..e0002e5be
--- /dev/null
+++ b/src/api/dotnet/core/DummyContracts.cs
@@ -0,0 +1,59 @@
+/*++
+Copyright (<c>) 2016 Microsoft Corporation
+
+Module Name:
+
+    Contracts.cs
+
+Abstract:
+
+    Z3 Managed API: Dummy Code Contracts class for .NET
+    frameworks that don't support them (e.g., CoreCLR).
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2016-10-06
+
+Notes:
+
+--*/
+
+namespace System.Diagnostics.Contracts
+{
+    public class ContractClass : Attribute
+    {
+        public ContractClass(Type t) { }
+    }
+
+    public class ContractClassFor : Attribute
+    {
+        public ContractClassFor(Type t) { }
+    }
+
+    public class ContractInvariantMethod : Attribute
+    {
+        public ContractInvariantMethod() { }
+    }
+
+    public class ContractVerification : Attribute
+    {
+        public ContractVerification(bool b) { }
+    }
+
+    public class Pure : Attribute { }
+
+    public static class Contract
+    {
+        public static void Ensures(bool b) { }
+        public static void Requires(bool b) { }
+        public static void Assume(bool b, string msg) { }
+        public static void Assert(bool b) { }
+        public static bool ForAll(bool b) { return true; }
+        public static bool ForAll(Object c, Func<Object, bool> p) { return true; }
+        public static bool ForAll(int from, int to, Predicate<int> p) { return true; }
+        public static void Invariant(bool b) { }
+        public static T[] Result<T>() { return new T[1]; }
+        public static void EndContractBlock() { }
+        public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
+    }
+}
\ No newline at end of file
diff --git a/src/api/dotnet/core/project.json b/src/api/dotnet/core/project.json
new file mode 100644
index 000000000..afe281a50
--- /dev/null
+++ b/src/api/dotnet/core/project.json
@@ -0,0 +1,21 @@
+{
+    "version": "1.0.0-*",
+    "buildOptions": {
+        "debugType": "portable",
+        "emitEntryPoint": false,
+        "outputName": "Microsoft.Z3",
+        "compile": [ "../*.cs", "*.cs" ]
+    },
+    "dependencies": { },
+    "frameworks": {
+        "netcoreapp1.0": {
+            "dependencies": {
+                "Microsoft.NETCore.App": {
+                    "type": "platform",
+                    "version": "1.0.1"
+                }
+            },
+            "imports": "dnxcore50"
+        }
+    }
+}