From bb966776b8e79b213c0c785683bfcbfd1d2e24f6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Jul 2022 13:15:05 -0700
Subject: [PATCH] Update UserPropagator.cs

---
 src/api/dotnet/UserPropagator.cs | 3 +++
 1 file changed, 3 insertions(+)

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
     {
         /// <summary>
         /// 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.
         /// </summary>                
         public delegate void FixedEh(Expr term, Expr value);