fix #6692

Z3Prover · Apr 17, 2023 · 1319b64 · 1319b64
1 parent 97b66d1
commit 1319b64
Showing 1 changed file with 6 additions and 5 deletions.
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
@@ -2858,19 +2858,20 @@ namespace pb {
 
     void solver::subsumes(pbc& p1, literal lit) {
         for (constraint* c : m_cnstr_use_list[lit.index()]) {
-            if (c == &p1 || c->was_removed()) continue;
-            bool s = false;
+            if (c == &p1 || c->was_removed() || c->lit() != sat::null_literal)
+                continue;
+            bool sub = false;
             switch (c->tag()) {
             case pb::tag_t::card_t:
-                s = subsumes(p1, c->to_card()); 
+                sub = subsumes(p1, c->to_card()); 
                 break;
             case pb::tag_t::pb_t:
-                s = subsumes(p1, c->to_pb()); 
+                sub = subsumes(p1, c->to_pb()); 
                 break;
             default: 
                 break;
             }
-            if (s) {
+            if (sub) {
                 ++m_stats.m_num_pb_subsumes;                
                 set_non_learned(p1);
                 remove_constraint(*c, "subsumed");