mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-05 17:30:38 -07:00
parent 7cd901019f
commit 6f56d87694
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/q_mam.cpp
View file

@ -1991,7 +1991,8 @@ namespace q {
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);
if (t->filter_candidates()) { if (t->filter_candidates()) {
for (enode* app : t->get_candidates()) { for (unsigned i = 0; i < t->get_candidates().size(); ++i) {
enode* app = t->get_candidates()[i];
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_marked1() && app->is_cgr()) { if (!app->is_marked1() && app->is_cgr()) {
if (ctx.resource_limits_exceeded() || !execute_core(t, app)) if (ctx.resource_limits_exceeded() || !execute_core(t, app))
@ -2005,7 +2006,8 @@ namespace q {
} }
} }
else { else {
for (enode* app : t->get_candidates()) { for (unsigned i = 0; i < t->get_candidates().size(); ++i) {
enode* app = t->get_candidates()[i];
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";);