Fixed nested user-propagator callbacks in .NET (#6307)

* Fixed nested user-propagator callbacks in .NET * Typo
Z3Prover · Aug 29, 2022 · a0ca5d7 · a0ca5d7
1 parent e2f4fc2
commit a0ca5d7
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs
@@ -71,6 +71,7 @@ public class UserPropagator
         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 @@ public class UserPropagator
 
         void Callback(Action fn, Z3_solver_callback cb)
         {
+            this.callbackNesting++;
             this.callback = cb;
             try
             {
@@ -102,7 +104,9 @@ void Callback(Action fn, Z3_solver_callback cb)
             }
             finally
             {
-                this.callback = IntPtr.Zero;
+                callbackNesting--;
+                if (callbackNesting == 0) // callbacks can be nested (e.g., internalizing new element in "created")
+                    this.callback = IntPtr.Zero;
             }
         }