diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 764beb470..8896904dd 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -938,6 +938,15 @@ namespace Microsoft.Z3 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } + /// + /// Creates a distinct term. + /// + public BoolExpr MkDistinct(IEnumerable args) + { + Debug.Assert(args != null); + return MkDistinct(args.ToArray()); + } + /// /// Mk an expression representing not(a). ///