diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index 93180e583..afae66e46 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -100,6 +100,17 @@ namespace Microsoft.Z3 return Native.Z3_mk_mul(nCtx, (uint)(ts?.Length ?? 0), ts); } + /// + /// Create an expression representing t[0] - t[1] - .... + /// + public Z3_ast MkSub(params Z3_ast[] t) + { + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != IntPtr.Zero)); + var ts = t.ToArray(); + return Native.Z3_mk_sub(nCtx, (uint)(ts?.Length ?? 0), ts); + } + /// /// Create an expression representing t1 / t2. ///