diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index df90f9cd4..345019892 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -315,6 +315,23 @@ namespace Microsoft.Z3 #endif #endregion + /// + /// Translates (copies) the function declaration to the Context . + /// + /// A context + /// A copy of the function declaration which is associated with + new public FuncDecl Translate(Context ctx) + { + Contract.Requires(ctx != null); + Contract.Ensures(Contract.Result() != null); + + if (ReferenceEquals(Context, ctx)) + return this; + else + return new FuncDecl(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + } + + /// /// Create expression that applies function to arguments. ///