diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 66a72dea9..0d2328136 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -77,8 +77,6 @@ namespace polysat {
         void gc_clauses();
 
         void normalize_watch(clause& cl);
-        bool watch(clause& cl);
-        void unwatch(clause& cl);
 
         void register_clause(clause* cl);
 
@@ -103,6 +101,9 @@ namespace polysat {
         void gc();
         bool should_gc();
 
+        bool watch(clause& cl);
+        void unwatch(clause& cl);
+
         constraint* lookup(sat::bool_var var) const;
         signed_constraint lookup(sat::literal lit) const;
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b51862b18..50222b7c7 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -349,11 +349,8 @@ namespace polysat {
             clause& c = *m_clauses_to_reinit[i];
             SASSERT(c.on_reinit_stack());
             bool reinit = false;
-#if 0
-            // todo, private methods to constraint_manager
             m_constraints.unwatch(c);
             reinit = m_constraints.watch(c);
-#endif
 
             // reinit <- true if clause is used for propagation