mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix #5253

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-10 13:00:52 -07:00
parent 2ea4b0f4e0
commit f02fbb49bb
2 changed files with 9 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1224,16 +1224,10 @@ namespace q {
m_mp_already_processed[first_idx] = true; m_mp_already_processed[first_idx] = true;
linearise_multi_pattern(first_idx); linearise_multi_pattern(first_idx);
} }
for (unsigned i = 0; i < m_qa->get_num_decls(); i++)
#ifdef Z3DEBUG if (m_vars[i] == -1)
for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { return;
CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n";
tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n";
tout << "tree:\n" << *m_tree << "\n";
);
SASSERT(m_vars[i] >= 0);
}
#endif
SASSERT(head->m_next == 0); SASSERT(head->m_next == 0);
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin()))); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));

14
src/smt/mam.cpp
View file

@ -1218,15 +1218,11 @@ namespace {
linearise_multi_pattern(first_idx); linearise_multi_pattern(first_idx);
} }
#ifdef Z3DEBUG // check that all variables are captured by pattern.
for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { for (unsigned i = 0; i < m_qa->get_num_decls(); i++)
CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; if (m_vars[i] == -1)
tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n"; return;
tout << "tree:\n" << *m_tree << "\n";
);
SASSERT(m_vars[i] >= 0);
}
#endif
SASSERT(head->m_next == 0); SASSERT(head->m_next == 0);
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin()))); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));