Fixed bug in UP (#7545)

* Fixed bug in UP * Put decrement at the right position
Z3Prover · Feb 4, 2025 · 0919844 · 0919844
1 parent 17d47ca
commit 0919844
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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;
             }
         };