mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

bug in bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-13 15:42:23 -08:00
parent 2363bfc132
commit d5cc162fa7
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1377,7 +1377,7 @@ namespace pb {
return nullptr; return nullptr;
} }
if (k < lits.size()) { if (k > lits.size()) {
if (lit == sat::null_literal) if (lit == sat::null_literal)
s().add_clause(0, nullptr, sat::status::th(false, get_id())); s().add_clause(0, nullptr, sat::status::th(false, get_id()));
else else
@ -1458,6 +1458,7 @@ namespace pb {
for (auto const [w, l] : wlits) for (auto const [w, l] : wlits)
weight += w; weight += w;
if (weight < k) { if (weight < k) {
std::cout << "weight " << weight << " " << k << "\n";
if (lit == sat::null_literal) if (lit == sat::null_literal)
s().add_clause(0, nullptr, sat::status::th(false, get_id())); s().add_clause(0, nullptr, sat::status::th(false, get_id()));
else else