mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix scope accounting bug in deprecated solver mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-16 20:11:44 -07:00
parent e8b9c251d5
commit 1636e35bf9
1 changed files with 8 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/api/api_context.cpp
View file

@ -343,22 +343,18 @@ namespace api {
void context::push() { void context::push() {
get_smt_kernel().push(); get_smt_kernel().push();
if (!m_user_ref_count) { m_ast_lim.push_back(m_ast_trail.size());
m_ast_lim.push_back(m_ast_trail.size()); m_replay_stack.push_back(0);
m_replay_stack.push_back(0);
}
} }
void context::pop(unsigned num_scopes) { void context::pop(unsigned num_scopes) {
for (unsigned i = 0; i < num_scopes; ++i) { for (unsigned i = 0; i < num_scopes; ++i) {
if (!m_user_ref_count) { unsigned sz = m_ast_lim.back();
unsigned sz = m_ast_lim.back(); m_ast_lim.pop_back();
m_ast_lim.pop_back(); dealloc(m_replay_stack.back());
dealloc(m_replay_stack.back()); m_replay_stack.pop_back();
m_replay_stack.pop_back(); while (m_ast_trail.size() > sz) {
while (m_ast_trail.size() > sz) { m_ast_trail.pop_back();
m_ast_trail.pop_back();
}
} }
} }
SASSERT(num_scopes <= get_smt_kernel().get_scope_level()); SASSERT(num_scopes <= get_smt_kernel().get_scope_level());