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; } }