diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs index ce9680a7a..d937b17a9 100644 --- a/src/api/dotnet/UserPropagator.cs +++ b/src/api/dotnet/UserPropagator.cs @@ -41,6 +41,9 @@ namespace Microsoft.Z3 { /// /// Delegate type for fixed callback + /// Note that the life-time of the term and value only applies within the scope of the callback. + /// That means the term and value cannot be stored in an array, dictionary or similar and accessed after the callback has returned. + /// Use the functionality Dup on expressions to create a duplicate copy that extends the lifetime. /// public delegate void FixedEh(Expr term, Expr value);