diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index e649a94b85d..53561eaba10 100644
--- 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