mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

Region scoping

Browse source
This commit is contained in:
CEisenhofer 2022-12-05 15:37:54 +01:00
parent f22aa0eec5
commit 7d58a29bd5
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -247,6 +247,9 @@ namespace xr {
m_prop_queue_lim.push_back(m_prop_queue.size()); m_prop_queue_lim.push_back(m_prop_queue.size());
m_prop_queue_head_queue.push_back(m_prop_queue_head); m_prop_queue_head_queue.push_back(m_prop_queue_head);
//m_justifications_lim.push_back(m_justifications.size()); //m_justifications_lim.push_back(m_justifications.size());
if (m_region)
m_region->push_scope();
} }
void solver::pop_core(unsigned num_scopes) { void solver::pop_core(unsigned num_scopes) {
@ -264,6 +267,9 @@ namespace xr {
} }
m_justifications_lim.shrink(old_sz); m_justifications_lim.shrink(old_sz);
m_justifications.shrink(old_sz);*/ m_justifications.shrink(old_sz);*/
if (m_region)
m_region->pop_scope(num_scopes);
} }
void solver::push() { void solver::push() {