mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 16:27:28 -08:00
parent 5c2a9d9936
commit fa605454fb
3 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_context.cpp
View file

@ -3512,6 +3512,7 @@ namespace smt {
TRACE("after_search", display(tout << "result: " << r << "\n"); TRACE("after_search", display(tout << "result: " << r << "\n");
m_case_split_queue->display(tout << "case splits\n"); m_case_split_queue->display(tout << "case splits\n");
); );
m_search_finalized = true;
display_profile(verbose_stream()); display_profile(verbose_stream());
if (r == l_true && get_cancel_flag()) if (r == l_true && get_cancel_flag())
r = l_undef; r = l_undef;
@ -3638,6 +3639,7 @@ namespace smt {
return check(0, nullptr, reset_cancel); return check(0, nullptr, reset_cancel);
} }
else { else {
search_completion sc(*this);
TRACE("before_search", display(tout);); TRACE("before_search", display(tout););
return check_finalize(search()); return check_finalize(search());
} }
@ -3685,6 +3687,7 @@ namespace smt {
if (!check_preamble(reset_cancel)) return l_undef; if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(at_base_level()); SASSERT(at_base_level());
setup_context(false); setup_context(false);
search_completion sc(*this);
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) { if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
expr_ref_vector asms(m, num_assumptions, assumptions); expr_ref_vector asms(m, num_assumptions, assumptions);
parallel p(*this); parallel p(*this);
@ -3716,6 +3719,7 @@ namespace smt {
TRACE("before_search", display(tout);); TRACE("before_search", display(tout););
setup_context(false); setup_context(false);
lbool r = l_undef; lbool r = l_undef;
search_completion sc(*this);
do { do {
pop_to_base_lvl(); pop_to_base_lvl();
expr_ref_vector asms(cube); expr_ref_vector asms(cube);
@ -4728,12 +4732,14 @@ namespace smt {
} }
void context::get_model(model_ref & mdl) { void context::get_model(model_ref & mdl) {
if (inconsistent()) if (inconsistent())
mdl = nullptr; mdl = nullptr;
else if (m_model.get()) else if (m_model.get())
mdl = m_model.get(); mdl = m_model.get();
else if (!m.inc()) else if (!m.inc())
mdl = nullptr; mdl = nullptr;
else if (!m_search_finalized)
mdl = nullptr;
else { else {
mk_proto_model(); mk_proto_model();
if (!m_model && m_proto_model) { if (!m_model && m_proto_model) {

7
src/smt/smt_context.h
View file

@ -1575,6 +1575,13 @@ namespace smt {
bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const; bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const;
#endif #endif
bool check_preamble(bool reset_cancel); bool check_preamble(bool reset_cancel);
struct search_completion {
context& ctx;
search_completion(context& ctx) : ctx(ctx) { ctx.m_search_finalized = false; }
~search_completion() { if (!ctx.m_search_finalized) ctx.m_last_search_failure = CANCELED; }
};
bool m_search_finalized = true;
lbool check_finalize(lbool r); lbool check_finalize(lbool r);
// ----------------------------------- // -----------------------------------

2
src/smt/smt_failure.h
View file

@ -30,7 +30,7 @@ namespace smt {
CANCELED, //!< External cancel flag was set CANCELED, //!< External cancel flag was set
NUM_CONFLICTS, //!< Maximum number of conflicts was reached NUM_CONFLICTS, //!< Maximum number of conflicts was reached
THEORY, //!< Theory is incomplete THEORY, //!< Theory is incomplete
RESOURCE_LIMIT, RESOURCE_LIMIT,
LAMBDAS, //!< Logical context contains lambdas. LAMBDAS, //!< Logical context contains lambdas.
QUANTIFIERS //!< Logical context contains universal quantifiers. QUANTIFIERS //!< Logical context contains universal quantifiers.
}; };