diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index 6944dcfa0..41628372f 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -398,7 +398,6 @@ namespace pb {
     }
 
     std::pair<unsigned, unsigned> solver::normalize(wliteral* begin, wliteral* end, unsigned k) {
-        SASSERT(p.num_watch() == 0);
         m_weights.resize(2 * s().num_vars(), 0);
         for (auto it = begin; it != end; ++it) {
             auto [w, lit] = *it;