From 15ee879602bff36db70049a3e862834808f0f7fb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jan 2025 10:51:12 -0800
Subject: [PATCH] fix #7532

---
 src/sat/sat_integrity_checker.cpp | 18 +++++++++++-------
 src/sat/sat_simplifier.h          |  2 +-
 src/sat/sat_solver.cpp            |  3 ++-
 3 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index cb951ca44..6733feac0 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/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;
-        clause * const * end = s.end_clauses();
-        for (clause * const * it = s.begin_clauses(); it != end; ++it) {
-            clause & c = *(*it);
-            if (c.frozen())
-                num_frozen++;
-        }
+        unsigned num_frozen = num_true(s.learned(), [&](clause const* c) { return c->frozen(); });
         VERIFY(num_frozen == s.m_num_frozen);
         return check_clauses(s.begin_learned(), s.end_learned());
     }
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index a9b7e9ef9..e32c52e4a 100644
--- a/src/sat/sat_simplifier.h
+++ b/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.
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 441457c0a..ba3ed2e3a 100644
--- a/src/sat/sat_solver.cpp
+++ b/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);