Fixed registering expressions in push/pop (#5964)

* Fixed registering expressions in push/pop

* Reused existing function

src/api/api_solver.cpp

@@ -883,8 +883,8 @@ extern "C" {
         Z3_TRY;
         RESET_ERROR_CODE();
         init_solver(c, s);
-        user_propagator::push_eh_t _push = push_eh;
-        user_propagator::pop_eh_t _pop = pop_eh;
+        user_propagator::push_eh_t _push = (void(*)(void*,user_propagator::callback*)) push_eh;
+        user_propagator::pop_eh_t _pop = (void(*)(void*,user_propagator::callback*,unsigned)) pop_eh;
         user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) {
             ast_context_params params;
             params.set_foreign_manager(&m);

src/api/c++/z3++.h

@@ -3964,18 +3964,23 @@ namespace z3 {
             }
         };
 
-        static void push_eh(void* p) {
+        static void push_eh(void* _p, Z3_solver_callback cb) {
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
+            scoped_cb _cb(p, cb);
             static_cast<user_propagator_base*>(p)->push();
         }
 
-        static void pop_eh(void* p, unsigned num_scopes) {
-            static_cast<user_propagator_base*>(p)->pop(num_scopes);
+        static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
+            scoped_cb _cb(p, cb);
+            static_cast<user_propagator_base*>(_p)->pop(num_scopes);
         }
 
-        static void* fresh_eh(void* p, Z3_context ctx) {
+        static void* fresh_eh(void* _p, Z3_context ctx) {
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
             context* c = new context(ctx);
-            static_cast<user_propagator_base*>(p)->subcontexts.push_back(c);
-            return static_cast<user_propagator_base*>(p)->fresh(*c);
+            p->subcontexts.push_back(c);
+            return p->fresh(*c);
         }
 
         static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {

src/api/z3_api.h

@@ -1434,8 +1434,8 @@ Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e));
 /**
    \brief callback functions for user propagator.
 */
-Z3_DECLARE_CLOSURE(Z3_push_eh,    void, (void* ctx));
-Z3_DECLARE_CLOSURE(Z3_pop_eh,     void, (void* ctx, unsigned num_scopes));
+Z3_DECLARE_CLOSURE(Z3_push_eh,    void, (void* ctx, Z3_solver_callback cb));
+Z3_DECLARE_CLOSURE(Z3_pop_eh,     void, (void* ctx, Z3_solver_callback cb, unsigned num_scopes));
 Z3_DECLARE_CLOSURE(Z3_fresh_eh,   void*, (void* ctx, Z3_context new_context));
 Z3_DECLARE_CLOSURE(Z3_fixed_eh,   void, (void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value));
 Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));

src/sat/smt/user_solver.cpp

@@ -88,7 +88,7 @@ namespace user_solver {
     void solver::push_core() {
         th_euf_solver::push_core();
         m_prop_lim.push_back(m_prop.size());
-        m_push_eh(m_user_context);
+        m_push_eh(m_user_context, this);
     }
 
     void solver::pop_core(unsigned num_scopes) {
@@ -96,7 +96,7 @@ namespace user_solver {
         unsigned old_sz = m_prop_lim.size() - num_scopes;
         m_prop.shrink(m_prop_lim[old_sz]);
         m_prop_lim.shrink(old_sz);
-        m_pop_eh(m_user_context, num_scopes);
+        m_pop_eh(m_user_context, this, num_scopes);
     }
 
     void solver::propagate_consequence(prop_info const& prop) {

src/smt/theory_user_propagator.cpp

@@ -25,6 +25,7 @@ using namespace smt;
 theory_user_propagator::theory_user_propagator(context& ctx):
     theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())),
     m_var2expr(ctx.get_manager()),
+    m_push_popping(false),
     m_to_add(ctx.get_manager())
 {}
 
@@ -38,7 +39,7 @@ void theory_user_propagator::force_push() {
         theory::push_scope_eh();
         m_prop_lim.push_back(m_prop.size());
         m_to_add_lim.push_back(m_to_add.size());
-        m_push_eh(m_user_context);
+        m_push_eh(m_user_context, this);
     }
 }
 
@@ -122,7 +123,8 @@ final_check_status theory_user_propagator::final_check_eh() {
     if (!(bool)m_final_eh)
         return FC_DONE;
     force_push();
-    unsigned sz = m_prop.size();
+    unsigned sz1 = m_prop.size();
+    unsigned sz2 = m_expr2var.size();
     try {
         m_final_eh(m_user_context, this);
     }
@@ -130,7 +132,8 @@ final_check_status theory_user_propagator::final_check_eh() {
       throw default_exception("Exception thrown in \"final\"-callback");
     }
     propagate();
-    bool done = (sz == m_prop.size()) && !ctx.inconsistent();
+    // check if it became inconsistent or something new was propagated/registered
+    bool done = !can_propagate() && !ctx.inconsistent();
     return done ? FC_DONE : FC_CONTINUE;
 }
 
@@ -169,11 +172,11 @@ void theory_user_propagator::pop_scope_eh(unsigned num_scopes) {
     old_sz = m_to_add_lim.size() - num_scopes;
     m_to_add.shrink(m_to_add_lim[old_sz]);
     m_to_add_lim.shrink(old_sz);
-    m_pop_eh(m_user_context, num_scopes);
+    m_pop_eh(m_user_context, this, num_scopes);
 }
 
 bool theory_user_propagator::can_propagate() {
-    return m_qhead < m_prop.size() || !m_to_add.empty();
+    return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size();
 }
 
 void theory_user_propagator::propagate_consequence(prop_info const& prop) {

src/tactic/user_propagator_base.h

@@ -21,8 +21,8 @@ namespace user_propagator {
     typedef std::function<void(void*, callback*, expr*, expr*)>      fixed_eh_t;
     typedef std::function<void(void*, callback*, expr*, expr*)>      eq_eh_t;
     typedef std::function<void*(void*, ast_manager&, context_obj*&)> fresh_eh_t;
-    typedef std::function<void(void*)>                 push_eh_t;
-    typedef std::function<void(void*,unsigned)>        pop_eh_t;
+    typedef std::function<void(void*, callback*)>                    push_eh_t;
+    typedef std::function<void(void*, callback*, unsigned)>          pop_eh_t;
     typedef std::function<void(void*, callback*, expr*)>             created_eh_t;