fix #7532

src/sat/sat_integrity_checker.cpp

@@ -22,6 +22,16 @@ Revision History:
 #include "util/trace.h"
 
 namespace sat {
+
+    // move to util.h
+    template<typename S, typename P>
+    unsigned num_true(S const& set, P const& p) {
+        unsigned r = 0;
+        for (auto const& e : set)
+            if (p(e))
+                r++;
+        return r;
+    }
     
     integrity_checker::integrity_checker(solver const & _s):
         s(_s) {
@@ -101,13 +111,7 @@ namespace sat {
     }
 
     bool integrity_checker::check_learned_clauses() const {
-        unsigned num_frozen = 0;
+        unsigned num_frozen = num_true(s.learned(), [&](clause const* c) { return c->frozen(); });
-        clause * const * end = s.end_clauses();
-        for (clause * const * it = s.begin_clauses(); it != end; ++it) {
-            clause & c = *(*it);
-            if (c.frozen())
-                num_frozen++;
-        }
         VERIFY(num_frozen == s.m_num_frozen);
         return check_clauses(s.begin_learned(), s.end_learned());
     }

src/sat/sat_simplifier.h

@@ -66,7 +66,7 @@ namespace sat {
         svector<bin_clause>    m_sub_bin_todo;
         unsigned               m_last_sub_trail_sz; // size of the trail since last cleanup
         bool_var_set           m_elim_todo;
-        bool                   m_need_cleanup;
+        bool                   m_need_cleanup = false;
         tmp_clause             m_dummy;
 
         // simplifier extra variable fields.

src/sat/sat_solver.cpp

@@ -3871,7 +3871,8 @@ namespace sat {
     //
     // -----------------------
     bool solver::check_invariant() const {
-        if (!m_rlimit.inc()) return true;
+        if (!m_rlimit.inc()) 
+            return true;
         if (m_simplifier.need_cleanup())
             return true;
         integrity_checker checker(*this);