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,