From d5cc162fa788e143e04d45a5cddbe84c7e319583 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 13 Jan 2022 15:42:23 -0800
Subject: [PATCH] bug in bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/pb_solver.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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