diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index ec0a2df69..630d92d35 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -160,15 +160,18 @@ namespace polysat {
     }
 
     void constraint_manager::gc(solver& s) {
+        LOG_H1("gc");
         gc_clauses(s);
         gc_constraints(s);
     }
 
     void constraint_manager::gc_clauses(solver& s) {
+        LOG_H3("gc_clauses");
         // place to gc redundant clauses
     }
 
     void constraint_manager::gc_constraints(solver& s) {
+        LOG_H3("gc_constraints");
         uint_set used_vars;
         for (auto const& cls : m_clauses)
             for (auto const& cl : cls)
@@ -184,6 +187,7 @@ namespace polysat {
                 continue;
             if (c->is_external())
                 continue;
+            LOG("Erasing: " << show_deref(c));
             erase_bvar(c);
             m_constraints.swap(i, m_constraints.size() - 1);
             m_constraints.pop_back();
diff --git a/src/math/polysat/restart.cpp b/src/math/polysat/restart.cpp
index 05e1378c7..4d2696a89 100644
--- a/src/math/polysat/restart.cpp
+++ b/src/math/polysat/restart.cpp
@@ -35,6 +35,7 @@ namespace polysat {
     }
 
     void restart::operator()() {
+        LOG_H2("Restarting");
         ++s.m_stats.m_num_restarts;
         s.pop_levels(s.m_level - s.base_level());
         m_conflicts_at_restart = s.m_stats.m_num_conflicts;
diff --git a/src/math/polysat/simplify.cpp b/src/math/polysat/simplify.cpp
index fe6662175..3897e1e19 100644
--- a/src/math/polysat/simplify.cpp
+++ b/src/math/polysat/simplify.cpp
@@ -49,7 +49,8 @@ namespace polysat {
     }
 
     void simplify::operator()() {
-      (void)s; // silence warning
+        LOG_H2("Simplify");
+        (void)s; // silence warning
     }
 
 }