From a0ca5d745e6cefc93358b18ff29774ec569c96f8 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Mon, 29 Aug 2022 02:49:15 +0200
Subject: [PATCH] Fixed nested user-propagator callbacks in .NET (#6307)

* Fixed nested user-propagator callbacks in .NET

* Typo
---
 src/api/dotnet/UserPropagator.cs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs
index 3e9344556..9b4fbc9b7 100644
--- a/src/api/dotnet/UserPropagator.cs
+++ b/src/api/dotnet/UserPropagator.cs
@@ -71,6 +71,7 @@ namespace Microsoft.Z3
         Solver solver;
         Context ctx;
         Z3_solver_callback callback = IntPtr.Zero;
+        int callbackNesting = 0;
         FixedEh fixed_eh;
         Action final_eh;
         EqEh eq_eh;
@@ -91,6 +92,7 @@ namespace Microsoft.Z3
 
         void Callback(Action fn, Z3_solver_callback cb)
         {
+            this.callbackNesting++;
             this.callback = cb;
             try
             {
@@ -102,7 +104,9 @@ namespace Microsoft.Z3
             }
             finally
             {
-                this.callback = IntPtr.Zero;
+                callbackNesting--;
+                if (callbackNesting == 0) // callbacks can be nested (e.g., internalizing new element in "created")
+                    this.callback = IntPtr.Zero;
             }
         }