mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

logging checks that can be omitted when GET_CGR is used

Browse source
This commit is contained in:
nilsbecker 2018-10-20 17:24:08 +02:00
parent 91dd01d6ff
commit c73147d8fa
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/mam.cpp
View file

@ -2572,6 +2572,9 @@ namespace smt {
if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \ if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \
goto backtrack; \ goto backtrack; \
update_max_generation(m_n1, nullptr); \ update_max_generation(m_n1, nullptr); \
for (unsigned i = 0; i < static_cast<const get_cgr *>(m_pc)->m_num_args; ++i) { \
m_used_enodes.push_back(std::make_tuple(m_n1->get_arg(i), m_args[i])); \
} \
m_registers[static_cast<const get_cgr *>(m_pc)->m_oreg] = m_n1; \ m_registers[static_cast<const get_cgr *>(m_pc)->m_oreg] = m_n1; \
m_pc = m_pc->m_next; \ m_pc = m_pc->m_next; \
goto main_loop; goto main_loop;