bug in bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 13, 2022 · d5cc162 · d5cc162
1 parent 2363bfc
commit d5cc162
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
@@ -1377,7 +1377,7 @@ namespace pb {
             return nullptr;
         }
 
-        if (k < lits.size()) {
+        if (k > lits.size()) {
             if (lit == sat::null_literal)
                 s().add_clause(0, nullptr, sat::status::th(false, get_id()));
             else
@@ -1458,6 +1458,7 @@ namespace pb {
         for (auto const [w, l] : wlits)
             weight += w;
         if (weight < k) {
+            std::cout << "weight " << weight << " " << k << "\n";
             if (lit == sat::null_literal)
                 s().add_clause(0, nullptr, sat::status::th(false, get_id()));
             else