mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

ctx-simplify: simplify destructor

Browse source
This commit is contained in:
Nuno Lopes 2016-02-16 09:53:04 +00:00
parent 98c5a5c86c
commit 293566d464
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -177,8 +177,7 @@ struct ctx_simplify_tactic::imp {
~imp() { ~imp() {
pop(scope_level()); pop(scope_level());
SASSERT(scope_level() == 0); SASSERT(scope_level() == 0 && m_cache_undo.empty());
restore_cache(0);
DEBUG_CODE({ DEBUG_CODE({
for (unsigned i = 0; i < m_cache.size(); i++) { for (unsigned i = 0; i < m_cache.size(); i++) {
CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from,