diff --git a/scripts/update_api.py b/scripts/update_api.py index b8978ff21..031b39c75 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -365,7 +365,7 @@ def mk_dotnet(dotnet): dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public class LIB\n') dotnet.write(' {\n') - dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' + dotnet.write(' const string Z3_DLL_NAME = \"libz3\";\n' ' \n') dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs index e0002e5be..49b498b1a 100644 --- a/src/api/dotnet/core/DummyContracts.cs +++ b/src/api/dotnet/core/DummyContracts.cs @@ -44,15 +44,21 @@ namespace System.Diagnostics.Contracts 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 p) { return true; } public static bool ForAll(int from, int to, Predicate p) { return true; } + [Conditional("false")] public static void Invariant(bool b) { } public static T[] Result() { return new T[1]; } + [Conditional("false")] public static void EndContractBlock() { } public static T ValueAtReturn(out T v) { T[] t = new T[1]; v = t[0]; return v; } }