diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index a8de05e0f..cb951ca44 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -45,6 +45,7 @@ namespace sat {
     }
 
     bool integrity_checker::check_clause(clause const & c) const {
+        CTRACE("sat_bug", c.was_removed(), s.display(tout << "c: " << c.id() << ": " << c << "\n"));
         SASSERT(!c.was_removed());
         for (unsigned i = 0; i < c.size(); i++) {
             VERIFY(c[i].var() <= s.num_vars());
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index a1bd18901..a9b7e9ef9 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -247,6 +247,8 @@ namespace sat {
 
         bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
 
+        bool need_cleanup() const { return m_need_cleanup; }
+
     };
 };
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 4390729fd..441457c0a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -89,7 +89,7 @@ namespace sat {
 
     solver::~solver() {
         m_ext = nullptr;
-        SASSERT(m_config.m_num_threads > 1 || m_trim || check_invariant());
+        SASSERT(m_config.m_num_threads > 1 || m_trim || rlimit().is_canceled() || check_invariant());
         CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
         del_clauses(m_clauses);
         CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
@@ -3872,6 +3872,8 @@ namespace sat {
     // -----------------------
     bool solver::check_invariant() const {
         if (!m_rlimit.inc()) return true;
+        if (m_simplifier.need_cleanup())
+            return true;
         integrity_checker checker(*this);
         VERIFY(checker());
         VERIFY(!m_ext || m_ext->validate());