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

Merge pull request #1850 from Nils-Becker/master

Browse source 
adding call to update_max_generation
This commit is contained in:
Nikolaj Bjorner 2018-10-01 21:49:14 -07:00 committed by GitHub
parent 2cf6ada38e c92c431570
commit 620c5d1d81
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/mam.cpp
View file

@ -2571,6 +2571,7 @@ namespace smt {
m_n1 = m_context.get_enode_eq_to(static_cast<const get_cgr *>(m_pc)->m_label, static_cast<const get_cgr *>(m_pc)->m_num_args, m_args.c_ptr()); \ m_n1 = m_context.get_enode_eq_to(static_cast<const get_cgr *>(m_pc)->m_label, static_cast<const get_cgr *>(m_pc)->m_num_args, m_args.c_ptr()); \
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); \
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;