From 366cd9b16ddc8b5808d1dbb2e65af394b8f02622 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Jan 2022 14:50:40 -0800
Subject: [PATCH] missing pb cases

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

diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index b88ba7715..8ac81343a 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -1370,6 +1370,15 @@ namespace pb {
             s().mk_clause(_lits.size(), _lits.data(), sat::status::th(learned, get_id()));
             return nullptr;
         }
+        if (k == 0 && lit == sat::null_literal)
+            return nullptr;
+
+        if (k == 0) {
+            s().assign_unit(lit);
+            return nullptr;
+        }
+            
+
         if (!learned && clausify(lit, lits.size(), lits.data(), k)) {
             return nullptr;
         }