na

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/api/api_solver.cpp

@@ -886,6 +886,13 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    class api_context_obj : public solver::context_obj {
+        api::context* c;
+    public:
+        api_context_obj(api::context* c):c(c) {}
+        ~api_context_obj() override { dealloc(c); }
+    };
+
     void Z3_API Z3_solver_propagate_init(
         Z3_context  c, 
         Z3_solver   s, 
@@ -898,12 +905,12 @@ extern "C" {
         init_solver(c, s);
         solver::push_eh_t _push = push_eh;
         solver::pop_eh_t _pop = pop_eh;
-        solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, void*& _ctx) {
+        solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, solver::context_obj*& _ctx) {
             context_params params;
             params.set_foreign_manager(&m);
-            auto* ctx = reinterpret_cast<Z3_context>(alloc(api::context, &params, false));
-            _ctx = ctx;
-            return fresh_eh(user_ctx, ctx);
+            auto* ctx = alloc(api::context, &params, false);
+            _ctx = alloc(api_context_obj, ctx);
+            return fresh_eh(user_ctx, reinterpret_cast<Z3_context>(ctx));
         };
         to_solver_ref(s)->user_propagate_init(user_context, _push, _pop, _fresh);
         Z3_CATCH;

src/smt/user_propagator.cpp

@@ -27,7 +27,7 @@ user_propagator::user_propagator(context& ctx):
 {}
 
 user_propagator::~user_propagator() {
-    if (m_api_context) memory::deallocate(m_api_context);
+    dealloc(m_api_context);
 }
 
 void user_propagator::force_push() {
@@ -48,7 +48,10 @@ unsigned user_propagator::add_expr(expr* e) {
     return v;
 }
 
-void user_propagator::propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) {
+void user_propagator::propagate(
+    unsigned num_fixed, unsigned const* fixed_ids, 
+    unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, 
+    expr* conseq) {
     m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));
 }
 

src/smt/user_propagator.h

@@ -57,7 +57,7 @@ namespace smt {
         solver::fixed_eh_t  m_fixed_eh;
         solver::eq_eh_t     m_eq_eh;
         solver::eq_eh_t     m_diseq_eh;
-        void*               m_api_context { nullptr };
+        solver::context_obj*   m_api_context { nullptr };
 
         unsigned               m_qhead { 0 };
         vector<prop_info>      m_prop;

src/solver/solver.h

@@ -243,11 +243,14 @@ class solver : public check_sat_result {
     public:
         virtual void propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0;
     };
-
+    class context_obj {
+    public:
+        virtual ~context_obj() {}
+    };
     typedef std::function<void(void*, solver::propagate_callback*)> final_eh_t;
     typedef std::function<void(void*, solver::propagate_callback*, unsigned, expr*)> fixed_eh_t;
     typedef std::function<void(void*, solver::propagate_callback*, unsigned, unsigned)> eq_eh_t;
-    typedef std::function<void*(void*, ast_manager&, void*&)> fresh_eh_t;
+    typedef std::function<void*(void*, ast_manager&, solver::context_obj*&)> fresh_eh_t;
     typedef std::function<void(void*)>                 push_eh_t;
     typedef std::function<void(void*,unsigned)>        pop_eh_t;