From c05a0dfa61fda18f57e2c9e670ba40d0eccf08e4 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Feb 2016 13:10:17 +0000 Subject: [PATCH] revert my previous attempt to simplify the destructor of ctx-simplify there can be assertions at level 0 --- src/tactic/core/ctx_simplify_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 894aea117..95be200a8 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -177,7 +177,8 @@ struct ctx_simplify_tactic::imp { ~imp() { pop(scope_level()); - SASSERT(scope_level() == 0 && m_cache_undo.empty()); + SASSERT(scope_level() == 0); + restore_cache(0); DEBUG_CODE({ for (unsigned i = 0; i < m_cache.size(); i++) { CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from,