diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 52e017b6c..06e2dc781 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -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 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(); }