mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

fix #6398

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-13 11:16:14 +02:00
parent ddf4895c2f
commit 93e1db0b0b
2 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/mam.cpp
View file

@ -2006,33 +2006,36 @@ namespace {
m_backtrack_stack.resize(t->get_num_choices()); m_backtrack_stack.resize(t->get_num_choices());
} }
void execute(code_tree * t) { bool execute(code_tree * t) {
TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout);); TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
init(t); init(t);
#define CLEANUP for (enode* app : t->get_candidates()) if (app->is_marked()) app->unset_mark();
if (t->filter_candidates()) { if (t->filter_candidates()) {
for (enode* app : t->get_candidates()) { for (enode* app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";); TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";);
if (!app->is_marked() && app->is_cgr()) { if (!app->is_marked() && app->is_cgr()) {
if (m_context.resource_limits_exceeded() || !execute_core(t, app)) if (m_context.resource_limits_exceeded() || !execute_core(t, app)) {
return; CLEANUP;
return false;
}
app->set_mark(); app->set_mark();
} }
} }
for (enode* app : t->get_candidates()) { CLEANUP;
if (app->is_marked())
app->unset_mark();
}
} }
else { else {
for (enode* app : t->get_candidates()) { for (enode* app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";); TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";);
if (app->is_cgr()) { if (app->is_cgr()) {
TRACE("trigger_bug", tout << "is_cgr\n";); TRACE("trigger_bug", tout << "is_cgr\n";);
// scoped_suspend_rlimit susp(m.limit(), false);
if (m_context.resource_limits_exceeded() || !execute_core(t, app)) if (m_context.resource_limits_exceeded() || !execute_core(t, app))
return; return false;
} }
} }
} }
return true;
} }
// init(t) must be invoked before execute_core // init(t) must be invoked before execute_core
@ -3886,7 +3889,8 @@ namespace {
TRACE("trigger_bug", tout << "match\n"; display(tout);); TRACE("trigger_bug", tout << "match\n"; display(tout););
for (code_tree* t : m_to_match) { for (code_tree* t : m_to_match) {
SASSERT(t->has_candidates()); SASSERT(t->has_candidates());
m_interpreter.execute(t); if (!m_interpreter.execute(t))
return;
t->reset_candidates(); t->reset_candidates();
} }
m_to_match.reset(); m_to_match.reset();

2
src/smt/smt_context.cpp
View file

@ -1723,7 +1723,7 @@ namespace smt {
return false; return false;
} }
if (!get_cancel_flag()) { if (!get_cancel_flag()) {
scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level()); // scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
m_qmanager->propagate(); m_qmanager->propagate();
} }
if (inconsistent()) if (inconsistent())