From 091984419e938ea16e143c38b37ef11180e3233c Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Tue, 4 Feb 2025 17:41:28 +0100
Subject: [PATCH] Fixed bug in UP (#7545)

* Fixed bug in UP

* Put decrement at the right position
---
 src/api/c++/z3++.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index e29bde4a8..02fbe311b 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -4305,15 +4305,18 @@ namespace z3 {
         context*   c;
         std::vector<z3::context*> subcontexts;
 
+        unsigned   m_callbackNesting = 0;
         Z3_solver_callback cb { nullptr };
 
         struct scoped_cb {
             user_propagator_base& p;
             scoped_cb(void* _p, Z3_solver_callback cb):p(*static_cast<user_propagator_base*>(_p)) {
                 p.cb = cb;
+                p.m_callbackNesting++;
             }
             ~scoped_cb() {
-                p.cb = nullptr;
+                if (--p.m_callbackNesting == 0)
+                    p.cb = nullptr;
             }
         };