diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 5b336a2d5..91a4ba358 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -232,6 +232,7 @@ namespace polysat {
     void constraint_manager::gc_clauses() {
         LOG_H3("gc_clauses");
         // place to gc redundant clauses
+        // clauses on_reinit_stack() cannot be gc'ed
     }
 
     void constraint_manager::gc_constraints() {
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 2710dfb70..1619223c8 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -106,6 +106,13 @@ namespace polysat {
         bool watch(clause& cl);
         void unwatch(clause& cl);
 
+        unsigned num_clauses() const {
+            unsigned n = 0;
+            for (auto const& lvl : m_clauses)
+                n += lvl.size();
+            return n;
+        }
+
         constraint* lookup(sat::bool_var var) const;
         signed_constraint lookup(sat::literal lit) const;