From 3849f665d620f823b405e5cfcfad0f04e5ca95fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 14 Jul 2023 10:17:19 -0700
Subject: [PATCH] #6523

---
 src/sat/smt/pb_internalize.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp
index abbd79c44..42b06872a 100644
--- a/src/sat/smt/pb_internalize.cpp
+++ b/src/sat/smt/pb_internalize.cpp
@@ -171,6 +171,15 @@ namespace pb {
             wl.second.neg();
             k += rational(wl.first);
         }
+        if (k < 0) {
+            bool_var v = s().add_var(false);
+            literal l(v, false);
+            s().assign_unit(~l);
+            si.cache(t, l);
+            if (sign) l.neg();
+            return l;
+        }
+            
         check_unsigned(k);
         add_pb_ge(v2, false, wlits, k.get_unsigned());
         if (base_assert) {