From 745d9c1fe9b8a13e0c3e4dd3f7877c95349ef053 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Tue, 4 Feb 2025 15:49:43 +0100
Subject: [PATCH 1/2] Fixed bug in UP

---
 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 e29bde4a8dd..176353d1e1d 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;
             }
         };
 

From 9111dc37ad576fb05d19e95e77bdc1139702c2ec Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Tue, 4 Feb 2025 15:52:42 +0100
Subject: [PATCH 2/2] Put decrement at the right position

---
 src/api/c++/z3++.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 176353d1e1d..02fbe311bac 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -4315,7 +4315,7 @@ namespace z3 {
                 p.m_callbackNesting++;
             }
             ~scoped_cb() {
-                if (p.m_callbackNesting-- == 0)
+                if (--p.m_callbackNesting == 0)
                     p.cb = nullptr;
             }
         };