mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
ca97bfb4b8
commit
2d358a9a50
|
@ -1346,7 +1346,8 @@ void cmd_context::push() {
|
|||
s.m_macros_stack_lim = m_macros_stack.size();
|
||||
s.m_aux_pdecls_lim = m_aux_pdecls.size();
|
||||
s.m_assertions_lim = m_assertions.size();
|
||||
pm().push();
|
||||
if (!m_global_decls)
|
||||
pm().push();
|
||||
unsigned timeout = m_params.m_timeout;
|
||||
m().limit().push(m_params.rlimit());
|
||||
cancel_eh<reslimit> eh(m().limit());
|
||||
|
@ -1475,7 +1476,8 @@ void cmd_context::pop(unsigned n) {
|
|||
restore_assertions(s.m_assertions_lim);
|
||||
restore_psort_inst(s.m_psort_inst_stack_lim);
|
||||
m_scopes.shrink(new_lvl);
|
||||
pm().pop(n);
|
||||
if (!m_global_decls)
|
||||
pm().pop(n);
|
||||
while (n--) {
|
||||
m().limit().pop();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue