From 293566d464f3d39edccbe0a13b9d013c7f0e4251 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Feb 2016 09:53:04 +0000 Subject: [PATCH] ctx-simplify: simplify destructor --- src/tactic/core/ctx_simplify_tactic.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 95be200a8..894aea117 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -177,8 +177,7 @@ struct ctx_simplify_tactic::imp { ~imp() { pop(scope_level()); - SASSERT(scope_level() == 0); - restore_cache(0); + SASSERT(scope_level() == 0 && m_cache_undo.empty()); DEBUG_CODE({ for (unsigned i = 0; i < m_cache.size(); i++) { CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from,