From e2cf229df26e00b6e274d56af9cc469a7a3e24f3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Feb 2026 07:03:52 -0800
Subject: [PATCH] Remove assertion for number of watches in normalize

---
 src/sat/smt/pb_solver.cpp | 1 -
 1 file changed, 1 deletion(-)

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;