From 39d8053a5496cbd42d3cd067be7cce3068cc999b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 20 Oct 2018 10:32:09 -0700
Subject: [PATCH] remove dummy contracts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/core/DummyContracts.cs | 65 ---------------------------
 src/api/dotnet/core/README.txt        |  4 ++
 2 files changed, 4 insertions(+), 65 deletions(-)
 delete mode 100644 src/api/dotnet/core/DummyContracts.cs

diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs
deleted file mode 100644
index 103cc1288..000000000
--- a/src/api/dotnet/core/DummyContracts.cs
+++ /dev/null
@@ -1,65 +0,0 @@
-/*++
-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
-    {
-        [Conditional("false")]
-        public static void Ensures(bool b) { }
-        [Conditional("false")]
-        public static void Requires(bool b) { }
-        [Conditional("false")]
-        public static void Assume(bool b, string msg) { }
-        [Conditional("false")]
-        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; }
-        [Conditional("false")]
-        public static void Invariant(bool b) { }
-        public static T[] Result<T>() { return new T[1]; }
-        [Conditional("false")]
-        public static void EndContractBlock() { }
-        public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
-    }
-}
diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt
index 7af9cbf2c..fa274f72b 100644
--- a/src/api/dotnet/core/README.txt
+++ b/src/api/dotnet/core/README.txt
@@ -8,4 +8,8 @@ checking. To build this using .NET core, run (in this directory):
 dotnet restore
 dotnet build core.csproj -c Release
 
+If you are building with the cmake system, you should first
+copy over files that are produced by the compiler into
+this directory. You need to copy over Native.cs and Enumeration.cs
+
 -- good luck!