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

#7362

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-30 14:35:37 -07:00
parent 9a87bb1097
commit 01a419546f
1 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/smt/smt_context.cpp
View file

@ -99,13 +99,16 @@ namespace smt {
m_model_generator->set_context(this); m_model_generator->set_context(this);
} }
::
/** /**
\brief retrieve flag for when cancelation is possible. \brief retrieve flag for when cancelation is possible.
*/ */
bool context::get_cancel_flag() { bool context::get_cancel_flag() {
return !m.limit().inc(); if (m.limit().inc())
return false;
m_last_search_failure = CANCELED;
return true;
} }
void context::updt_params(params_ref const& p) { void context::updt_params(params_ref const& p) {
@ -3745,8 +3748,9 @@ namespace smt {
VERIFY(!resolve_conflict()); VERIFY(!resolve_conflict());
return l_false; return l_false;
} }
if (get_cancel_flag()) if (get_cancel_flag())
return l_undef; return l_undef;
timeit tt(get_verbosity_level() >= 100, "smt.stats"); timeit tt(get_verbosity_level() >= 100, "smt.stats");
reset_model(); reset_model();
SASSERT(at_search_level()); SASSERT(at_search_level());
@ -3959,10 +3963,8 @@ namespace smt {
if (m_last_search_failure != OK) if (m_last_search_failure != OK)
return true; return true;
if (get_cancel_flag()) { if (get_cancel_flag())
m_last_search_failure = CANCELED; return true;
return true;
}
if (m_progress_callback) { if (m_progress_callback) {
m_progress_callback->fast_progress_sample(); m_progress_callback->fast_progress_sample();
@ -3973,10 +3975,8 @@ namespace smt {
} }
} }
if (get_cancel_flag()) { if (get_cancel_flag())
m_last_search_failure = CANCELED; return true;
return true;
}
if (memory::above_high_watermark()) { if (memory::above_high_watermark()) {
m_last_search_failure = MEMOUT; m_last_search_failure = MEMOUT;