mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 19:00:25 +00:00
Code Activity

make sure that we do no access a null m_ctx

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-07-02 15:18:29 -07:00
parent d2990e2f68
commit 5b2226127e
1 changed files with 20 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/smt/tactic/smt_tactic_core.cpp
View file

@ -32,6 +32,7 @@ Notes:
#include "solver/mus.h" #include "solver/mus.h"
#include "solver/parallel_tactical.h" #include "solver/parallel_tactical.h"
#include "solver/parallel_params.hpp" #include "solver/parallel_params.hpp"
#include <atomic>
typedef obj_map<expr, expr *> expr2expr_map; typedef obj_map<expr, expr *> expr2expr_map;
@ -44,6 +45,7 @@ class smt_tactic : public tactic {
vector<std::pair<expr_ref, expr_ref>> m_values; vector<std::pair<expr_ref, expr_ref>> m_values;
statistics m_stats; statistics m_stats;
smt::kernel* m_ctx = nullptr; smt::kernel* m_ctx = nullptr;
mutable std::atomic<bool> m_ctx_destroying;
symbol m_logic; symbol m_logic;
progress_callback* m_callback = nullptr; progress_callback* m_callback = nullptr;
bool m_candidate_models = false; bool m_candidate_models = false;
@ -53,7 +55,8 @@ public:
smt_tactic(ast_manager& m, params_ref const & p): smt_tactic(ast_manager& m, params_ref const & p):
m(m), m(m),
m_params_ref(p), m_params_ref(p),
m_vars(m) { m_vars(m),
m_ctx_destroying(false) {
updt_params_core(p); updt_params_core(p);
TRACE(smt_tactic, tout << "p: " << p << "\n";); TRACE(smt_tactic, tout << "p: " << p << "\n";);
} }
@ -101,10 +104,16 @@ public:
void collect_statistics(statistics & st) const override { void collect_statistics(statistics & st) const override {
if (m_ctx) // Check if context is being destroyed to avoid race condition
m_ctx->collect_statistics(st); // ctx is still running... if (!m_ctx_destroying.load() && m_ctx) {
else try {
st.copy(m_stats); m_ctx->collect_statistics(st);
return;
} catch (...) {
// If exception occurs, fall back to cached stats
}
}
st.copy(m_stats);
} }
void cleanup() override { void cleanup() override {
@ -141,12 +150,18 @@ public:
} }
~scoped_init_ctx() { ~scoped_init_ctx() {
// Signal that we're destroying the context
m_owner.m_ctx_destroying.store(true);
smt::kernel * d = m_owner.m_ctx; smt::kernel * d = m_owner.m_ctx;
m_owner.m_ctx = nullptr; m_owner.m_ctx = nullptr;
m_owner.m_user_ctx = nullptr; m_owner.m_user_ctx = nullptr;
if (d) if (d)
dealloc(d); dealloc(d);
// Reset the flag after cleanup
m_owner.m_ctx_destroying.store(false);
} }
}; };