From 1636e35bf99443d4186f9a4b9c7f828b2aa9502d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Sep 2014 20:11:44 -0700 Subject: [PATCH] fix scope accounting bug in deprecated solver mode Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 3349bed7c..b10621d43 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -343,22 +343,18 @@ namespace api { void context::push() { get_smt_kernel().push(); - if (!m_user_ref_count) { - m_ast_lim.push_back(m_ast_trail.size()); - m_replay_stack.push_back(0); - } + m_ast_lim.push_back(m_ast_trail.size()); + m_replay_stack.push_back(0); } void context::pop(unsigned num_scopes) { for (unsigned i = 0; i < num_scopes; ++i) { - if (!m_user_ref_count) { - unsigned sz = m_ast_lim.back(); - m_ast_lim.pop_back(); - dealloc(m_replay_stack.back()); - m_replay_stack.pop_back(); - while (m_ast_trail.size() > sz) { - m_ast_trail.pop_back(); - } + unsigned sz = m_ast_lim.back(); + m_ast_lim.pop_back(); + dealloc(m_replay_stack.back()); + m_replay_stack.pop_back(); + while (m_ast_trail.size() > sz) { + m_ast_trail.pop_back(); } } SASSERT(num_scopes <= get_smt_kernel().get_scope_level());