mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 04:41:48 +00:00
Code Activity

Remove assertion for number of watches in normalize

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-02-12 07:03:52 -08:00 • committed by copilot-swe-agent[bot]
parent 0ec79e17cc
commit e2cf229df2
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/pb_solver.cpp
View file

@ -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;